Fixed: bug in Formula::Normalize(); improved Formula::Flatten().
* Formula::Normalize() was missing a negation: normalization of ~c should be ~c when c is no unit clause, but it was just c. * Formula::Flatten() now also leads to clausal form in a negated context provided the original clause is a unit clause: it now adds a double negation. * Improved error reporting in Parser.
Loading
Please register or sign in to comment