Repository: pysmt/pysmt
Pull request #353 (2016-10-10 20:07:55)

Tests for FNode
This increases the coverage of tests for FNode.

**Note**: This also changes the implementation of FNode.array_value_get, since the current implementation was incorrect.

marcogario: This depends on PR #351 

Patch:
diff --git a/pysmt/fnode.py b/pysmt/fnode.py
index 84ab00a..5faa3a8 100644
--- a/pysmt/fnode.py
+++ b/pysmt/fnode.py
@@ -578,32 +578,12 @@ class FNode(object):
     def array_value_get(self, index):
         """Returns the value of this Array Value at the given index. The
         index must be a constant of the correct type.
-
-        This function is equivalent (but possibly faster) than the
-        following code::
-
-          m = self.array_value_assigned_values_map()
-          try:
-              return m[index]
-          except KeyError:
-              return self.array_value_default()
-
         """
-        assert index.is_constant()
-        args = self.args()
-        start = 0
-        end = (len(args) - 1) // 2
-        while end - start > 0:
-            pivot = (end - start) // 2
-            i = args[2 * pivot + 1]
-            if id(i) == id(index):
-                return args[2 * pivot + 2]
-            elif id(i) < id(index):
-                end = pivot
-            else:
-                start = pivot + 1
-        return self.array_value_default()
-
+        m = self.array_value_assigned_values_map()
+        try:
+            return m[index]
+        except KeyError:
+            return self.array_value_default()
 
     def array_value_assigned_values_map(self):
         args = self.args()
@@ -669,8 +649,14 @@ class FNode(object):
     def Equals(self, right):
         return self._apply_infix(right, _mgr().Equals)
 
-    def Ite(self, right):
-        return self._apply_infix(right, _mgr().Ite)
+    def Ite(self, then_, else_):
+        if _env().enable_infix_notation:
+            if isinstance(then_, FNode) and isinstance(else_, FNode):
+                return _mgr().Ite(self, then_, else_)
+            else:
+                raise Exception("Cannot infix ITE with implicit argument types.")
+        else:
+            raise Exception("Cannot use infix notation")
 
     def And(self, right):
         return self._apply_infix(right, _mgr().And)
@@ -807,21 +793,6 @@ class FNode(object):
             return _mgr().BVNot(self)
         return _mgr().Not(self)
 
-    def __int__(self):
-        if self.is_int_constant():
-            return self.constant_value()
-        raise NotImplementedError("Cannot convert `%s` to integer" % str(self))
-
-    def __long__(self):
-        if self.is_int_constant():
-            return self.constant_value()
-        raise NotImplementedError("Cannot convert `%s` to integer" % str(self))
-
-    def __float__(self):
-        if self.is_int_constant() or self.is_real_constant():
-            return float(self.constant_value())
-        raise NotImplementedError("Cannot convert `%s` to float" % str(self))
-
     def __getitem__(self, idx):
         if not _env().enable_infix_notation:
             raise Exception("Cannot use infix notation")
diff --git a/pysmt/formula.py b/pysmt/formula.py
index 59d98ec..518df39 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -800,6 +800,8 @@ class FormulaManager(object):
     def BVAShr(self, left, right):
         """Returns the RIGHT arithmetic rotation of the left BV by the number
         of steps specified by the right BV."""
+        if is_python_integer(right):
+            right = self.BV(right, left.bv_width())
         return self.create_node(node_type=op.BV_ASHR,
                                 args=(left, right),
                                 payload=(left.bv_width(),))


Test patch:
diff --git a/pysmt/test/test_array.py b/pysmt/test/test_array.py
index bb1f7c7..81fe0e0 100644
--- a/pysmt/test/test_array.py
+++ b/pysmt/test/test_array.py
@@ -103,6 +103,39 @@ class TestArray(TestCase):
         select_ = Select(store_, Int(100))
         self.assertTrue(store_.is_array_op())
         self.assertTrue(select_.is_array_op())
