Merge pull request #450 from pysmt/bv2nat

BV2NAT: Add bv2nat operator

pysmt/formula.py

@@ -897,6 +897,13 @@ def BVRepeat(self, formula, count=1):
             res = self.BVConcat(res, formula)
         return res
 
+    def BVToNatural(self, formula):
+        """Returns the Natural number represented by the BitVector.
+
+        Given a BitVector of width m returns an integer between 0 and 2^m-1
+        """
+        return self.create_node(node_type=op.BV_TONATURAL, args=(formula,))
+
     def Select(self, arr, idx):
         """Creates a node representing an array selection."""
         return self.create_node(node_type=op.ARRAY_SELECT, args=(arr, idx))

pysmt/operators.py

@@ -25,7 +25,7 @@
 from six.moves import xrange
 
 
-ALL_TYPES = tuple(xrange(0,53))
+ALL_TYPES = tuple(xrange(0,54))
 
 (
 FORALL, EXISTS, AND, OR, NOT, IMPLIES, IFF, # Boolean Logic (0-6)
@@ -54,13 +54,15 @@
                                             # equal otherwise it returns 0_1 (44)
 BV_SDIV, BV_SREM,                           # Signed Division and Reminder(45-46)
 BV_ASHR,                                    # Arithmetic shift right (47)
-ARRAY_SELECT,                               # Array Select (48)
-ARRAY_STORE,                                # Array Store (49)
-ARRAY_VALUE,                                # Array Value (50)
+BV_TONATURAL,                               # BV to Natural Conversion (48)
 
-DIV,                                        # Arithmetic Division (51)
-POW,                                        # Arithmetic Power (52)
-ALGEBRAIC_CONSTANT,                         # Algebraic Number (53)
+ARRAY_SELECT,                               # Array Select (49)
+ARRAY_STORE,                                # Array Store (50)
+ARRAY_VALUE,                                # Array Value (51)
+
+DIV,                                        # Arithmetic Division (52)
+POW,                                        # Arithmetic Power (53)
+ALGEBRAIC_CONSTANT,                         # Algebraic Number (54)
 ) = ALL_TYPES
 
 QUANTIFIERS = frozenset([FORALL, EXISTS])
@@ -84,7 +86,7 @@
                           BV_ROL, BV_ROR, BV_ZEXT, BV_SEXT,
                           BV_COMP, BV_SDIV, BV_SREM, BV_ASHR])
 
-IRA_OPERATORS = frozenset([PLUS, MINUS, TIMES, TOREAL, DIV, POW])
+IRA_OPERATORS = frozenset([PLUS, MINUS, TIMES, TOREAL, DIV, POW, BV_TONATURAL])
 
 ARRAY_OPERATORS = frozenset([ARRAY_SELECT, ARRAY_STORE, ARRAY_VALUE])
 
@@ -177,6 +179,7 @@ def all_types():
     BV_SDIV : "BV_SDIV",
     BV_SREM : "BV_SREM",
     BV_ASHR : "BV_ASHR",
+    BV_TONATURAL : "BV_TONATURAL",
     ARRAY_SELECT : "ARRAY_SELECT",
     ARRAY_STORE : "ARRAY_STORE",
     ARRAY_VALUE : "ARRAY_VALUE",

pysmt/oracles.py

@@ -231,6 +231,13 @@ def walk_toreal(self, formula, args, **kwargs):
         theory_out = theory_out.set_lira()
         return theory_out
 
+    def walk_bv_tonatural(self, formula, args, **kwargs):
+        #pylint: disable=unused-argument
+        """Extends the Theory with Integer."""
+        theory_out = args[0].copy()
+        theory_out.integer_arithmetic = True
+        return theory_out
+
     def walk_times(self, formula, args, **kwargs):
         """Extends the Theory with Non-Linear, if needed."""
         theory_out = args[0]

pysmt/parsing.py

