Learning Effective BDD Variable Orders for BDD-based Program Analysis