Improved simplification effectiveness on conjunctions and disjunctions

pysmt/simplifier.py

@@ -79,28 +79,54 @@ def walk_debug(self, formula, **kwargs):
         return res
 
     def walk_and(self, formula, args, **kwargs):
-        args = [x for x in args if not x.is_true()]
-        if len(args) == 0:
-            return self.manager.TRUE()
-        elif len(args) == 1:
-            return args[0]
-        else:
-            if any(x.is_false() for x in args):
+        new_args = set()
+        for a in args:
+            if a.is_true():
+                continue
+            if a.is_false():
                 return self.manager.FALSE()
 
-        return self.manager.And(args)
+            if a.is_and():
+                for s in a.args():
+                    if self.walk_not(self.manager.Not(s), [s]) in new_args:
+                        return self.manager.FALSE()
+                    new_args.add(s)
+            else:
+                if self.walk_not(self.manager.Not(a), [a]) in new_args:
+                    return self.manager.FALSE()
+                new_args.add(a)
 
-    def walk_or(self, formula, args, **kwargs):
-        args = [x for x in args if not x.is_false()]
-        if len(args) == 0:
-            return self.manager.FALSE()
-        elif len(args) == 1:
-            return args[0]
+        if len(new_args) == 0:
+            return self.manager.TRUE()
+        elif len(new_args) == 1:
+            return next(iter(new_args))
         else:
-            if any(x.is_true() for x in args):
+            return self.manager.And(new_args)
+
+    def walk_or(self, formula, args, **kwargs):
+        new_args = set()
+        for a in args:
+            if a.is_false():
+                continue
+            if a.is_true():
                 return self.manager.TRUE()
 
-        return self.manager.Or(args)
+            if a.is_or():
+                for s in a.args():
+                    if self.walk_not(self.manager.Not(s), [s]) in new_args:
+                        return self.manager.TRUE()
+                    new_args.add(s)
+            else:
+                if self.walk_not(self.manager.Not(a), [a]) in new_args:
+                    return self.manager.TRUE()
+                new_args.add(a)
+
+        if len(new_args) == 0:
+            return self.manager.FALSE()
+        elif len(new_args) == 1:
+            return next(iter(new_args))
+        else:
+            return self.manager.Or(new_args)
 
     def walk_not(self, formula, args, **kwargs):
         assert len(args) == 1

pysmt/test/test_simplify.py

@@ -20,7 +20,7 @@
 from pysmt.test.examples import get_example_formulae
 from pysmt.environment import get_env
 from pysmt.shortcuts import (Array, Store, Int, Iff, Symbol, Plus, Equals, And,
-                             Real, Times)
+                             Real, Times, Not, FALSE, Or, TRUE)
 from pysmt.typing import INT, REAL
 from pysmt.simplifier import BddSimplifier
 from pysmt.logics import QF_BOOL
@@ -109,5 +109,28 @@ def test_times_one(self):
         f = f.simplify()
         self.assertNotIn(Real(1), f.args())
 
+
+    def test_and_flattening(self):
+        x,y,z = (Symbol(name) for name in "xyz")
+        f1 = And(x, y, z)
+        f2 = And(x, And(y, z))
+        self.assertEqual(f2.simplify(), f1)
+
+    def test_or_flattening(self):
+        x,y,z = (Symbol(name) for name in "xyz")
+        f1 = Or(x, y, z)
+        f2 = Or(x, Or(y, z))
+        self.assertEqual(f2.simplify(), f1)
+
+    def test_trivial_false_and(self):
+        x,y,z = (Symbol(name) for name in "xyz")
+        f = And(x, y, z, Not(x))
+        self.assertEqual(f.simplify(), FALSE())
+
+    def test_trivial_true_or(self):
+        x,y,z = (Symbol(name) for name in "xyz")
+        f = Or(x, y, z, Not(x))
+        self.assertEqual(f.simplify(), TRUE())
+
 if __name__ == '__main__':
     main()