Repository: pysmt/pysmt

Issue:
IdentityDagWalker lacks BV support

Discussion:

Patch:
diff --git a/pysmt/simplifier.py b/pysmt/simplifier.py
index 418bc0d..3303577 100644
--- a/pysmt/simplifier.py
+++ b/pysmt/simplifier.py
@@ -445,7 +445,7 @@ class Simplifier(walkers.DagWalker):
                 res = args[0].bv_unsigned_value() // args[1].bv_unsigned_value()
                 res = res % 2**formula.bv_width()
             return self.manager.BV(res, width=formula.bv_width())
-        return self.manager.BVUdiv(*args)
+        return self.manager.BVUDiv(*args)
 
     def walk_bv_urem(self, formula, args):
         if args[0].is_bv_constant() and args[1].is_bv_constant:
@@ -454,7 +454,7 @@ class Simplifier(walkers.DagWalker):
             else:
                 res = args[0].bv_unsigned_value() % args[1].bv_unsigned_value()
             return self.manager.BV(res, width=formula.bv_width())
-        return self.manager.BVUrem(*args)
+        return self.manager.BVURem(*args)
 
     def walk_bv_ult(self, formula, args):
         if args[0].is_bv_constant() and args[1].is_bv_constant:
@@ -506,7 +506,7 @@ class Simplifier(walkers.DagWalker):
             filler = bitstr[0]
             res = filler*formula.bv_extend_step() + bitstr
             return self.manager.BV(res, width=formula.bv_width())
-        return self.manager.BVSext(args[0], formula.bv_extend_step())
+        return self.manager.BVSExt(args[0], formula.bv_extend_step())
 
     def walk_bv_zext(self, formula, args):
         if args[0].is_bv_constant():
@@ -517,7 +517,7 @@ class Simplifier(walkers.DagWalker):
         return self.manager.BVZExt(args[0], formula.bv_extend_step())
 
     def walk_bv_concat(self, formula, args):
-        if args[0].is_bv_constant() and args[1].is_bv_constant:
+        if args[0].is_bv_constant() and args[1].is_bv_constant():
             w0 = args[0].bv_width()
             w1 = args[1].bv_width()
             res = (2**w1) * args[0].bv_unsigned_value() + \
@@ -526,14 +526,14 @@ class Simplifier(walkers.DagWalker):
         return self.manager.BVConcat(*args)
 
     def walk_bv_lshl(self, formula, args):
-        if args[0].is_bv_constant() and args[1].is_bv_constant:
+        if args[0].is_bv_constant() and args[1].is_bv_constant():
             res = args[0].bv_unsigned_value() << args[1].bv_unsigned_value()
             w = args[0].bv_width()
             return self.manager.BV(res % (2 ** w), w)
         return self.manager.BVLShl(*args)
 
     def walk_bv_lshr(self, formula, args):
-        if args[0].is_bv_constant() and args[1].is_bv_constant:
+        if args[0].is_bv_constant() and args[1].is_bv_constant():
             res = args[0].bv_unsigned_value() >> args[1].bv_unsigned_value()
             w = args[0].bv_width()
             return self.manager.BV(res % (2 ** w), w)
diff --git a/pysmt/walkers/identitydag.py b/pysmt/walkers/identitydag.py
index 1fc1915..b422926 100644
--- a/pysmt/walkers/identitydag.py
+++ b/pysmt/walkers/identitydag.py
@@ -31,72 +31,135 @@ class IdentityDagWalker(DagWalker):
         DagWalker.__init__(self,
                            env=env,
                            invalidate_memoization=invalidate_memoization)
+        self.mgr = self.env.formula_manager
 
     def walk_symbol(self, formula, args):
