Previously we used to desugar implications and biconditionals into equivalent CNF/DNF as soon as possible. However, this desugaring makes debug output (Environment::dump()) less readable than it could be. Therefore, it makes sense to keep the sugared representation of a boolean formula, and desugar it in the solver. Reviewed By: sgatev, xazax.hun, wyt Differential Revision: https://reviews.llvm.org/D130519
7.3 KiB
7.3 KiB