@@ -107,7 +107,7 @@ def led(self, parser, left):
 # 70 : Plus, Minus, BVAdd, BVSub
 # 80 : Times, Div, BVMul, BVUDiv, BVSDiv, BVSRem, BVURem
 # 90 : BVLShl, BVLShr, BVAShr, BVConcat, BVXor, BVRor, BVRol, BVZExt, BVSExt, BVComp
-# 100 : ToReal Uminus BVNeg
+# 100 : ToReal Uminus BVNeg BVToNat
 # 200 : ()
 # 300 : []
 
@@ -172,14 +172,15 @@ def __init__(self, env=None):
             Rule(r"(,)", ExprComma(), False),# comma
             Rule(r"(\.)", ExprDot(), False),# dot
             Rule(r"(xor)", InfixOpAdapter(self.mgr.BVXor, 10), False),# BVXor
-            Rule(r"(ROR)", InfixOpAdapter(self.BVHack(self.mgr.BVRor), 90), False),# BVXor
-            Rule(r"(ROL)", InfixOpAdapter(self.BVHack(self.mgr.BVRol), 90), False),# BVXor
-            Rule(r"(ZEXT)", InfixOpAdapter(self.BVHack(self.mgr.BVZExt), 90), False),# BVXor
-            Rule(r"(SEXT)", InfixOpAdapter(self.BVHack(self.mgr.BVSExt), 90), False),# BVXor
-            Rule(r"(bvcomp)", InfixOpAdapter(self.mgr.BVComp, 90), False),# BVXor
-            Rule(r"(forall)", Quantifier(self.mgr.ForAll, 20), False),# BVXor
-            Rule(r"(exists)", Quantifier(self.mgr.Exists, 20), False),# BVXor
-            Rule(r"(ToReal)", UnaryOpAdapter(self.mgr.ToReal, 100), False),# BVXor
+            Rule(r"(ROR)", InfixOpAdapter(self.BVHack(self.mgr.BVRor), 90), False),# BVRor
+            Rule(r"(ROL)", InfixOpAdapter(self.BVHack(self.mgr.BVRol), 90), False),# BVRol
+            Rule(r"(ZEXT)", InfixOpAdapter(self.BVHack(self.mgr.BVZExt), 90), False),# BVZext
+            Rule(r"(SEXT)", InfixOpAdapter(self.BVHack(self.mgr.BVSExt), 90), False),# BVSext
+            Rule(r"(bvcomp)", InfixOpAdapter(self.mgr.BVComp, 90), False),#
+            Rule(r"(forall)", Quantifier(self.mgr.ForAll, 20), False),#
+            Rule(r"(exists)", Quantifier(self.mgr.Exists, 20), False),#
+            Rule(r"(ToReal)", UnaryOpAdapter(self.mgr.ToReal, 100), False),#
+            Rule(r"(bv2nat)", UnaryOpAdapter(self.mgr.BVToNatural, 100), False),#
             Rule(r"\"(.*?)\"", self.identifier, True),# quoted identifiers
             Rule(r"([A-Za-z_][A-Za-z0-9_]*)", self.identifier, True),# identifiers
             Rule(r"(.)", self.lexing_error, True), # input error

pysmt/printers.py

@@ -202,6 +202,11 @@ def walk_array_value(self, formula):
             yield assign[k]
             self.write("]")
 
+    def walk_bv_tonatural(self, formula):
+        self.write("bv2nat(")
+        yield formula.arg(0)
+        self.write(")")
+
     def walk_and(self, formula): return self.walk_nary(formula, " & ")
     def walk_or(self, formula): return self.walk_nary(formula, " | ")
     def walk_plus(self, formula): return self.walk_nary(formula, " + ")
@@ -212,22 +217,22 @@ def walk_iff(self, formula): return self.walk_nary(formula, " <-> ")
     def walk_implies(self, formula): return self.walk_nary(formula, " -> ")
     def walk_minus(self, formula): return self.walk_nary(formula, " - ")
     def walk_equals(self, formula): return self.walk_nary(formula, " = ")