+        self.assertTrue(store_.is_store())
+        self.assertTrue(select_.is_select())
+        self.assertFalse(select_.is_store())
+        self.assertFalse(store_.is_select())
+
+    def test_array_value_get(self):
+        ax = Array(REAL, Real(0),
+                   {Real(1): Real(2),
+                    Real(2): Real(3),
+                    Real(3): Real(4),
+                    Real(4): Real(5),
+                })
+        self.assertEqual(ax.array_value_get(Real(1)), Real(2))
+        self.assertEqual(ax.array_value_get(Real(2)), Real(3))
+        self.assertEqual(ax.array_value_get(Real(3)), Real(4))
+        self.assertEqual(ax.array_value_get(Real(4)), Real(5))
+        self.assertEqual(ax.array_value_get(Real(-1)), Real(0))
+        self.assertEqual(ax.array_value_get(Real(5)), Real(0))
+
+    def test_array_value_is_constant(self):
+        r = Symbol("r", REAL)
+        ax1 = Array(REAL, Real(0), {Real(1): r})
+        ax2 = Array(REAL, r, {Real(1): Real(2)})
+        ax3 = Array(REAL, Real(0), {Real(1): Real(2)})
+        self.assertFalse(ax1.is_constant())
+        self.assertFalse(ax2.is_constant())
+        self.assertTrue(ax3.is_constant())
+
+        with self.assertRaises(ValueError):
+            self.assertTrue(ax3.is_constant(_type=REAL))
+
+        with self.assertRaises(ValueError):
+            self.assertTrue(ax3.is_constant(value=Real(2)))
 
 
 if __name__ == "__main__":
diff --git a/pysmt/test/test_bv.py b/pysmt/test/test_bv.py
index 7c4c31e..434ea4b 100644
--- a/pysmt/test/test_bv.py
+++ b/pysmt/test/test_bv.py
@@ -68,6 +68,7 @@ class TestBV(TestCase):
 
         not_zero32 = mgr.BVNot(zero)
         not_b128 = mgr.BVNot(b128)
+        self.assertTrue(not_b128.is_bv_not())
 
         f1 = Equals(not_zero32, b32)
         f2 = Equals(not_b128, big)
@@ -75,8 +76,11 @@ class TestBV(TestCase):
         self.assertTrue(is_sat(f2, logic=QF_BV))
 
         zero_and_one = mgr.BVAnd(zero, one)
+        self.assertTrue(zero_and_one.is_bv_and())
         zero_or_one = mgr.BVOr(zero, one)
+        self.assertTrue(zero_or_one.is_bv_or())
         zero_xor_one = mgr.BVXor(zero, one)
+        self.assertTrue(zero_xor_one.is_bv_xor())
 
         zero_xor_one.simplify()
         self.assertTrue(zero_xor_one.is_bv_op())
@@ -104,6 +108,8 @@ class TestBV(TestCase):
         zero_one_64 = mgr.BVConcat(zero, one)
         one_zero_64 = mgr.BVConcat(one, zero)
         one_one_64  = mgr.BVConcat(one, one)
