This does not mean the formula is fully in NNF (the ITE condition appears both negated and unnegated, conceptually), but this enables the anti-prenex and scalar quantifier optimizations inside ITE conditions.
This provides a performance boost in the case of complex formulas inside an ITE and fixes the issue from #111.
This does not mean the formula is fully in NNF (the ITE condition appears both negated and unnegated, conceptually), but this enables the anti-prenex and scalar quantifier optimizations inside ITE conditions.
This provides a performance boost in the case of complex formulas inside an ITE and fixes the issue from #111.
Resolves #111