Update on Z3 solver use

pyState/Assign.py

@@ -39,7 +39,7 @@ def _handleAssignNum(target,value):
 
     for x2 in x:
 
-        parent = state.objectManager.getParent(x2)
+        parent = x2.state.objectManager.getParent(x2)
         index = parent.index(x2)
         parent[index] = value
 

pyState/BinOp.py

@@ -38,6 +38,7 @@ def _handleNum(state,left,right,op):
         ret = leftZ3Object / rightZ3Object
 
     elif type(op) == ast.Mod:
+        print(type(leftZ3Object),type(rightZ3Object))
         ret = leftZ3Object % rightZ3Object
 
     elif type(op) == ast.BitXor:

pyState/__init__.py

@@ -207,7 +207,8 @@ def __init__(self,path=None,solver=None,ctx=None,functions=None,simFunctions=Non
         self.path = [] if path is None else path
         self.ctx = 0 if ctx is None else ctx
         self.objectManager = objectManager if objectManager is not None else ObjectManager(state=self)
-        self.solver = z3.Solver() if solver is None else solver
+        #self.solver = z3.Solver() if solver is None else solver
+        self.solver = z3.Then("simplify","solve-eqs","smt").solver() if solver is None else solver
         self.functions = {} if functions is None else functions
         self.simFunctions = {} if simFunctions is None else simFunctions
         self.retVar = self.getVar('ret',ctx=1,varType=Int) if retVar is None else retVar
@@ -1207,7 +1208,8 @@ def any_n_real(self,var,n,ctx=None):
                 break
 
             out.append(myInt)
-            s.addConstraint(varZ3Object != myInt)
+            #s.addConstraint(varZ3Object != myInt)
+            s.addConstraint(varZ3Object != s.solver.model().eval(varZ3Object))
 
         return out
 
@@ -1437,11 +1439,15 @@ def any_real(self,var,ctx=None):
             return None
 
         # Check the type of the value
-        if type(value) not in [z3.IntNumRef,z3.RatNumRef]:
+        if type(value) not in [z3.IntNumRef,z3.RatNumRef,z3.AlgebraicNumRef]:
             err = "any_real: var '{0}' not of type int or real, of type '{1}'".format(var,type(value))
             logger.error(err)
             raise Exception(err) 
 
+        if type(value) is z3.AlgebraicNumRef:
+            # Defaulting to precision of 10 for now
+            return float(value.as_decimal(10).replace('?',''))
+
         # Made it! Return it as a real/float
         return float(eval(value.as_string()))
 
@@ -1453,7 +1459,8 @@ def copy(self):
         """
 
         # Copy the solver state
-        solverCopy = z3.Solver()
+        #solverCopy = z3.Solver()
+        solverCopy = z3.Then("simplify","solve-eqs","smt").solver()
         solverCopy.add(self.solver.assertions())
 
         newState = State(

pyState/functions/pyState/Real.py

@@ -1,6 +1,7 @@
 import z3
 import ast
 from pyObjectManager.Real import Real
+import pyState.z3Helpers
 
 def handle(state,call,value=None,ctx=None):
     """
@@ -11,16 +12,23 @@ def handle(state,call,value=None,ctx=None):
 
     myReal = state.resolveObject(ast.Name('tempReal',0),ctx=ctx,varType=Real)
 
-    ret = myReal
+    ret = []
+
+    for r in myReal:
 
-    if value is not None:
-        ret = []
-        for r in myReal:
+        if value is not None:
             state = r.state
             value = state.resolveObject(value,ctx=ctx)
+
             for v in value:
-                r.setTo(v)
-                ret.append(r.copy())
+                realObj,valueObj = pyState.z3Helpers.z3_matchLeftAndRight(r,v,ast.Add)
+                #r.setTo(v)
                 r.increment()
+                state.addConstraint(r.getZ3Object() == valueObj)
+                ret.append(r.copy())
+
+        else:
+            r.increment()
+            ret.append(r.copy())
 
     return ret

pyState/z3Helpers.py

@@ -150,6 +150,52 @@ def z3_matchLeftAndRight(left,right,op):
         else:
             left = z3_int_to_bv(left.getZ3Object(),size=bitVecSize)
 
+    ################################
+    # Case: One is Int one is Real #
+    ################################
+    # So long as this isn't modular arithmetic, let's change to Real things
+    if lType is Real and rType is Int and type(op) is not ast.Mod:
+        if right.isStatic():
+            right = z3.RealVal(right.getValue())
+        else:
+            # TODO: Z3 is really bad at handling these...
+            right = z3.ToReal(right.getZ3Object())
+
+    if rType is Real and lType is Int and type(op) is not ast.Mod:
+        if left.isStatic():
+            left = z3.RealVal(left.getValue())
+        else:
+            # TODO: Z3 is really bad at handling these...
+            left = z3.ToReal(left.getZ3Object())
+
+
+    ############################################
+    # Case: One is Int one is Real for ast.Mod #
+    ############################################
+    # So long as this isn't modular arithmetic, let's change to Real things
+    if lType is Real and rType is Int and type(op) is ast.Mod:
+        if left.isStatic():
+            leftVal = left.getValue()
+            left = z3.IntVal(leftVal)
+            if int(leftVal) != leftVal:
+                logger.warn("Truncating value for Modular Arithmetic. That may or may not be what was intended!")
+
+        else:
+            # TODO: Z3 is really bad at handling these...
+            left = z3.ToInt(left.getZ3Object())
+
+    if rType is Real and lType is Int and type(op) is ast.Mod:
+        if right.isStatic():
+            rightVal = right.getValue()
+            right = z3.IntVal(rightVal)
+            if int(rightVal) != rightVal:
+                logger.warn("Truncating value for Modular Arithmetic. That may or may not be what was intended!")
+
+        else:
+            # TODO: Z3 is really bad at handling these...
+            right = z3.ToInt(right.getZ3Object())
+
+
     # Sync-up the output variables
     left = left.getZ3Object() if type(left) in [Int, Real, BitVec] else left
     right = right.getZ3Object() if type(right) in [Int, Real, BitVec] else right