+        self.assertTrue(one_one_64.is_bv_concat())
+        self.assertFalse(one_one_64.is_bv_and())
 
         self.assertTrue(zero_one_64.bv_width() == 64)
         f1 = Equals(mgr.BVXor(one_zero_64, zero_one_64),
@@ -117,15 +123,20 @@ class TestBV(TestCase):
         self.assertTrue(is_valid(Equals(extraction, zero)))
 
         ult = mgr.BVULT(zero, one)
+        self.assertTrue(ult.is_bv_ult())
         neg = mgr.BVNeg(one)
+        self.assertTrue(neg.is_bv_neg())
         self.assertTrue(is_valid(ult, logic=QF_BV), ult)
         test_eq = Equals(neg, one)
         self.assertTrue(is_unsat(test_eq, logic=QF_BV))
 
         f = zero
         addition = mgr.BVAdd(f, one)
+        self.assertTrue(addition.is_bv_add())
         multiplication = mgr.BVMul(f, one)
+        self.assertTrue(multiplication.is_bv_mul())
         udiv = mgr.BVUDiv(f, one)
+        self.assertTrue(udiv.is_bv_udiv())
 
         self.assertTrue(is_valid(Equals(addition, one), logic=QF_BV), addition)
         self.assertTrue(is_valid(Equals(multiplication, zero), logic=QF_BV), multiplication)
@@ -133,9 +144,12 @@ class TestBV(TestCase):
 
         three = mgr.BV(3, 32)
         two = mgr.BV(2, 32)
+        self.assertEqual(3, three.bv2nat())
 
         reminder = mgr.BVURem(three, two)
+        self.assertTrue(reminder.is_bv_urem())
         shift_l_a = mgr.BVLShl(one, one)
+        self.assertTrue(shift_l_a.is_bv_lshl())
         shift_l_b = mgr.BVLShl(one, 1)
 
         self.assertTrue(is_valid(Equals(reminder, one)), reminder)
@@ -143,16 +157,26 @@ class TestBV(TestCase):
         self.assertTrue(is_valid(Equals(shift_l_a, two)))
 
         shift_r_a = mgr.BVLShr(one, one)
+        self.assertTrue(shift_r_a.is_bv_lshr())
         shift_r_b = mgr.BVLShr(one, 1)
         self.assertEqual(shift_r_a, shift_r_b)
         self.assertTrue(is_valid(Equals(shift_r_a, zero)))
 
+        ashift_r_a = mgr.BVAShr(one, one)
+        ashift_r_b = mgr.BVAShr(one, 1)
+        self.assertEqual(ashift_r_a, ashift_r_b)
+        self.assertTrue(ashift_r_a.is_bv_ashr())
+
         rotate_l = mgr.BVRol(one, 3)
+        self.assertTrue(rotate_l.is_bv_rol())
         rotate_r = mgr.BVRor(rotate_l, 3)
+        self.assertTrue(rotate_r.is_bv_ror())
         self.assertTrue(is_valid(Equals(one, rotate_r)))
 
         zero_ext = mgr.BVZExt(one, 64)
+        self.assertTrue(zero_ext.is_bv_zext())
         signed_ext = mgr.BVSExt(one, 64)
+        self.assertTrue(signed_ext.is_bv_sext())
         signed_ext2 = mgr.BVSExt(mgr.BVNeg(one), 64)
 
         self.assertNotEqual(signed_ext2, signed_ext)
@@ -207,7 +231,22 @@ class TestBV(TestCase):
         # SBV should behave as BV for positive numbers
         self.assertEqual(mgr.SBV(10, 16), mgr.BV(10, 16))
 
-        return
+        # Additional is_bv_* tests
+        f = mgr.BVSub(one, one)
+        self.assertTrue(f.is_bv_sub())
+
+        f = mgr.BVSLT(one, one)
+        self.assertTrue(f.is_bv_slt())
+        f = mgr.BVSLE(one, one)
+        self.assertTrue(f.is_bv_sle())
+        f = mgr.BVComp(one, one)
+        self.assertTrue(f.is_bv_comp())
+        f = mgr.BVSDiv(one, one)
+        self.assertTrue(f.is_bv_sdiv())
+        f = mgr.BVSRem(one, one)
+        self.assertTrue(f.is_bv_srem())
+        f = mgr.BVULE(one, one)
+        self.assertTrue(f.is_bv_ule())
 
     @skipIfNoSolverForLogic(QF_BV)
     def test_bv_div_by_zero(self):
@@ -256,6 +295,17 @@ class TestBV(TestCase):
                                        bvx))
         self.assertValid(fsrem)
 
