Merge pull request #219 from pysmt/fix-cnf-inplication-bug

BUGFIX in CNF converter

pysmt/rewritings.py

@@ -141,8 +141,9 @@ def walk_implies(self, formula,  args, **kwargs):
         k = self._key_var(formula)
         not_a = self.mgr.Not(a).simplify()
         not_b = self.mgr.Not(b).simplify()
+        not_k = self.mgr.Not(k)
 
-        return k, (cnf_a | cnf_b | frozenset([frozenset([not_a, b, k]),
+        return k, (cnf_a | cnf_b | frozenset([frozenset([not_a, b, not_k]),
                                               frozenset([a, k]),
                                               frozenset([not_b, k])]))
 

pysmt/test/test_cnf.py

@@ -18,7 +18,7 @@
 import os
 from nose.plugins.attrib import attr
 
-from pysmt.shortcuts import Implies, is_sat, is_valid, reset_env
+from pysmt.shortcuts import Implies, is_sat, reset_env, Symbol, Iff
 from pysmt.rewritings import CNFizer
 from pysmt.logics import QF_BOOL, QF_LRA, QF_LIA, QF_UFLIRA
 from pysmt.test import TestCase, skipIfNoSolverForLogic, main
@@ -90,5 +90,15 @@ def _smtlib_cnf(self, filename, logic, res_is_sat):
         res = is_sat(cnf, logic=logic)
         self.assertEqual(res, res_is_sat)
 
+    @skipIfNoSolverForLogic(QF_BOOL)
+    def test_implies(self):
+        a,b,c,d = (Symbol(x) for x in "abcd")
+        f = Implies(Iff(a, b), Iff(c, d))
+
+        conv = CNFizer()
+        cnf = conv.convert_as_formula(f)
+
+        self.assertValid(Implies(cnf, f), logic=QF_BOOL)
+
 if __name__ == '__main__':
     main()