Repository: pysmt/pysmt
Pull request #341 (2016-10-05 13:35:12)

Fix array values map bug
This PR is the extension of #340.

There is a bug in  ```FNode.array_value_assigned_values_map``` that returns the wromg map of initial values for an array. This PR fixes it.

Thanks to @daniel-rs for noticing the problem


Patch:
diff --git a/pysmt/factory.py b/pysmt/factory.py
index e7a3f00..f9e6878 100644
--- a/pysmt/factory.py
+++ b/pysmt/factory.py
@@ -511,6 +511,7 @@ class Factory(object):
                         if solver.get_value(a).is_true():
                             res.append(a)
                         else:
+                            assert solver.get_value(a).is_false()
                             res.append(mgr.Not(a))
                 return mgr.And(res)
 
diff --git a/pysmt/fnode.py b/pysmt/fnode.py
index 64fc763..84ab00a 100644
--- a/pysmt/fnode.py
+++ b/pysmt/fnode.py
@@ -576,28 +576,38 @@ class FNode(object):
         return self._content.payload
 
     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()
-        idx = index.simplify()
         args = self.args()
-        s = 0
-        e = (len(args) - 1) / 2
-        while e - s > 0:
-            p = (e - s) / 2
-            i = args[2 * p + 1]
-            if i == idx:
-                return args[i+1]
-            elif i < idx:
-                s = p
+        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:
-                e = p
+                start = pivot + 1
         return self.array_value_default()
 
+
     def array_value_assigned_values_map(self):
-        res = {}
         args = self.args()
-        for i,c in enumerate(args[1::2]):
-            res[c] = args[i+1]
-        return res
+        return dict(zip(args[1::2], args[2::2]))
 
     def array_value_default(self):
         return self.args()[0]
diff --git a/pysmt/printers.py b/pysmt/printers.py
index b6ca797..cf5ae4a 100644
--- a/pysmt/printers.py
+++ b/pysmt/printers.py
@@ -223,11 +223,13 @@ class HRPrinter(TreeWalker):
         yield formula.array_value_default()
         self.write(")")
         assign = formula.array_value_assigned_values_map()
-        for k, v in iteritems(assign):
+        # We sort the array value assigments in lexicographic order
+        # for deterministic printing
+        for k in sorted(assign, key=str):
             self.write("[")
             yield k
             self.write(" := ")
-            yield v
+            yield assign[k]
             self.write("]")
 
 
diff --git a/pysmt/simplifier.py b/pysmt/simplifier.py
index 3248c7f..22adc0a 100644
--- a/pysmt/simplifier.py
+++ b/pysmt/simplifier.py
@@ -642,9 +642,7 @@ class Simplifier(pysmt.walkers.DagWalker):
         return self.manager.Store(a, i, v)
 
     def walk_array_value(self, formula, args, **kwargs):
-        assign = {}
-        for i,c in enumerate(args[1::2]):
-            assign[c] = args[i+1]
+        assign = dict(zip(args[1::2], args[2::2]))
         return self.manager.Array(formula.array_value_index_type(),
                                   args[0],
                                   assign)
diff --git a/pysmt/smtlib/printers.py b/pysmt/smtlib/printers.py
index 116e85f..867f80a 100644
--- a/pysmt/smtlib/printers.py
+++ b/pysmt/smtlib/printers.py
@@ -186,7 +186,7 @@ class SmtPrinter(TreeWalker):
         yield formula.array_value_default()
         self.write(")")
 
-        for k in sorted(assign):
+        for k in sorted(assign, key=str):
             self.write(" ")
             yield k
             self.write(" ")
diff --git a/pysmt/solvers/msat.py b/pysmt/solvers/msat.py
index b2b1ab0..2dc9005 100644
--- a/pysmt/solvers/msat.py
+++ b/pysmt/solvers/msat.py
@@ -520,15 +520,12 @@ class MSatConverter(Converter, DagWalker):
 
         elif mathsat.msat_term_is_array_read(self.msat_env(), term):
             t1 = self.env.stc.get_type(args[0])