-    def walk_le (self, formula): return self.walk_nary(formula, " <= ")
-    def walk_lt (self, formula): return self.walk_nary(formula, " < ")
-    def walk_bv_xor (self, formula): return self.walk_nary(formula, " xor ")
-    def walk_bv_concat (self, formula): return self.walk_nary(formula, "::")
-    def walk_bv_udiv (self, formula): return self.walk_nary(formula, " u/ ")
-    def walk_bv_urem (self, formula): return self.walk_nary(formula, " u% ")
-    def walk_bv_sdiv (self, formula): return self.walk_nary(formula, " s/ ")
-    def walk_bv_srem (self, formula): return self.walk_nary(formula, " s% ")
-    def walk_bv_sle (self, formula): return self.walk_nary(formula, " s<= ")
-    def walk_bv_slt (self, formula): return self.walk_nary(formula, " s< ")
-    def walk_bv_ule (self, formula): return self.walk_nary(formula, " u<= ")
-    def walk_bv_ult (self, formula): return self.walk_nary(formula, " u< ")
-    def walk_bv_lshl (self, formula): return self.walk_nary(formula, " << ")
-    def walk_bv_lshr (self, formula): return self.walk_nary(formula, " >> ")
-    def walk_bv_ashr (self, formula): return self.walk_nary(formula, " a>> ")
-    def walk_bv_comp (self, formula): return self.walk_nary(formula, " bvcomp ")
+    def walk_le(self, formula): return self.walk_nary(formula, " <= ")
+    def walk_lt(self, formula): return self.walk_nary(formula, " < ")
+    def walk_bv_xor(self, formula): return self.walk_nary(formula, " xor ")
+    def walk_bv_concat(self, formula): return self.walk_nary(formula, "::")
+    def walk_bv_udiv(self, formula): return self.walk_nary(formula, " u/ ")
+    def walk_bv_urem(self, formula): return self.walk_nary(formula, " u% ")
+    def walk_bv_sdiv(self, formula): return self.walk_nary(formula, " s/ ")
+    def walk_bv_srem(self, formula): return self.walk_nary(formula, " s% ")
+    def walk_bv_sle(self, formula): return self.walk_nary(formula, " s<= ")
+    def walk_bv_slt(self, formula): return self.walk_nary(formula, " s< ")
+    def walk_bv_ule(self, formula): return self.walk_nary(formula, " u<= ")
+    def walk_bv_ult(self, formula): return self.walk_nary(formula, " u< ")
+    def walk_bv_lshl(self, formula): return self.walk_nary(formula, " << ")
+    def walk_bv_lshr(self, formula): return self.walk_nary(formula, " >> ")
+    def walk_bv_ashr(self, formula): return self.walk_nary(formula, " a>> ")
+    def walk_bv_comp(self, formula): return self.walk_nary(formula, " bvcomp ")
     walk_bv_and = walk_and
     walk_bv_or = walk_or
     walk_bv_not = walk_not

pysmt/shortcuts.py