+    def test_is_bv_constant(self):
+        mgr = self.env.formula_manager
+        bvconst = mgr.BV(4, 8)
+        self.assertTrue(bvconst.is_bv_constant())
+        self.assertTrue(bvconst.is_bv_constant(value=4))
+        self.assertTrue(bvconst.is_bv_constant(width=8))
+        self.assertTrue(bvconst.is_bv_constant(value=4, width=8))
+        self.assertFalse(bvconst.is_bv_constant(value=4, width=9))
+        self.assertFalse(bvconst.is_bv_constant(value=5, width=8))
+        self.assertFalse(bvconst.is_bv_constant(3,9))
+        self.assertFalse(bvconst.is_bv_constant(3))
 
 if __name__ == "__main__":
     main()
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index 4fcd948..be9f5a1 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -21,7 +21,7 @@ from six.moves import xrange
 import pysmt
 from pysmt.typing import BOOL, REAL, INT, FunctionType, BV8, BVType
 from pysmt.shortcuts import Symbol, is_sat, Not, Implies, GT, Plus, Int, Real
-from pysmt.shortcuts import Minus, Times, Xor, And, Or, TRUE
+from pysmt.shortcuts import Minus, Times, Xor, And, Or, TRUE, Iff, FALSE, Ite
 from pysmt.shortcuts import get_env
 from pysmt.environment import Environment
 from pysmt.test import TestCase, skipIfNoSolverForLogic, main
@@ -128,7 +128,6 @@ class TestFormulaManager(TestCase):
         with self.assertRaises(AssertionError):
             s.function_name()
 
-
     def test_and_node(self):
         n = self.mgr.And(self.x, self.y)
         self.assertIsNotNone(n)
@@ -503,6 +502,16 @@ class TestFormulaManager(TestCase):
         self.assertEqual(a,b)
         self.assertEqual(b,c)
 
+        # Constant's Type
+        b = self.mgr.Bool(True)
+        i = self.mgr.Int(1)
+        r = self.mgr.Real(1)
+        bv8 = self.mgr.BV(1, 8)
+        self.assertEqual(i.constant_type(), INT)
+        self.assertEqual(r.constant_type(), REAL)
+        self.assertEqual(bv8.constant_type(), BV8)
+        self.assertEqual(b.constant_type(), BOOL)
+
     def test_bconstant(self):
         n = self.mgr.Bool(True)
         m = self.mgr.Bool(False)
@@ -559,7 +568,6 @@ class TestFormulaManager(TestCase):
         self.assertEqual(f1,f2)
         self.assertEqual(f2,f3)
 
-
     @skipIfNoSolverForLogic(QF_BOOL)
     def test_exactly_one_is_sat(self):
         symbols = [ self.mgr.Symbol("s%d"%i, BOOL) for i in range(5) ]
@@ -570,7 +578,6 @@ class TestFormulaManager(TestCase):
         self.assertFalse(is_sat(test_zero, logic=QF_BOOL),
                          "ExactlyOne should not allow all symbols to be False")
 
-
     def test_at_most_one(self):
         symbols = [ self.mgr.Symbol("s%d"%i, BOOL) for i in range(5) ]
         c = self.mgr.AtMostOne(symbols)
@@ -618,7 +625,6 @@ class TestFormulaManager(TestCase):
                          "AllDifferent should be tautological for a set " \
                          "of different values")
 
-
     def test_min(self):
         min1 = self.mgr.Min(self.p, Plus(self.q, self.mgr.Int(1)))
         self.assertIsNotNone(min1)
@@ -634,7 +640,6 @@ class TestFormulaManager(TestCase):
         self.assertEqual(min_real.simplify(), self.mgr.Real(1),
                          "The minimum of 1.0, 2.0 and 3.0 should be 1.0")
 
-
     def test_max(self):
         max1 = self.mgr.Max(self.p, Plus(self.q, self.mgr.Int(1)))
         self.assertIsNotNone(max1)
@@ -650,8 +655,6 @@ class TestFormulaManager(TestCase):
         self.assertEqual(max_real.simplify(), self.mgr.Real(3),
                          "The maximum of 1.0, 2.0 and 3.0 should be 3.0")
 
-
-
     def test_pickling(self):
         import pickle
 
@@ -699,12 +702,21 @@ class TestFormulaManager(TestCase):
 
         with self.assertRaises(Exception):
             x.Implies(y)
+        with self.assertRaises(Exception):
+            ~x
+        with self.assertRaises(Exception):
+            x[1]
+        with self.assertRaises(Exception):
+            x.Ite(x,y)
+
         get_env().enable_infix_notation = True
         self.assertEqual(Implies(x,y), x.Implies(y))
 
         self.assertEqual(p + p, Plus(p,p))
         self.assertEqual(p > p, GT(p,p))
-        get_env().enable_infix_notation = False
+
+        with self.assertRaises(NotImplementedError):
+            x[1]
 
     def test_infix_extended(self):
         p, r, x, y = self.p, self.r, self.x, self.y
@@ -743,6 +755,16 @@ class TestFormulaManager(TestCase):
         self.assertEqual(And(x, TRUE()), x & True)
         self.assertEqual(And(x, TRUE()), True & x)
 
+        self.assertEqual(Iff(x, y), x.Iff(y))
+        self.assertEqual(And(x,y), x.And(y))
+        self.assertEqual(Or(x,y), x.Or(y))
+
+        self.assertEqual(Ite(x, TRUE(), FALSE()), x.Ite(TRUE(), FALSE()))
+        with self.assertRaises(Exception):
+            x.Ite(1,2)
+
+        self.assertEqual(6 - r, Plus(Times(r, Real(-1)), Real(6)))
+
         # BVs
 
         # BV_CONSTANT: We use directly python numbers
@@ -820,7 +842,6 @@ class TestFormulaManager(TestCase):
         self.assertEqual(const1 * bv8,
                          self.mgr.BVMul(bv8, const1_8))
 
-
         # BV_NOT:
         # !!!WARNING!!! Cannot be applied to python constants!!
         # This results in a negative number
@@ -939,8 +960,6 @@ class TestFormulaManager(TestCase):
         self.assertEqual(self.mgr.BVRepeat(bv8, count=5),
                          bv8.BVRepeat(5))
 
-        # Reset Env
-        get_env().enable_infix_notation = False
 
     def test_toReal(self):
         f = self.mgr.Equals(self.rconst, self.mgr.ToReal(self.p))
@@ -1066,6 +1085,13 @@ class TestFormulaManager(TestCase):
             c_mpz = self.mgr.Int(v_mpz)
             self.assertIs(c_base, c_mpz)
 
+    def test_node_id(self):
+        x = Symbol("x")
+        y = Symbol("y")
+        xx = Symbol("x")
+        self.assertEqual(x.node_id(), xx.node_id())
+        self.assertNotEqual(x.node_id(), y.node_id())
+
 
 class TestShortcuts(TestCase):
 
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index 1d44e55..0419672 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -62,7 +62,6 @@ class TestRegressions(TestCase):
         self.assertValid(Equals(p1, p2), solver_name='z3')
         self.assertValid(Equals(p1, p2), solver_name='msat')
 
-
     def test_substitute_memoization(self):
         a = Symbol("A", BOOL)
         b = Symbol("B", BOOL)
@@ -412,6 +411,12 @@ class TestRegressions(TestCase):
     def test_array_initialization_printing(self):
         self.assertEqual(str(Array(INT, Int(0), {Int(1):Int(2)})), "Array{Int, Int}(0)[1 := 2]")
 
+    def test_git_version(self):
+        from pysmt import git_version
+        v = git_version()
+        self.assertIsNotNone(v)
+        parts = v.split(b"-")
+        self.assertTrue(len(parts) , 4)
 
 
 if __name__ == "__main__":