Fixed: Formula::Flatten() handled positive literals like definitions.
Formula::Flatten() manages a term-to-var map to avoid unnecessarily new variables. The map is initialized with all variables that are 'set' in the clause already. That is, every literal (f(...) != x) boils down to an entry that maps f(...) to x. The bug was that this entry was also made for (f(...) == x) literals.
Loading
Please register or sign in to comment