-            t2 = self.env.stc.get_type(args[1])
             t = t1.elem_type
-            res = types.FunctionType(t, [t1, t2])
+            res = types.FunctionType(t, [t1, t1.index_type])
 
         elif mathsat.msat_term_is_array_write(self.msat_env(), term):
-            t1 = self.env.stc.get_type(args[0])
-            t2 = self.env.stc.get_type(args[1])
-            t3 = self.env.stc.get_type(args[2])
-            res = types.FunctionType(t1, [t1, t2, t3])
+            at = self.env.stc.get_type(args[0])
+            res = types.FunctionType(at, [at, at.index_type, at.elem_type])
 
         elif mathsat.msat_term_is_array_const(self.msat_env(), term):
             ty = mathsat.msat_term_get_type(term)
diff --git a/pysmt/solvers/z3.py b/pysmt/solvers/z3.py
index 4b66b64..a317014 100644
--- a/pysmt/solvers/z3.py
+++ b/pysmt/solvers/z3.py
@@ -245,7 +245,10 @@ class Z3Solver(IncrementalTrackingSolver, UnsatCoreSolver,
 
         titem = self.converter.convert(item)
         z3_res = self.z3.model().eval(titem, model_completion=True)
-        return self.converter.back(z3_res, self.z3.model())
+        res = self.converter.back(z3_res, self.z3.model())
+        if not res.is_constant():
+            return res.simplify()
+        return res
 
     def _exit(self):
         del self.z3
diff --git a/pysmt/walkers/identitydag.py b/pysmt/walkers/identitydag.py
index d7d1e0e..ca84bcb 100644
--- a/pysmt/walkers/identitydag.py
+++ b/pysmt/walkers/identitydag.py
@@ -192,9 +192,7 @@ class IdentityDagWalker(DagWalker):
         return self.mgr.Store(args[0], args[1], args[2])
 
     def walk_array_value(self, formula, args, **kwargs):
-        assign = {}
-        for i,c in enumerate(args[1::2]):
-            assign[c] = args[i+1]
+        assign = dict(zip(args[1::2], args[2::2]))
         return self.mgr.Array(formula.array_value_index_type(),
                               args[0],
                               assign)


Test patch:
diff --git a/pysmt/test/examples.py b/pysmt/test/examples.py
index ca188d1..748d133 100644
--- a/pysmt/test/examples.py
+++ b/pysmt/test/examples.py
@@ -61,6 +61,7 @@ def get_full_example_formulae(environment=None):
         r = Symbol("r", REAL)
         s = Symbol("s", REAL)
         aii = Symbol("aii", ARRAY_INT_INT)
+        ari = Symbol("ari", ArrayType(REAL, INT))
         arb = Symbol("arb", ArrayType(REAL, BV8))
         abb = Symbol("abb", ArrayType(BV8, BV8))
         nested_a = Symbol("a_arb_aii", ArrayType(ArrayType(REAL, BV8),
@@ -323,7 +324,7 @@ def get_full_example_formulae(environment=None):
                     logic=pysmt.logics.QF_BV
                 ),
 
-            Example(hr="((((1_32 + (- ...)) << 1_32) >> 1_32) = 1_32)",
+            Example(hr="((((1_32 + (- 1_32)) << 1_32) >> 1_32) = 1_32)",
                     expr=Equals(BVLShr(BVLShl(BVAdd(BVOne(32),
                                                     BVNeg(BVOne(32))),
                                               1), 1),
@@ -564,7 +565,7 @@ def get_full_example_formulae(environment=None):
                     logic=pysmt.logics.QF_UFLIRA
                 ),
 
-            Example(hr="(((p - 3) = q) -> ((p < ih(r, (... + ...))) | (ih(r, p) <= p)))",
+            Example(hr="(((p - 3) = q) -> ((p < ih(r, (q + 3))) | (ih(r, p) <= p)))",
                     expr=Implies(Equals(Minus(p, Int(3)), q),
                                  Or(GT(Function(ih, (r, Plus(q, Int(3)))), p),
                                     LE(Function(ih, (r, p)), p))),
@@ -573,7 +574,7 @@ def get_full_example_formulae(environment=None):
                     logic=pysmt.logics.QF_UFLIRA
                 ),
 
-            Example(hr="(((ToReal((... - ...)) = r) & (ToReal(q) = r)) -> ((p < ih(ToReal(...), (... + ...))) | (ih(r, p) <= p)))",
+            Example(hr="(((ToReal((p - 3)) = r) & (ToReal(q) = r)) -> ((p < ih(ToReal((p - 3)), (q + 3))) | (ih(r, p) <= p)))",
                     expr=Implies(And(Equals(ToReal(Minus(p, Int(3))), r),
                                      Equals(ToReal(q), r)),
                                  Or(GT(Function(ih, (ToReal(Minus(p, Int(3))),
@@ -584,7 +585,7 @@ def get_full_example_formulae(environment=None):
                     logic=pysmt.logics.QF_UFLIRA
                 ),
 
-            Example(hr="(! (((ToReal(...) = r) & (ToReal(...) = r)) -> ((p < ...(..., ...)) | (...(..., ...) <= p))))",
+            Example(hr="(! (((ToReal((p - 3)) = r) & (ToReal(q) = r)) -> ((p < ih(ToReal((p - 3)), (q + 3))) | (ih(r, p) <= p))))",
                     expr=Not(Implies(And(Equals(ToReal(Minus(p, Int(3))), r),
                                          Equals(ToReal(q), r)),
                                      Or(GT(Function(ih, (ToReal(Minus(p, Int(3))),
@@ -632,6 +633,46 @@ def get_full_example_formulae(environment=None):
                     logic=pysmt.logics.get_logic_by_name("QF_ALIA*")
                 ),
 
+            Example(hr="((Array{Int, Int}(0)[1 := 3] = aii) & (aii[1] = 3))",
+                    expr=And(Equals(Array(INT, Int(0), {Int(1) : Int(3)}), aii), Equals(Select(aii, Int(1)), Int(3))),
+                    is_valid=False,
+                    is_sat=True,
+                    logic=pysmt.logics.get_logic_by_name("QF_ALIA*")
+                ),
+
+            Example(hr="((Array{Real, Int}(10) = ari) & (ari[6/5] = 0))",
+                    expr=And(Equals(Array(REAL, Int(10)), ari), Equals(Select(ari, Real((6, 5))), Int(0))),
+                    is_valid=False,
+                    is_sat=False,
+                    logic=pysmt.logics.get_logic_by_name("QF_AUFBVLIRA*")
+                ),
+
+            Example(hr="((Array{Real, Int}(0)[1.0 := 10][2.0 := 20][3.0 := 30][4.0 := 40] = ari) & (! ((ari[0.0] = 0) & (ari[1.0] = 10) & (ari[2.0] = 20) & (ari[3.0] = 30) & (ari[4.0] = 40))))",
+                    expr=And(Equals(Array(REAL, Int(0), {Real(1) : Int(10), Real(2) : Int(20), Real(3) : Int(30), Real(4) : Int(40)}), ari),
+                             Not(And(Equals(Select(ari, Real(0)), Int(0)),
+                                     Equals(Select(ari, Real(1)), Int(10)),
+                                     Equals(Select(ari, Real(2)), Int(20)),
+                                     Equals(Select(ari, Real(3)), Int(30)),
+                                     Equals(Select(ari, Real(4)), Int(40))))),
+                    is_valid=False,
+                    is_sat=False,
+                    logic=pysmt.logics.get_logic_by_name("QF_AUFBVLIRA*")
+                ),
+
+            Example(hr="((Array{Real, Int}(0)[1.0 := 10][2.0 := 20][3.0 := 30][4.0 := 40][5.0 := 50] = ari) & (! ((ari[0.0] = 0) & (ari[1.0] = 10) & (ari[2.0] = 20) & (ari[3.0] = 30) & (ari[4.0] = 40) & (ari[5.0] = 50))))",
+                    expr=And(Equals(Array(REAL, Int(0), {Real(1) : Int(10), Real(2) : Int(20), Real(3) : Int(30), Real(4) : Int(40), Real(5) : Int(50)}), ari),
+                             Not(And(Equals(Select(ari, Real(0)), Int(0)),
+                                     Equals(Select(ari, Real(1)), Int(10)),
+                                     Equals(Select(ari, Real(2)), Int(20)),
+                                     Equals(Select(ari, Real(3)), Int(30)),
+                                     Equals(Select(ari, Real(4)), Int(40)),
+                                     Equals(Select(ari, Real(5)), Int(50))))),
+                    is_valid=False,
+                    is_sat=False,
+                    logic=pysmt.logics.get_logic_by_name("QF_AUFBVLIRA*")
+                ),
+
+
             Example(hr="((a_arb_aii = Array{Array{Real, BV{8}}, Array{Int, Int}}(Array{Int, Int}(7))) -> (a_arb_aii[arb][42] = 7))",
                     expr=Implies(Equals(nested_a, Array(ArrayType(REAL, BV8),
                                                         Array(INT, Int(7)))),
diff --git a/pysmt/test/test_printing.py b/pysmt/test/test_printing.py
index d39fe8e..fefb812 100644
--- a/pysmt/test/test_printing.py
+++ b/pysmt/test/test_printing.py
@@ -170,8 +170,9 @@ class TestPrinting(TestCase):
 
     def test_examples(self):
         for s, f, logic in get_str_example_formulae(environment=None):
-            self.assertTrue(len(str(f)) >= 1, str(f))
-            self.assertEqual(str(f), s)
+            str_f = f.serialize()
+            self.assertTrue(len(str_f) >= 1, str_f)
+            self.assertEqual(str_f, s)
 
     def test_smart_serialize(self):
         x, y = Symbol("x"), Symbol("y")
diff --git a/pysmt/test/test_regressions.py b/pysmt/test/test_regressions.py
index d74752f..1d44e55 100644
--- a/pysmt/test/test_regressions.py
+++ b/pysmt/test/test_regressions.py
@@ -23,7 +23,7 @@ import pysmt.smtlib.commands as smtcmd
 from pysmt.shortcuts import (Real, Plus, Symbol, Equals, And, Bool, Or,
                              Div, LT, LE, Int, ToReal, Iff, Exists, Times, FALSE,
                              BVLShr, BVLShl, BVAShr, BV, BVAdd, BVULT, BVMul,
-                             Select)
+                             Select, Array)
 from pysmt.shortcuts import Solver, get_env, qelim, get_model, TRUE, ExactlyOne
 from pysmt.typing import REAL, BOOL, INT, BVType, FunctionType, ArrayType
 from pysmt.test import (TestCase, skipIfSolverNotAvailable, skipIfNoSolverForLogic,
@@ -409,6 +409,9 @@ class TestRegressions(TestCase):
             fp = solver.converter.back(z3_f)
             self.assertValid(Iff(f, fp), (f, fp))
 
+    def test_array_initialization_printing(self):
+        self.assertEqual(str(Array(INT, Int(0), {Int(1):Int(2)})), "Array{Int, Int}(0)[1 := 2]")
+
 
 
 if __name__ == "__main__":
diff --git a/pysmt/test/test_solving.py b/pysmt/test/test_solving.py
index 0891b56..662d03d 100644
--- a/pysmt/test/test_solving.py
+++ b/pysmt/test/test_solving.py
@@ -317,7 +317,7 @@ class TestBasic(TestCase):
                     try:
                         f_i = get_implicant(f, logic=logic, solver_name=sname)
                         if satisfiability:
-                            self.assertValid(Implies(f_i, f), logic=logic, msg=f)
+                            self.assertValid(Implies(f_i, f), logic=logic, msg=(f_i, f))
                         else:
                             self.assertIsNone(f_i)
                     except ConvertExpressionError as ex: