improved efficiency of BDD-infer

also use "if c then e1 else e2" in generated formulas instead of (c /\ e1) / (not c /\ e2)