Adding pyState.Real(integer) method

pyObjectManager/Real.py

@@ -113,6 +113,44 @@ def __str__(self):
         """
         return str(self.state.any_real(self))
 
+    def mustBe(self,var):
+        """
+        Test if this Real must be equal to another variable
+        Returns True or False
+        """
+        if not self.canBe(var):
+            return False
+
+        # So we can be, now must we?
+        if len(self.state.any_n_real(self,2)) == 1:
+            return True
+
+        return False
+
+
+    def canBe(self,var):
+        """
+        Test if this Real can be equal to the given variable
+        Returns True or False
+        """
+        # TODO: Maybe want canBe to include Integers?
+        if type(var) not in [Real, float]:
+            return False
+
+        # Ask the solver
+        s = self.state.copy()
+
+        if type(var) is Real:
+            s.addConstraint(self.getZ3Object() == var.getZ3Object())
+        else:
+            s.addConstraint(self.getZ3Object() == var)
+
+        if s.isSat():
+            return True
+
+        return False
+
+
 
 # Circular importing problem. Don't hate :-)
 from pyObjectManager.Int import Int

pyState/If.py

@@ -57,8 +57,16 @@ def handle(state,element):
     elif type(element.test) == ast.BoolOp:
         trueConstraint = pyState.BoolOp.handle(state, element.test)
 
+    #elif type(element.test) == ast.UnaryOp:
+    #    trueConstraint = pyState.UnaryOp.handle(state, element.test)
+    #    # This returns pyObjectManager objects, need to resolve the
+    #    trueConstraint = [[x for x in constraint.state.assertions()][-1] for constraint in trueConstraint]
+
     else:
-        logger.error("handle: I don't know how to handle type {0}".format(type(element.test)))
+        err = "handle: I don't know how to handle type {0}".format(type(element.test))
+        logger.error(err)
+        raise Exception(err)
+
 
     # Normalize
     trueConstraint = trueConstraint if type(trueConstraint) is list else [trueConstraint]

pyState/UnaryOp.py

@@ -29,7 +29,7 @@ def handle(state,element,ctx=None):
     targets = state.resolveObject(element.operand)
 
     ret = []    
-
+    
     for target in targets:
 
         # Use the target's state

pyState/functions/pyState/Real.py

@@ -2,12 +2,25 @@
 import ast
 from pyObjectManager.Real import Real
 
-def handle(state,call,ctx=None):
+def handle(state,call,value=None,ctx=None):
     """
     Returns a z3 Real object. Use this to inform pySym that something should be Real symbolic
+    (optional) value == the value to set this variable to
     """
     ctx = ctx if ctx is not None else state.ctx
 
-    myReal = state.resolveObject(ast.Name('temp',0),ctx=1,varType=Real)
+    myReal = state.resolveObject(ast.Name('tempReal',0),ctx=ctx,varType=Real)
+
+    ret = myReal
+
+    if value is not None:
+        ret = []
+        for r in myReal:
+            state = r.state
+            value = state.resolveObject(value,ctx=ctx)
+            for v in value:
+                r.setTo(v)
+                ret.append(r.copy())
+                r.increment()
 
-    return myReal
+    return ret

tests/test_function_pyState_Real.py

@@ -0,0 +1,45 @@
+import sys, os
+myPath = os.path.dirname(os.path.abspath(__file__))
+sys.path.insert(0, myPath + '/../')
+
+import logging
+import Colorer
+logging.basicConfig(level=logging.DEBUG,format='%(name)s - %(levelname)s - %(message)s', datefmt='%m/%d/%Y %I:%M:%S %p')
+
+import ast
+import z3
+from pyPath import Path
+from pyPathGroup import PathGroup
+import pytest
+from pyObjectManager.Int import Int
+from pyObjectManager.Real import Real
+from pyObjectManager.BitVec import BitVec
+from pyObjectManager.List import List
+from pyState.z3Helpers import Z3_MAX_STRING_LENGTH
+
+test1 = """
+s = pyState.Real()
+s2 = pyState.Real(123)
+s3 = pyState.Real(123.5)
+"""
+
+
+def test_function_pyState_Real():
+    b = ast.parse(test1).body
+    p = Path(b,source=test1)
+    pg = PathGroup(p)
+
+    pg.explore()
+    assert len(pg.completed) == 1
+
+    s = pg.completed[0].state.getVar('s')
+    s2 = pg.completed[0].state.getVar('s2')
+    s3 = pg.completed[0].state.getVar('s3')
+
+    assert type(s) == Real
+    assert type(s2) == Real
+    assert type(s3) == Real
+
+    assert s.canBe(123.0)
+    assert s2.getValue() == 123.0
+    assert s3.getValue() == 123.5