@@ -760,6 +760,14 @@ def BVComp(left, right):
     """
     return get_env().formula_manager.BVComp(left, right)
 
+def BVToNatural(formula):
+    """Returns the Natural number represented by the BitVector.
+
+    :param formula: Bitvector to be converted
+    :returns: An integer between 0 and 2^m-1
+    :rtype: FNode
+    """
+    return get_env().formula_manager.BVToNatural(formula)
 
 #
 # Arrays

pysmt/simplifier.py

@@ -648,6 +648,11 @@ def walk_bv_ashr(self, formula, args, **kwargs):
             return ret
         return self.manager.BVAShr(l, r)
 
+    def walk_bv_tonatural(self, formula, args, **kwargs):
+        if args[0].is_bv_constant():
+            return self.manager.Int(args[0].constant_value())
+        return self.manager.BVToNatural(args[0])
+
     def walk_array_select(self, formula, args, **kwargs):
         a, i = args
         if a.is_array_value() and i.is_constant():
@@ -778,7 +783,6 @@ def _validate(self, old, new):
     def abstract_and_simplify(self, formula):
         abs_formula = self.walk(formula)
         abs_res = self.back(self.convert(abs_formula))
-        print(formula, abs_formula, abs_res)
         res = abs_res.substitute(self.ba_map)
         return res
 

pysmt/smtlib/parser/parser.py

@@ -412,6 +412,7 @@ def fix_real(op, *args):
                             'bvsle':self._operator_adapter(mgr.BVSLE),
                             'bvsgt':self._operator_adapter(mgr.BVSGT),
                             'bvsge':self._operator_adapter(mgr.BVSGE),
+                            'bv2nat':self._operator_adapter(mgr.BVToNatural),
                             # arrays
                             'select':self._operator_adapter(mgr.Select),
                             'store':self._operator_adapter(mgr.Store),
@@ -1304,6 +1305,8 @@ def __init__(self, environment=None, interactive=False):
                                 self._operator_adapter(self._ext_rotate_left)
         self.interpreted["ext_rotate_right"] =\
                                 self._operator_adapter(self._ext_rotate_right)
+        mgr = self.env.formula_manager
+        self.interpreted['bv2int'] = self._operator_adapter(mgr.BVToNatural)
 
     def _ext_rotate_left(self, x, y):
         return self.env.formula_manager.BVRol(x, y.simplify().constant_value())

pysmt/smtlib/printers.py

@@ -83,6 +83,7 @@ def walk_bv_comp(self, formula): return self.walk_nary(formula, "bvcomp")
     def walk_bv_ashr(self, formula): return self.walk_nary(formula, "bvashr")
     def walk_bv_sdiv(self, formula): return self.walk_nary(formula, "bvsdiv")
     def walk_bv_srem(self, formula): return self.walk_nary(formula, "bvsrem")
+    def walk_bv_tonatural(self, formula): return self.walk_nary(formula, "bv2nat")
     def walk_array_select(self, formula): return self.walk_nary(formula, "select")
     def walk_array_store(self, formula): return self.walk_nary(formula, "store")
 
@@ -350,6 +351,9 @@ def walk_bv_sdiv(self, formula, args):
     def walk_bv_srem(self, formula, args):
         return self.walk_nary(formula, args, "bvsrem")
 
+    def walk_bv_tonatural(self, formula, args):
+        return self.walk_nary(formula, args, "bv2nat")
+
     def walk_array_select(self, formula, args):
         return self.walk_nary(formula, args, "select")
 

pysmt/solvers/cvc4.py

@@ -384,6 +384,9 @@ def walk_bv_neg(self, formula, args, **kwargs):
     def walk_bv_mul(self, formula, args, **kwargs):
         return self.mkExpr(CVC4.BITVECTOR_MULT, args[0], args[1])
 
+    def walk_bv_tonatural(self, formula, args, **kwargs):
+        return self.mkExpr(CVC4.BITVECTOR_TO_NAT, args[0])
+
     def walk_bv_udiv(self, formula, args, **kwargs):
         # Force deterministic semantics of division by 0
         # If the denominator is bv0, then the result is ~0
@@ -448,13 +451,13 @@ def walk_bv_sext (self, formula, args, **kwargs):
     def walk_bv_slt(self, formula, args, **kwargs):
         return self.mkExpr(CVC4.BITVECTOR_SLT, args[0], args[1])
 
-    def walk_bv_sle (self, formula, args, **kwargs):
+    def walk_bv_sle(self, formula, args, **kwargs):
         return self.mkExpr(CVC4.BITVECTOR_SLE, args[0], args[1])
 
-    def walk_bv_comp (self, formula, args, **kwargs):
+    def walk_bv_comp(self, formula, args, **kwargs):
         return self.mkExpr(CVC4.BITVECTOR_COMP, args[0], args[1])
 
-    def walk_bv_sdiv (self, formula, args, **kwargs):
+    def walk_bv_sdiv(self, formula, args, **kwargs):
         # Force deterministic semantics of division by 0
         # If the denominator is bv0, then the result is:
         #   * ~0 (if the numerator is signed >= 0)
@@ -480,7 +483,7 @@ def walk_bv_sdiv (self, formula, args, **kwargs):
             is_zero = self.mkExpr(CVC4.EQUAL, d, zero)
             return self.mkExpr(CVC4.ITE, is_zero, sign_expr, base)
 
-    def walk_bv_srem (self, formula, args, **kwargs):
+    def walk_bv_srem(self, formula, args, **kwargs):
         # Force deterministic semantics of reminder by 0
         # If the denominator is bv0, then the result is the numerator
         n,d = args
@@ -498,7 +501,7 @@ def walk_bv_srem (self, formula, args, **kwargs):
             test = self.mkExpr(CVC4.EQUAL, d, zero)
             return self.mkExpr(CVC4.ITE, test, n, base)
 
-    def walk_bv_ashr (self, formula, args, **kwargs):
+    def walk_bv_ashr(self, formula, args, **kwargs):
         return self.mkExpr(CVC4.BITVECTOR_ASHR, args[0], args[1])
 
     def _type_to_cvc4(self, tp):

pysmt/solvers/msat.py

@@ -433,9 +433,10 @@ def __init__(self, environment, msat_env):
             mathsat.MSAT_TAG_BV_LSHR: self._back_adapter(self.mgr.BVLShr),
             mathsat.MSAT_TAG_BV_ASHR: self._back_adapter(self.mgr.BVAShr),
             mathsat.MSAT_TAG_BV_COMP: self._back_adapter(self.mgr.BVComp),
+            mathsat.MSAT_TAG_INT_FROM_UBV: self._back_adapter(self.mgr.BVToNatural),
             mathsat.MSAT_TAG_ARRAY_READ: self._back_adapter(self.mgr.Select),
             mathsat.MSAT_TAG_ARRAY_WRITE: self._back_adapter(self.mgr.Store),
-            # Slightly more complext conversion
+            # Slightly more complex conversion
             mathsat.MSAT_TAG_BV_EXTRACT: self._back_bv_extract,
             mathsat.MSAT_TAG_BV_ZEXT: self._back_bv_zext,
             mathsat.MSAT_TAG_BV_SEXT: self._back_bv_sext,
@@ -991,6 +992,9 @@ def walk_toreal(self, formula, args, **kwargs):
         # In mathsat toreal is implicit
         return args[0]
 
+    def walk_bv_tonatural(self, formula, args, **kwargs):
+        return mathsat.msat_make_int_from_ubv(self.msat_env(), args[0])
+
     def walk_array_select(self, formula, args, **kwargs):
         return mathsat.msat_make_array_read(self.msat_env(), args[0], args[1])
 

pysmt/solvers/z3.py

@@ -341,6 +341,7 @@ def __init__(self, environment, z3_ctx):
             z3.Z3_OP_BSUB : lambda args, expr: self.mgr.BVSub(args[0], args[1]),
             z3.Z3_OP_EXT_ROTATE_LEFT : lambda args, expr: self.mgr.BVRol(args[0], args[1].bv_unsigned_value()),
             z3.Z3_OP_EXT_ROTATE_RIGHT: lambda args, expr: self.mgr.BVRor(args[0], args[1].bv_unsigned_value()),
+            z3.Z3_OP_BV2INT: lambda args, expr: self.mgr.BVToNatural(args[0]),
             z3.Z3_OP_POWER : lambda args, expr: self.mgr.Pow(args[0], args[1]),
             z3.Z3_OP_SELECT : lambda args, expr: self.mgr.Select(args[0], args[1]),
             z3.Z3_OP_STORE : lambda args, expr: self.mgr.Store(args[0], args[1], args[2]),
@@ -550,7 +551,7 @@ def _back_single_term(self, expr, args, model=None):
 
         # If we reach this point, we did not manage to translate the expression
         raise ConvertExpressionError(message=("Unsupported expression: %s" %
-                                              str(expr)),
+                                              (str(expr))),
                                      expression=expr)
 
     def _back_z3_eq(self, args, expr):
@@ -771,7 +772,7 @@ def walk_bv_sext (self, formula, args, **kwargs):
         z3.Z3_inc_ref(self.ctx.ref(), z3term)
         return z3term
 
-    def walk_bv_comp (self, formula, args, **kwargs):
+    def walk_bv_comp(self, formula, args, **kwargs):
         cond = z3.Z3_mk_eq(self.ctx.ref(), args[0], args[1])
         z3.Z3_inc_ref(self.ctx.ref(), cond)
         then_ = z3.Z3_mk_numeral(self.ctx.ref(), "1", self.z3BitVecSort(1).ast)
@@ -786,6 +787,11 @@ def walk_bv_comp (self, formula, args, **kwargs):
         z3.Z3_dec_ref(self.ctx.ref(), else_)
         return z3term
 
+    def walk_bv_tonatural(self, formula, args, **kwargs):
+        z3term = z3.Z3_mk_bv2int(self.ctx.ref(), args[0], False)
+        z3.Z3_inc_ref(self.ctx.ref(), z3term)
+        return z3term
+
     def walk_array_select(self, formula, args, **kwargs):
         z3term = z3.Z3_mk_select(self.ctx.ref(), args[0], args[1])
         z3.Z3_inc_ref(self.ctx.ref(), z3term)

pysmt/test/examples.py

@@ -32,7 +32,7 @@
                              BVNeg, BVAdd, BVMul, BVUDiv, BVURem, BVSub,
                              BVLShl, BVLShr,BVRol, BVRor,
                              BVZExt, BVSExt, BVSub, BVComp, BVAShr, BVSLE,
-                             BVSLT, BVSGT, BVSGE, BVSDiv, BVSRem,
+                             BVSLT, BVSGT, BVSGE, BVSDiv, BVSRem, BVToNatural,
                              Store, Select, Array,
                              Type)
 from pysmt.constants import Fraction
@@ -575,6 +575,13 @@ def get_full_example_formulae(environment=None):
                     is_sat=True,
                     logic=pysmt.logics.QF_BV
                 ),
+
+            Example(hr="(bv2nat(1_8) = 1)",
+                    expr=Equals(BVToNatural(BVOne(8)), Int(1)),
+                    is_valid=True,
+                    is_sat=True,
+                    logic=pysmt.logics.QF_AUFBVLIRA
+                ),
             #
             # Quantification
             #

pysmt/test/smtlib/test_parser_extensibility.py

@@ -111,6 +111,5 @@ def test_basic(self):
         self.assertIsNotNone(ts)
 
 
-
 if __name__ == '__main__':
     main()

pysmt/test/test_bv.py

@@ -329,6 +329,10 @@ def test_infix_with_array(self):
         self.assertEqual(f.Equals(5),
                          f.Equals(mgr.BV(5, 128)))
 
+    def test_bv_to_natural(self):
+        mgr = self.env.formula_manager
+        c1 = mgr.BVToNatural(mgr.BV(1, 32)).simplify()
+        self.assertEqual(c1.constant_value(), 1)
 
 if __name__ == "__main__":
     main()

pysmt/test/test_solving.py

@@ -324,8 +324,9 @@ def test_examples_get_implicant(self):
                             self.assertIsNone(f_i)
                     except ConvertExpressionError as ex:
                         # Some solvers do not support ARRAY_VALUE
-                        self.assertEqual(ex.expression.node_type(), op.ARRAY_VALUE)
-                        self.assertTrue(sname in ["cvc4", "btor"])
+                        if ex.expression.node_type() == op.ARRAY_VALUE:
+                            self.assertTrue(sname in ["cvc4", "btor"])
+                        self.assertTrue(ex.expression.node_type() == op.BV_TONAT)
 
 
     def test_solving_under_assumption(self):