-        return self.env.formula_manager.Symbol(formula.symbol_name(),
+        return self.mgr.Symbol(formula.symbol_name(),
                                                formula.symbol_type())
 
     def walk_real_constant(self, formula, args):
-        return self.env.formula_manager.Real(formula.constant_value())
+        return self.mgr.Real(formula.constant_value())
 
     def walk_int_constant(self, formula, args):
-        return self.env.formula_manager.Int(formula.constant_value())
+        return self.mgr.Int(formula.constant_value())
 
     def walk_bool_constant(self, formula, args):
-        return self.env.formula_manager.Bool(formula.constant_value())
+        return self.mgr.Bool(formula.constant_value())
 
     def walk_and(self, formula, args):
-        return self.env.formula_manager.And(args)
+        return self.mgr.And(args)
 
     def walk_or(self, formula, args):
-        return self.env.formula_manager.Or(args)
+        return self.mgr.Or(args)
 
     def walk_not(self, formula, args):
-        return self.env.formula_manager.Not(args[0])
+        return self.mgr.Not(*args)
 
     def walk_iff(self, formula, args):
-        return self.env.formula_manager.Iff(args[0], args[1])
+        return self.mgr.Iff(*args)
 
     def walk_implies(self, formula, args):
-        return self.env.formula_manager.Implies(args[0], args[1])
+        return self.mgr.Implies(*args)
 
     def walk_equals(self, formula, args):
-        return self.env.formula_manager.Equals(args[0], args[1])
+        return self.mgr.Equals(*args)
 
     def walk_ite(self, formula, args):
-        return self.env.formula_manager.Ite(args[0], args[1], args[2])
+        return self.mgr.Ite(*args)
 
     def walk_ge(self, formula, args):
-        return self.env.formula_manager.GE(args[0], args[1])
+        return self.mgr.GE(*args)
 
     def walk_le(self, formula, args):
-        return self.env.formula_manager.LE(args[0], args[1])
+        return self.mgr.LE(*args)
 
     def walk_gt(self, formula, args):
-        return self.env.formula_manager.GT(args[0], args[1])
+        return self.mgr.GT(*args)
 
     def walk_lt(self, formula, args):
-        return self.env.formula_manager.LT(args[0], args[1])
+        return self.mgr.LT(*args)
 
     def walk_forall(self, formula, args):
         qvars = [self.walk_symbol(v, None) for v in formula.quantifier_vars()]
-        return self.env.formula_manager.ForAll(qvars,args[0])
+        return self.mgr.ForAll(qvars, *args)
 
     def walk_exists(self, formula, args):
         qvars = [self.walk_symbol(v, None) for v in formula.quantifier_vars()]
-        return self.env.formula_manager.Exists(qvars,args[0])
+        return self.mgr.Exists(qvars, *args)
 
     def walk_plus(self, formula, args):
-        return self.env.formula_manager.Plus(args)
+        return self.mgr.Plus(args)
 
     def walk_times(self, formula, args):
-        return self.env.formula_manager.Times(args[0], args[1])
+        return self.mgr.Times(*args)
 
     def walk_minus(self, formula, args):
-        return self.env.formula_manager.Minus(args[0], args[1])
+        return self.mgr.Minus(*args)
 
     def walk_function(self, formula, args):
-        return self.env.formula_manager.Function(formula.function_name(), args)
+        return self.mgr.Function(formula.function_name(), args)
 
     def walk_toreal(self, formula, args):
-        return self.env.formula_manager.ToReal(args[0])
+        return self.mgr.ToReal(*args)
+
+    def walk_bv_constant(self, formula, args):
+        return self.mgr.BV(formula.constant_value(), formula.bv_width())
+
+    def walk_bv_and(self, formula, args):
+        return self.mgr.BVAnd(*args)
+
+    def walk_bv_not(self, formula, args):
+        return self.mgr.BVNot(*args)
+
+    def walk_bv_neg(self, formula, args):
+        return self.mgr.BVNeg(*args)
+
+    def walk_bv_or(self, formula, args):
+        return self.mgr.BVOr(*args)
+
+    def walk_bv_xor(self, formula, args):
+        return self.mgr.BVXor(*args)
+
+    def walk_bv_add(self, formula, args):
+        return self.mgr.BVAdd(*args)
+
+    def walk_bv_mul(self, formula, args):
+        return self.mgr.BVMul(*args)
+
+    def walk_bv_udiv(self, formula, args):
+        return self.mgr.BVUDiv(*args)
+
+    def walk_bv_urem(self, formula, args):
+        return self.mgr.BVURem(*args)
+
+    def walk_bv_ult(self, formula, args):
+        return self.mgr.BVULT(*args)
+
+    def walk_bv_ule(self, formula, args):
+        return self.mgr.BVULE(*args)
+
+    def walk_bv_extract(self, formula, args):
+        return self.mgr.BVExtract(args[0],
+                                  start=formula.bv_extract_start(),
+                                  end=formula.bv_extract_end())
+
+    def walk_bv_ror(self, formula, args):
+        return self.mgr.BVRor(args[0], formula.bv_rotation_step())
+
+    def walk_bv_rol(self, formula, args):
+        return self.mgr.BVRol(args[0], formula.bv_rotation_step())
+
+    def walk_bv_sext(self, formula, args):
+        return self.mgr.BVSExt(args[0], formula.bv_extend_step())
+
+    def walk_bv_zext(self, formula, args):
+        return self.mgr.BVZExt(args[0], formula.bv_extend_step())
+
+    def walk_bv_concat(self, formula, args):
+        return self.mgr.BVConcat(*args)
+
+    def walk_bv_lshl(self, formula, args):
+        return self.mgr.BVLShl(*args)
+
+    def walk_bv_lshr(self, formula, args):
+        return self.mgr.BVLShr(*args)


Test patch:
diff --git a/pysmt/test/test_walkers.py b/pysmt/test/test_walkers.py
index 22a96c7..6defb39 100644
--- a/pysmt/test/test_walkers.py
+++ b/pysmt/test/test_walkers.py
@@ -25,6 +25,7 @@ from pysmt.typing import INT, BOOL, REAL, FunctionType
 from pysmt.walkers import TreeWalker, DagWalker, IdentityDagWalker
 from pysmt.test import TestCase
 from pysmt.formula import FormulaManager
+from pysmt.test.examples import get_example_formulae
 
 from six.moves import xrange
 
@@ -100,7 +101,7 @@ class TestWalkers(TestCase):
         self.assertFalse(tree_walker.is_complete())
 
 
-    def test_identity_walker(self):
+    def test_identity_walker_simple(self):
 
         def walk_and_to_or(formula, args, **kwargs):
             return Or(args)
@@ -125,6 +126,11 @@ class TestWalkers(TestCase):
         result = walker.walk(alternation)
         self.assertEqual(result, expected)
 
+    def test_identity_dag_walker(self):
+        idw = IdentityDagWalker()
+        for (f, _, _, _) in get_example_formulae():
+            rebuilt = idw.walk(f)
+            self.assertTrue(rebuilt == f, "Rebuilt formula is not identical")
 
     def test_substitution_on_quantifiers(self):
         x, y = FreshSymbol(), FreshSymbol()