Adding state.ctx to z3 objects created

pyObjectManager/BitVec.py

@@ -58,7 +58,7 @@ def getZ3Object(self,increment=False):
         if increment:
             self.increment()
 
-        return z3.BitVec("{0}{1}@{2}".format(self.count,self.varName,self.ctx),self.size)
+        return z3.BitVec("{0}{1}@{2}".format(self.count,self.varName,self.ctx),self.size,ctx=self.state.solver.ctx)
 
     def _isSame(self,size):
         """

pyObjectManager/Char.py

@@ -80,7 +80,7 @@ def setState(self,state):
     def increment(self):
         self.count += 1
         # reset variable list if we're incrementing our count
-        self.variable = BitVec('{1}{0}'.format(self.varName,self.count),ctx=self.ctx,size=self.size)
+        self.variable = BitVec('{1}{0}'.format(self.varName,self.count),ctx=self.ctx,size=self.size,state=self.state)
 
     def _isSame(self,**args):
         """

pyObjectManager/Int.py

@@ -60,7 +60,7 @@ def getZ3Object(self,increment=False):
             self.increment()
 
         if self.value is None:
-            return z3.Int("{0}{1}@{2}".format(self.count,self.varName,self.ctx))
+            return z3.Int("{0}{1}@{2}".format(self.count,self.varName,self.ctx),ctx=self.state.solver.ctx)
 
         return z3.IntVal(self.value)
 

pyObjectManager/List.py

@@ -162,17 +162,17 @@ def __setitem__(self,key,value):
 
         if type(value) is Int:
             logger.debug("__setitem__: setting Int")
-            self.variables[key] = Int('{2}{0}[{1}]'.format(self.varName,key,self.count),ctx=self.ctx,count=count)
+            self.variables[key] = Int('{2}{0}[{1}]'.format(self.varName,key,self.count),ctx=self.ctx,count=count,state=self.state)
             self.state.addConstraint(self.variables[key].getZ3Object() == value.getZ3Object())
 
         elif type(value) is Real:
             logger.debug("__setitem__: setting Real")
-            self.variables[key] = Real('{2}{0}[{1}]'.format(self.varName,key,self.count),ctx=self.ctx,count=count)
+            self.variables[key] = Real('{2}{0}[{1}]'.format(self.varName,key,self.count),ctx=self.ctx,count=count,state=self.state)
             self.state.addConstraint(self.variables[key].getZ3Object() == value.getZ3Object())
 
         elif type(value) is BitVec:
             logger.debug("__setitem__: setting BitVec")
-            self.variables[key] = BitVec('{2}{0}[{1}]'.format(self.varName,key,self.count),ctx=self.ctx,count=count,size=value.size)
+            self.variables[key] = BitVec('{2}{0}[{1}]'.format(self.varName,key,self.count),ctx=self.ctx,count=count,size=value.size,state=self.state)
             self.state.addConstraint(self.variables[key].getZ3Object() == value.getZ3Object())
 
         elif type(value) in [List, String]:

pyObjectManager/Real.py

@@ -60,7 +60,7 @@ def getZ3Object(self,increment=False):
             self.increment()
 
         if self.value is None:
-            return z3.Real("{0}{1}@{2}".format(self.count,self.varName,self.ctx))
+            return z3.Real("{0}{1}@{2}".format(self.count,self.varName,self.ctx),ctx=self.state.solver.ctx)
 
         return z3.RealVal(self.value)
 

pyState/AugAssign.py

@@ -41,15 +41,15 @@ def _handleNum(state,element,value,op):
         oldTargetVar, valueVar = z3Helpers.z3_matchLeftAndRight(oldTarget,value,op)
 
         if hasRealComponent(valueVar) or hasRealComponent(oldTargetVar):
-            parent[index] = Real(oldTarget.varName,ctx=state.ctx)
+            parent[index] = Real(oldTarget.varName,ctx=state.ctx,state=state)
             newTargetVar = parent[index].getZ3Object(increment=True)
 
         elif type(valueVar) in [z3.BitVecRef,z3.BitVecNumRef]:
-            parent[index] = BitVec(oldTarget.varName,ctx=state.ctx,size=valueVar.size())
+            parent[index] = BitVec(oldTarget.varName,ctx=state.ctx,size=valueVar.size(),state=state)
             newTargetVar = parent[index].getZ3Object(increment=True)
 
         else:
-            parent[index] = Int(oldTarget.varName,ctx=state.ctx)
+            parent[index] = Int(oldTarget.varName,ctx=state.ctx,state=state)
             newTargetVar = parent[index].getZ3Object(increment=True)
 
         # Figure out what the op is and add constraint

pyState/BinOp.py

@@ -57,7 +57,17 @@ def _handleNum(state,left,right,op):
 
     # TODO: This one will fail if we use BitVecs.. Maybe think about check/convert?
     elif type(op) == ast.Pow:
-        ret = leftZ3Object ** rightZ3Object
+        # Z3 has some problems with forms of x ** 0.5, let's try to change it for Z3...
+        if type(rightZ3Object) is z3.RatNumRef and rightZ3Object.numerator().as_long() == 1 and rightZ3Object.denominator().as_long() > 1:
+            tmp = state.getVar("tempRootVar",ctx=1,varType=Real)
+            # Rewrite as x ** 2 == y form
+            state.addConstraint(tmp.getZ3Object(increment=True) ** float(rightZ3Object.denominator().as_long()) == leftZ3Object)
+            # Because we're dealing with square, let's make sure it's positive
+            state.addConstraint(tmp.getZ3Object() >= 0)
+            ret = tmp.getZ3Object()
+        else:
+            ret = leftZ3Object ** rightZ3Object
+        #ret = leftZ3Object ** rightZ3Object
 
     else:
         err = "BinOP: Don't know how to handle op type {0} at line {1} col {2}".format(type(op),op.lineno,op.col_offset)

pyState/__init__.py

@@ -185,19 +185,6 @@ class State():
     Defines the state of execution at any given point.
     """
 
-    """
-    localVars and globalVars are dicts containing variables and their constraint expressions
-    
-    localVars = {
-        <contextID> : {
-            'x': {
-                'varType': "z3.IntSort()", # Eval string to re-create the object's type on the fly. This is because z3 kept on crashing everything :-(
-                'count': 0 # This helps us keep track of Static Single Assignment forms
-            }
-        }
-    }
-    """
-
     def __init__(self,path=None,solver=None,ctx=None,functions=None,simFunctions=None,retVar=None,callStack=None,backtrace=None,retID=None,loop=None,maxRetID=None,maxCtx=None,objectManager=None):
         """
         (optional) path = list of sequential actions. Derived by ast.parse. Passed to state.
@@ -208,7 +195,8 @@ def __init__(self,path=None,solver=None,ctx=None,functions=None,simFunctions=Non
         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.Then("simplify","solve-eqs","smt").solver() if solver is None else solver
+        #self.solver = z3.Then("simplify","solve-eqs","smt").solver() if solver is None else solver
+        self.solver = z3.OrElse(z3.Then("simplify","solve-eqs","smt","fail-if-undecided"),z3.Then("simplify","solve-eqs","nlsat")).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
@@ -1040,7 +1028,7 @@ def addConstraint(self,constraint):
         self.solver.add(constraint)
 
         # Using iterative engine
-        self.solver.push()
+        #self.solver.push()
 
 
     def isSat(self):
@@ -1459,8 +1447,13 @@ def copy(self):
 
         # Copy the solver state
         #solverCopy = z3.Solver()
-        solverCopy = z3.Then("simplify","solve-eqs","smt").solver()
+        #solverCopy = z3.OrElse(z3.Then("simplify","solve-eqs","smt","fail-if-undecided"),z3.Then("simplify","solve-eqs","nlsat")).solver()
+        solverCopy = z3.OrElse(z3.Then("simplify","propagate-ineqs","propagate-values","unit-subsume-simplify","smt","fail-if-undecided"),z3.Then("simplify","propagate-ineqs","propagate-values","unit-subsume-simplify","nlsat"),ctx=z3.Context()).solver()
         solverCopy.add(self.solver.assertions())
+
+
+        #solverCopy = self.solver.translate(z3.Context())
+        #print(solverCopy)
 
         newState = State(
             solver=solverCopy,

pyState/functions/int.py

@@ -62,6 +62,10 @@ def handle(state,call,obj,base=10,ctx=None):
 
         # TODO: Deal with symbolic values (returning list of possibilities)
         else:
+            print("any",state.any_n_real(obj,10))
+            print(state.solver)
+            print(obj.getZ3Object())
+            print(state.solver.check())
             err = "handle: Don't know how to handle symbolic ints for now"
             logger.error(err)
             raise Exception(err)

tests/test_pyObjectManager_List.py

@@ -117,27 +117,29 @@ def test_pyObjectManager_List_setitem():
 
     l = pg.completed[0].state.getVar('l')
 
+    s = pg.completed[0].state
+
     # Base check
     assert l[1].count == 0
     assert type(l[1]) == Real
 
     # Assign an Int
-    l[1] = Int(varName='x',ctx=0)
+    l[1] = Int(varName='x',ctx=0,state=s)
     assert l[1].count == 1
     assert type(l[1]) == Int
 
     # Assign back to Real
-    l[1] = Real(varName='x',ctx=0)
+    l[1] = Real(varName='x',ctx=0,state=s)
     assert l[1].count == 2
     assert type(l[1]) == Real
 
     # Assign to BitVec
-    l[1] = BitVec(varName='x',ctx=0,size=32)
+    l[1] = BitVec(varName='x',ctx=0,size=32,state=s)
     assert l[1].count == 3
     assert type(l[1]) == BitVec
 
     # Assign List
-    l[1] = List(varName='x',ctx=0)
+    l[1] = List(varName='x',ctx=0,state=s)
     #assert l[1].count == 4
     assert type(l[1]) == List