Repository: pysmt/pysmt
Pull request #714 (2022-04-13 15:59:34)

Add possibility to use several BV operators as left associative
This pull request adds the possibility to use several BV operators as left-associative, affected operators are BVAnd, BVOr, BVAdd, and BVMul.
The nodes themselves still only have two children, the formula manager was updated to allow passing an arbitrary number of operators after the left and right operator. The generated formula is created in a left-associative manner as indicated in https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml.

This also allows pySMT to read SMT-LIB scripts using these BV operators with more than two children.

A test was added in pysmt/test/test_formula.py demonstrating the new behavior.


Patch:
diff --git a/.mailmap b/.mailmap
index 8666395..a096141 100644
--- a/.mailmap
+++ b/.mailmap
@@ -5,6 +5,7 @@ Ahmed Irfan <ahmed.irfan@alumni.unitn.it>  Ahmed Irfan <43099566+ahmed-irfan@use
 Ahmed Irfan <ahmed.irfan@alumni.unitn.it>  Ahmed Irfan <ahmed.irfan@alumni.unitn.it>
 Ahmed Irfan <ahmed.irfan@alumni.unitn.it>  Ahmed Irfan <irfan@fbk.eu>
 Alessandro Girardi <girardiale00@gmail.com> rayz1065 <rayz1065@gmail.com>
+Alessandro Girardi <girardiale00@gmail.com> agirardi-fbk <95075950+agirardi-fbk@users.noreply.github.com>
 Andrea Micheli <micheli.andrea@gmail.com>  mikand <micheli.andrea@gmail.com>
 Andrea Micheli <micheli.andrea@gmail.com>  MikAnd <micheli.andrea@gmail.com>
 Ankit raj ojha <anoj123anru@gmail.com>  ankit01ojha <anoj123anru@gmail.com>
diff --git a/pysmt/formula.py b/pysmt/formula.py
index 84659cf..ea4b46c 100644
--- a/pysmt/formula.py
+++ b/pysmt/formula.py
@@ -660,17 +660,31 @@ class FormulaManager(object):
                                 args=(formula,),
                                 payload=(formula.bv_width(),))
 
-    def BVAnd(self, left, right):
-        """Returns the Bit-wise AND of two bitvectors of the same size."""
-        return self.create_node(node_type=op.BV_AND,
-                                args=(left,right),
-                                payload=(left.bv_width(),))
+    def BVAnd(self, *args):
+        """Returns the Bit-wise AND of bitvectors of the same size.
+        If more than 2 arguments are passed, a left-associative formula is generated."""
+        args = self._polymorph_args_to_tuple(args)
+        if len(args) == 0:
+            raise PysmtValueError("BVAnd expects at least one argument to be passed")
+        res = args[0]
+        for arg in args[1:]:
+            res = self.create_node(node_type=op.BV_AND,
+                             args=(res,arg),
+                             payload=(res.bv_width(),))
+        return res
 
-    def BVOr(self, left, right):
-        """Returns the Bit-wise OR of two bitvectors of the same size."""
-        return self.create_node(node_type=op.BV_OR,
-                                args=(left,right),
-                                payload=(left.bv_width(),))
+    def BVOr(self,  *args):
+        """Returns the Bit-wise OR of bitvectors of the same size.
+        If more than 2 arguments are passed, a left-associative formula is generated."""
+        args = self._polymorph_args_to_tuple(args)
+        if len(args) == 0:
+            raise PysmtValueError("BVOr expects at least one argument to be passed")
+        res = args[0]
+        for arg in args[1:]:
+            res = self.create_node(node_type=op.BV_OR,
+                             args=(res,arg),
+                             payload=(res.bv_width(),))
+        return res
 
     def BVXor(self, left, right):
         """Returns the Bit-wise XOR of two bitvectors of the same size."""
@@ -730,11 +744,18 @@ class FormulaManager(object):
                                 args=(formula,),
                                 payload=(formula.bv_width(),))
 
-    def BVAdd(self, left, right):
-        """Returns the sum of two BV."""
-        return self.create_node(node_type=op.BV_ADD,
-                                args=(left, right),
-                                payload=(left.bv_width(),))
+    def BVAdd(self, *args):
+        """Returns the sum of BV.
+        If more than 2 arguments are passed, a left-associative formula is generated."""
+        args = self._polymorph_args_to_tuple(args)
+        if len(args) == 0:
+            raise PysmtValueError("BVAdd expects at least one argument to be passed")
+        res = args[0]
+        for arg in args[1:]:
+            res = self.create_node(node_type=op.BV_ADD,
+                             args=(res,arg),
+                             payload=(res.bv_width(),))
+        return res
 
     def BVSub(self, left, right):
         """Returns the difference of two BV."""
@@ -742,11 +763,18 @@ class FormulaManager(object):
                                 args=(left, right),
                                 payload=(left.bv_width(),))
 
-    def BVMul(self, left, right):
-        """Returns the product of two BV."""
-        return self.create_node(node_type=op.BV_MUL,
-                                args=(left, right),
-                                payload=(left.bv_width(),))
+    def BVMul(self, *args):
+        """Returns the product of BV.
+        If more than 2 arguments are passed, a left-associative formula is generated."""
+        args = self._polymorph_args_to_tuple(args)
+        if len(args) == 0:
+            raise PysmtValueError("BVMul expects at least one argument to be passed")
+        res = args[0]
+        for arg in args[1:]:
+            res = self.create_node(node_type=op.BV_MUL,
+                             args=(res,arg),
+                             payload=(res.bv_width(),))
+        return res
 
     def BVUDiv(self, left, right):
         """Returns the division of the two BV."""
diff --git a/pysmt/shortcuts.py b/pysmt/shortcuts.py
index 26eefa0..fb1cc84 100644
--- a/pysmt/shortcuts.py
+++ b/pysmt/shortcuts.py
@@ -439,26 +439,26 @@ def BVNot(formula):
     return get_env().formula_manager.BVNot(formula)
 
 
-def BVAnd(left, right):
-    """Returns the Bit-wise AND of two bitvectors of the same size.
+def BVAnd(*args):
+    """Returns the Bit-wise AND of bitvectors of the same size.
+    If more than 2 arguments are passed, a left-associative formula is generated.
 
-    :param left: Specify the left bitvector
-    :param right: Specify the right bitvector
-    :returns: The bit-wise AND of left and right
+    :param *args: Specify the bitvectors
+    :returns: The bit-wise AND of the bitvectors using left association
     :rtype: FNode
     """
-    return get_env().formula_manager.BVAnd(left, right)
+    return get_env().formula_manager.BVAnd(*args)
 
 
-def BVOr(left, right):
-    """Returns the Bit-wise OR of two bitvectors of the same size.
+def BVOr(*args):
+    """Returns the Bit-wise OR of bitvectors of the same size.
+    If more than 2 arguments are passed, a left-associative formula is generated.
 
-    :param left: Specify the left bitvector
-    :param right: Specify the right bitvector
-    :returns: The bit-wise OR of left and right
+    :param *args: Specify the bitvectors
+    :returns: The bit-wise OR of the bitvectors using left association
     :rtype: FNode
     """
-    return get_env().formula_manager.BVOr(left, right)
+    return get_env().formula_manager.BVOr(*args)
 
 
 def BVXor(left, right):
@@ -547,16 +547,15 @@ def BVNeg(formula):
     """
     return get_env().formula_manager.BVNeg(formula)
 
+def BVAdd(*args):
+    """Returns the sum of BV.
+    If more than 2 arguments are passed, a left-associative formula is generated.
 
-def BVAdd(left, right):
-    """Returns the sum of two BV.
-
-    :param left: Specify the left bitvector
-    :param right: Specify the right bitvector
-    :returns: The sum of the two BVs.
+    :param *args: Specify the bitvectors
+    :returns: The sum of the bitvectors using left association.
     :rtype: FNode
     """
-    return get_env().formula_manager.BVAdd(left, right)
+    return get_env().formula_manager.BVAdd(*args)
 
 
 def BVSub(left, right):
@@ -570,15 +569,15 @@ def BVSub(left, right):
     return get_env().formula_manager.BVSub(left, right)
 
 
-def BVMul(left, right):
-    """Returns the product of two BV.
+def BVMul(*args):
+    """Returns the product of BV.
+    If more than 2 arguments are passed, a left-associative formula is generated.
 
-    :param left: Specify the left bitvector
-    :param right: Specify the right bitvector
-    :returns: The product of the two BV
+    :param *args: Specify the bitvectors
+    :returns: The product of the the bitvectors using left association
     :rtype: FNode
     """
-    return get_env().formula_manager.BVMul(left, right)
+    return get_env().formula_manager.BVMul(*args)
 
 
 def BVUDiv(left, right):


Test patch:
diff --git a/pysmt/test/test_formula.py b/pysmt/test/test_formula.py
index 545837b..25cb4db 100644
--- a/pysmt/test/test_formula.py
+++ b/pysmt/test/test_formula.py
@@ -1033,6 +1033,57 @@ class TestFormulaManager(TestCase):
         self.assertEqual(x.node_id(), xx.node_id())
         self.assertNotEqual(x.node_id(), y.node_id())
 
+    def test_left_associative_bv(self):
+        """Test that the left-associative bv operators work properly"""
+        bva = self.mgr.Symbol('a', BV8)
+        bvb = self.mgr.Symbol('b', BV8)
+        bvc = self.mgr.BV('10101010')
+        self.assertEqual(
+            # passing a list of elements
+            self.mgr.BVAnd([bva, bvb, bvc]),
+            self.mgr.BVAnd(
+                self.mgr.BVAnd(bva, bvb),
+                bvc
+            )
+        )
+        self.assertEqual(
+            # passing n elements
+            self.mgr.BVOr(bva, bvb, bvc),
+            self.mgr.BVOr(
+                self.mgr.BVOr(bva, bvb),
+                bvc
+            )
+        )
+        self.assertEqual(
+            self.mgr.BVAdd(bva, bvb, bvc),
+            self.mgr.BVAdd(
+                self.mgr.BVAdd(bva, bvb),
+                bvc
+            )
+        )
+        self.assertEqual(
+            self.mgr.BVMul(bva, bvb, bvc),
+            self.mgr.BVMul(
+                self.mgr.BVMul(bva, bvb),
+                bvc
+            )
+        )
+
+        # passing a single element
+        self.assertEqual(self.mgr.BVAnd(bva), bva)
+        self.assertEqual(self.mgr.BVOr(bva), bva)
+        self.assertEqual(self.mgr.BVAdd(bva), bva)
+        self.assertEqual(self.mgr.BVMul(bva), bva)
+
+        # passing no elements
+        self.assertRaises(PysmtValueError,
+            lambda: self.mgr.BVAnd([]))
+        self.assertRaises(PysmtValueError,
+            lambda: self.mgr.BVOr([]))
+        self.assertRaises(PysmtValueError,
+            lambda: self.mgr.BVAdd([]))
+        self.assertRaises(PysmtValueError,
+            lambda: self.mgr.BVMul([]))
 
 class TestShortcuts(TestCase):