Repository: pysmt/pysmt
Pull request #229 (2015-11-26 20:10:52)

BV Infix notation
 BV: Support for BV Infix notation

Tests explain quirks related to mixing python constants and pySMT
constants.
Moreover, infix operators are reserved to unsigned operations. Signed
operators (and operators that cannot easily be mapped into python
operators) need to rely on the l.Operator(r) syntax.

Apart from this, the rest of the infix notation is straight-forward


Patch:
diff --git a/pysmt/fnode.py b/pysmt/fnode.py
index dce7895..21d2946 100644
--- a/pysmt/fnode.py
+++ b/pysmt/fnode.py
@@ -541,9 +541,17 @@ class FNode(object):
         return self._content.payload
 
     # Infix Notation
-    def _apply_infix(self, right, function):
+    def _apply_infix(self, right, function, bv_function=None):
         if _env().enable_infix_notation:
             mgr = _mgr()
+            # BVs
+            # Default bv_function to function
+            if bv_function is None: bv_function = function
+            if _is_bv(self):
+                if is_python_integer(right):
+                    right = mgr.BV(right, width=self.bv_width())
+                return bv_function(self, right)
+            # Boolean, Integer and Arithmetic
             if is_python_boolean(right):
                 right = mgr.Bool(right)
             elif is_python_integer(right):
@@ -576,64 +584,133 @@ class FNode(object):
     def Or(self, right):
         return self._apply_infix(right, _mgr().Or)
 
+    # BV
+    def BVSLT(self, right):
+        return self._apply_infix(right, _mgr().BVSLT)
+
+    def BVSLE(self, right):
+        return self._apply_infix(right, _mgr().BVSLE)
+
+    def BVComp(self, right):
+        return self._apply_infix(right, _mgr().BVComp)
+
+    def BVSDiv(self, right):
+        return self._apply_infix(right, _mgr().BVSDiv)
+
+    def BVSRem(self, right):
+        return self._apply_infix(right, _mgr().BVSRem)
+
+    def BVAShr(self, right):
+        return self._apply_infix(right, _mgr().BVAShr)
+
+    def BVNand(self, right):
+        return self._apply_infix(right, _mgr().BVNand)
+
+    def BVNor(self, right):
+        return self._apply_infix(right, _mgr().BVNor)
+
+    def BVXnor(self, right):
+        return self._apply_infix(right, _mgr().BVXnor)
+
+    def BVSGT(self, right):
+        return self._apply_infix(right, _mgr().BVSGT)
+
+    def BVSGE(self, right):
+        return self._apply_infix(right, _mgr().BVSGE)
+
+    def BVSMod(self, right):
+        return self._apply_infix(right, _mgr().BVSMod)
+
+    def BVRol(self, steps):
+        return _mgr().BVRol(self, steps)
+
+    def BVRor(self, steps):
+        return _mgr().BVRor(self, steps)
+
+    def BVZExt(self, increase):
+        return _mgr().BVZExt(self, increase)
+
+    def BVSExt(self, increase):
+        return _mgr().BVSExt(self, increase)
+
+    def BVRepeat(self, count):
+        return _mgr().BVRepeat(self, count)
+
+    #
+    # Infix operators
+    #
     def __add__(self, right):
-        return self._apply_infix(right, _mgr().Plus)
+        return self._apply_infix(right, _mgr().Plus, _mgr().BVAdd)
 
     def __radd__(self, right):
-        return self._apply_infix(right, _mgr().Plus)
+        return self._apply_infix(right, _mgr().Plus, _mgr().BVAdd)
 
     def __sub__(self, right):
-        return self._apply_infix(right, _mgr().Minus)
-
-    def __rsub__(self, right):
+        return self._apply_infix(right, _mgr().Minus, _mgr().BVSub)
+
+    def __rsub__(self, left):
+        # Swap operators to perform right-subtract
+        # For BVs we might need to build the BV constant
+        if _is_bv(self):
+            if is_python_integer(left):
+                left = _mgr().BV(left, width=self.bv_width())
+            return left._apply_infix(self, _mgr().BVSub)
+        # (x - y) = (-y + x)
         minus_self = -self
-        return minus_self._apply_infix(right, _mgr().Plus)
+        return minus_self._apply_infix(left, _mgr().Plus)
 
     def __mul__(self, right):
-        return self._apply_infix(right, _mgr().Times)
+        return self._apply_infix(right, _mgr().Times, _mgr().BVMul)
 
     def __rmul__(self, right):
-        return self._apply_infix(right, _mgr().Times)
+        return self._apply_infix(right, _mgr().Times, _mgr().BVMul)
 
     def __div__(self, right):
-        return self._apply_infix(right, _mgr().Div)
+        return self._apply_infix(right, _mgr().Div, _mgr().BVUDiv)
 
     def __truediv__(self, right):
         return self.__div__(right)
 
     def __gt__(self, right):
-        return self._apply_infix(right, _mgr().GT)
+        return self._apply_infix(right, _mgr().GT, _mgr().BVUGT)
 
     def __ge__(self, right):
-        return self._apply_infix(right, _mgr().GE)
+        return self._apply_infix(right, _mgr().GE, _mgr().BVUGE)
 
     def __lt__(self, right):
-        return self._apply_infix(right, _mgr().LT)
+        return self._apply_infix(right, _mgr().LT, _mgr().BVULT)
 
     def __le__(self, right):
-        return self._apply_infix(right, _mgr().LE)
+        return self._apply_infix(right, _mgr().LE, _mgr().BVULE)
 
     def __and__(self, other):
-        return self.And(other)
+        return self._apply_infix(other, _mgr().And, _mgr().BVAnd)
 
     def __rand__(self, other):
-        return self.And(other)
+        return self._apply_infix(other, _mgr().And, _mgr().BVAnd)
 
     def __or__(self, other):
-        return self.Or(other)
+        return self._apply_infix(other, _mgr().Or, _mgr().BVOr)
 
     def __ror__(self, other):
-        return self.Or(other)
+        return self._apply_infix(other, _mgr().Or, _mgr().BVOr)
 
     def __xor__(self, other):
-        return self._apply_infix(other, _mgr().Xor)
+        return self._apply_infix(other, _mgr().Xor, _mgr().BVXor)
+
+    def __rxor__(self, other):
+        return self._apply_infix(other, _mgr().Xor, _mgr().BVXor)
 
     def __neg__(self):
+        if _is_bv(self):
+            return _mgr().BVNeg(self)
         return self._apply_infix(-1, _mgr().Times)
 
     def __invert__(self):
         if not _env().enable_infix_notation:
             raise Exception("Cannot use infix notation")
+        if _is_bv(self):
+            return _mgr().BVNot(self)
         return _mgr().Not(self)
 
     def __int__(self):
@@ -651,6 +728,29 @@ class FNode(object):
             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")
+        if isinstance(idx, slice):
+            end = idx.stop
+            start = idx.start
+            if start is None: start = 0
+        else:
+            # Single point [idx]
+            end = idx
+            start = idx
+        if _is_bv(self):
+            return _mgr().BVExtract(self, start=start, end=end)
+        raise NotImplementedError
+
+    def __lshift__(self, right):
+        return self._apply_infix(right, None, bv_function=_mgr().BVLShl)
+
+    def __rshift__(self, right):
+        return self._apply_infix(right, None, bv_function=_mgr().BVLShr)
+
+    def __mod__(self, right):
+        return self._apply_infix(right, None, bv_function=_mgr().BVURem)
 # EOC FNode
 
 def _env():
@@ -660,3 +760,8 @@ def _env():
 def _mgr():
     """Aux function to obtain the formula manager."""
     return pysmt.environment.get_env().formula_manager
+
+def _is_bv(node):
+    """Aux function to check if a fnode is a BV."""
+    return (node.is_symbol() and node.symbol_type().is_bv_type()) or \
+            node.node_type() in BV_OPERATORS


Test patch:
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index 52ff65c..0ddbec4 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -20,7 +20,7 @@ from fractions import Fraction
 from six.moves import xrange
 
 import pysmt
-from pysmt.typing import BOOL, REAL, INT, FunctionType
+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 get_env
@@ -673,6 +673,203 @@ class TestFormulaManager(TestCase):
         self.assertEqual(And(x, TRUE()), x & True)
         self.assertEqual(And(x, TRUE()), True & x)
 
+        # BVs
+
+        # BV_CONSTANT: We use directly python numbers
+        #
+        # Note: In this case, the width is implicit (yikes!)  The
+        #       width of the constant is inferred by the use of a
+        #       symbol or operator that enforces a bit_width.
+        #
+        #       This works in very simple cases. For complex
+        #       expressions it is advisable to create a shortcut for
+        #       the given BVType.
+        const1 = 3
+        const2 = 0b011
+        const3 = 0x3
+        # Since these are python numbers, the following holds
+        self.assertEqual(const1, const2)
+        self.assertEqual(const1, const3)
+
+        # However, we cannot use infix pySMT Equals, since const1 is a
+        # python int!!!
+        with self.assertRaises(AttributeError):
+            const1.Equals(const2)
+
+        # We use the usual syntax to build a constant with a fixed width
+        const1_8 = self.mgr.BV(3, width=8)
+
+        # In actual code, one can simply create a macro for this:
+        _8bv = lambda v : self.mgr.BV(v, width=8)
+        const1_8b = _8bv(3)
+        self.assertEqual(const1_8, const1_8b)
+
+        # Equals forces constants to have the width of the operand
+        self.assertEqual(const1_8.Equals(const1),
+                         self.mgr.Equals(const1_8, const1_8b))
+
+        # Symbols
+        bv8 = self.mgr.FreshSymbol(BV8)
+        bv7 = self.mgr.FreshSymbol(BVType(7))
+
+        self.assertEqual(bv8.Equals(const1),
+                         bv8.Equals(const1_8))
+
+        # BV_AND,
+        self.assertEqual(bv8 & const1,
+                         self.mgr.BVAnd(bv8, const1_8))
+
+        self.assertEqual(const1 & bv8,
+                         self.mgr.BVAnd(bv8, const1_8))
+
+        self.assertEqual(const1 & bv8,
+                         self.mgr.BVAnd(bv8, const1_8))
+        # BV_XOR,
+        self.assertEqual(bv8 ^ const1,
+                         self.mgr.BVXor(bv8, const1_8))
+        self.assertEqual(const1 ^ bv8,
+                         self.mgr.BVXor(bv8, const1_8))
+        # BV_OR,
+        self.assertEqual(bv8 | const1,
+                         self.mgr.BVOr(bv8, const1_8))
+        self.assertEqual(const1 | bv8,
+                         self.mgr.BVOr(bv8, const1_8))
+        # BV_ADD,
+        self.assertEqual(bv8 + const1,
+                         self.mgr.BVAdd(bv8, const1_8))
+        self.assertEqual(const1 + bv8,
+                         self.mgr.BVAdd(bv8, const1_8))
+        # BV_SUB,
+        self.assertEqual(bv8 - const1,
+                         self.mgr.BVSub(bv8, const1_8))
+        self.assertEqual(const1 - bv8,
+                         self.mgr.BVSub(const1_8, bv8))
+        # BV_MUL,
+        self.assertEqual(bv8 * const1,
+                         self.mgr.BVMul(bv8, const1_8))
+        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
+        with self.assertRaises(ValueError):
+            _8bv(~const1)
+
+        # For symbols and expressions this works as expected
+        self.assertEqual(~bv8,
+                         self.mgr.BVNot(bv8))
+
+        # BV_NEG -- Cannot be applied to 'infix' constants
+        self.assertEqual(-bv8, self.mgr.BVNeg(bv8))
+
+        # BV_EXTRACT -- Cannot be applied to 'infix' constants
+        self.assertEqual(bv8[0:7],
+                         self.mgr.BVExtract(bv8, 0, 7))
+        self.assertEqual(bv8[:7],
+                         self.mgr.BVExtract(bv8, end=7))
+        self.assertEqual(bv8[0:],
+                         self.mgr.BVExtract(bv8, start=0))
+        self.assertEqual(bv8[7],
+                         self.mgr.BVExtract(bv8, start=7, end=7))
+        # BV_ULT,
+        self.assertEqual(bv8 < const1,
+                         self.mgr.BVULT(bv8, const1_8))
+        # BV_ULE,
+        self.assertEqual(bv8 <= const1,
+                         self.mgr.BVULE(bv8, const1_8))
+        # BV_UGT
+        self.assertEqual(bv8 > const1,
+                         self.mgr.BVUGT(bv8, const1_8))
+        # BV_UGE
+        self.assertEqual(bv8 >= const1,
+                         self.mgr.BVUGE(bv8, const1_8))
+        # BV_LSHL,
+        self.assertEqual(bv8 << const1,
+                         self.mgr.BVLShl(bv8, const1_8))
+        # BV_LSHR,
+        self.assertEqual(bv8 >> const1,
+                         self.mgr.BVLShr(bv8, const1_8))
+        # BV_UDIV,
+        self.assertEqual(bv8 / const1,
+                         self.mgr.BVUDiv(bv8, const1_8))
+        # BV_UREM,
+        self.assertEqual(bv8 % const1,
+                         self.mgr.BVURem(bv8, const1_8))
+
+        # The following operators use the infix syntax left.Operator.right
+        # These includes all signed operators
+
+        # BVSLT,
+        self.assertEqual(self.mgr.BVSLT(bv8, const1_8),
+                         bv8.BVSLT(const1_8))
+
+        #BVSLE,
+        self.assertEqual(self.mgr.BVSLE(bv8, const1_8),
+                         bv8.BVSLE(const1_8))
+
+        #BVComp
+        self.assertEqual(self.mgr.BVComp(bv8, const1_8),
+                         bv8.BVComp(const1_8))
+
+        #BVSDiv
+        self.assertEqual(self.mgr.BVSDiv(bv8, const1_8),
+                         bv8.BVSDiv(const1_8))
+
+        #BVSRem
+        self.assertEqual(self.mgr.BVSRem(bv8, const1_8),
+                         bv8.BVSRem(const1_8))
+
+        #BVAShr
+        self.assertEqual(self.mgr.BVAShr(bv8, const1_8),
+                         bv8.BVAShr(const1_8))
+
+        #BVNand
+        self.assertEqual(self.mgr.BVNand(bv8, const1_8),
+                         bv8.BVNand(const1_8))
+
+        #BVNor
+        self.assertEqual(self.mgr.BVNor(bv8, const1_8),
+                         bv8.BVNor(const1_8))
+
+        #BVXnor
+        self.assertEqual(self.mgr.BVXnor(bv8, const1_8),
+                         bv8.BVXnor(const1_8))
+
+        #BVSGT
+        self.assertEqual(self.mgr.BVSGT(bv8, const1_8),
+                         bv8.BVSGT(const1_8))
+
+        #BVSGE
+        self.assertEqual(self.mgr.BVSGE(bv8, const1_8),
+                         bv8.BVSGE(const1_8))
+
+        #BVSMod
+        self.assertEqual(self.mgr.BVSMod(bv8, const1_8),
+                         bv8.BVSMod(const1_8))
+
+        #BVRol,
+        self.assertEqual(self.mgr.BVRol(bv8, steps=5),
+                         bv8.BVRol(5))
+
+        #BVRor,
+        self.assertEqual(self.mgr.BVRor(bv8, steps=5),
+                         bv8.BVRor(5))
+
+        #BVZExt,
+        self.assertEqual(self.mgr.BVZExt(bv8, increase=4),
+                         bv8.BVZExt(4))
+
+        #BVSExt,
+        self.assertEqual(self.mgr.BVSExt(bv8, increase=4),
+                         bv8.BVSExt(4))
+
+        #BVRepeat,
+        self.assertEqual(self.mgr.BVRepeat(bv8, count=5),
+                         bv8.BVRepeat(5))
+
+        # Reset Env
         get_env().enable_infix_notation = False
 
     def test_toReal(self):