Merge pull request #441 from pysmt/i435/bv_const_gmpy

BV: Convert GMPY object in BV constructor

pysmt/formula.py

@@ -569,21 +569,24 @@ def BV(self, value, width=None):
         if width is None:
             raise PysmtValueError("Need to specify a width for the constant")
 
-        if is_python_integer(value):
-            if value < 0:
-                raise PysmtValueError("Cannot specify a negative value: %d" \
-                                      % value)
-            if value >= 2**width:
-                raise PysmtValueError("Cannot express %d in %d bits" \
-                                      % (value, width))
-
-            return self.create_node(node_type=op.BV_CONSTANT,
-                                    args=tuple(),
-                                    payload=(value, width))
-
+        if is_pysmt_integer(value):
+            _value = value
+        elif is_python_integer(value):
+            _value = pysmt_integer_from_integer(value)
         else:
-            raise PysmtTypeError("Invalid type in constant. The type was:" + \
-                                 str(type(value)))
+            raise PysmtTypeError("Invalid type in constant. The type was: %s" \
+                                 % str(type(value)))
+        if _value < 0:
+            raise PysmtValueError("Cannot specify a negative value: %d" \
+                                  % _value)
+        if _value >= 2**width:
+            raise PysmtValueError("Cannot express %d in %d bits" \
+                                  % (_value, width))
+
+        return self.create_node(node_type=op.BV_CONSTANT,
+                                args=tuple(),
+                                payload=(_value, width))
+
 
     def SBV(self, value, width=None):
         """Returns a constant of type BitVector interpreting the sign.

pysmt/solvers/btor.py

@@ -34,6 +34,7 @@
                               ConvertExpressionError, PysmtValueError)
 from pysmt.decorators import clear_pending_pop, catch_conversion_error
 from pysmt.logics import QF_BV, QF_UFBV, QF_ABV, QF_AUFBV, QF_AX
+from pysmt.constants import to_python_integer
 
 
 class BoolectorOptions(SolverOptions):
@@ -343,7 +344,7 @@ def walk_function(self, formula, args, **kwargs):
         return _uf(*args)
 
     def walk_bv_constant(self, formula, **kwargs):
-        value = formula.constant_value()
+        value = to_python_integer(formula.constant_value())
         width = formula.bv_width()
         return self._btor.Const(value, width)
 

pysmt/test/__init__.py

@@ -24,6 +24,7 @@
     import unittest
 
 from pysmt.environment import get_env, reset_env
+skipIf = unittest.skipIf
 
 
 class TestCase(unittest.TestCase):

pysmt/test/test_bv.py

@@ -15,13 +15,15 @@
 #   See the License for the specific language governing permissions and
 #   limitations under the License.
 #
+
 from pysmt.test import TestCase, skipIfNoSolverForLogic, main
 from pysmt.shortcuts import Symbol, And, Symbol, Equals, TRUE
 from pysmt.shortcuts import is_sat, is_valid, get_model, is_unsat
 from pysmt.typing import BVType, BV32, BV128, FunctionType, ArrayType
 from pysmt.logics import QF_BV
 from pysmt.exceptions import PysmtValueError, PysmtTypeError
 
+
 class TestBV(TestCase):
 
     @skipIfNoSolverForLogic(QF_BV)

pysmt/test/test_constants.py

@@ -16,9 +16,10 @@
 #   limitations under the License.
 #
 from six import PY2
-from pysmt.test import TestCase, main
+from fractions import Fraction as pyFraction
 
-from pysmt.constants import Fraction, Integer, HAS_GMPY
+from pysmt.test import TestCase, main, skipIf
+from pysmt.constants import Fraction, Integer, HAS_GMPY, USE_GMPY
 from pysmt.constants import is_pysmt_fraction, is_pysmt_integer
 from pysmt.constants import is_python_integer, is_python_boolean, is_python_rational
 from pysmt.constants import pysmt_integer_from_integer
@@ -29,8 +30,6 @@
 class TestConstants(TestCase):
 
     def test_is_methods(self):
-        from fractions import Fraction as pyFraction
-
         self.assertFalse(is_pysmt_fraction(4))
         self.assertTrue(is_pysmt_fraction(Fraction(4)))
 
@@ -58,32 +57,68 @@ def test_is_methods(self):
         self.assertTrue(is_python_boolean(False))
 
     def test_pysmt_integer_from_integer(self):
-        from fractions import Fraction as pyFraction
-
         self.assertEqual(Integer(4), pysmt_integer_from_integer(4))
         self.assertEqual(Integer(4), pysmt_integer_from_integer(Integer(4)))
         self.assertEqual(Integer(4), pysmt_integer_from_integer(Fraction(4)))
         self.assertEqual(Integer(4), pysmt_integer_from_integer(pyFraction(4)))
 
     def test_to_python_integer(self):
-        from fractions import Fraction as pyFraction
-
         res = long(4) if PY2 else int(4)
         self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(4)))
         self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(Integer(4))))
         self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(Fraction(4))))
         self.assertEqual(res, to_python_integer(pysmt_integer_from_integer(pyFraction(4))))
 
-
     def test_pysmt_fraction_from_rational(self):
-        from fractions import Fraction as pyFraction
-
         self.assertEqual(Fraction(4,5), pysmt_fraction_from_rational("4/5"))
         self.assertEqual(Fraction(4,5), pysmt_fraction_from_rational(pyFraction(4,5)))
         self.assertEqual(Fraction(4,5), pysmt_fraction_from_rational(Fraction(4,5)))
         self.assertEqual(Fraction(4), pysmt_fraction_from_rational(4))
         self.assertEqual(Fraction(4), pysmt_fraction_from_rational(Integer(4)))
 
+    @skipIf(not HAS_GMPY or USE_GMPY, "Not using GMPY")
+    def test_constructors_from_gmpy(self):
+        from gmpy2 import mpz
+
+        mgr = self.env.formula_manager
+        five = mpz(5)
+        six = mpz(6)
+
+        int5a = mgr.Int(5)
+        int5b = mgr.Int(five)
+        type_5a = type(int5a.constant_value())
+        type_5b = type(int5b.constant_value())
+        self.assertEqual(type_5a, type_5b)
+
+        # Note that we first create the constant using the GMPY value
+        int6b = mgr.Int(six)
+        int6a = mgr.Int(6)
+
+        type_6a = type(int6a.constant_value())
+        type_6b = type(int6b.constant_value())
+        self.assertEqual(type_6a, type_6b)
+        # Verify that type is the same independently of how the first
+        # node was created
+        self.assertEqual(type_5a, type_6a)
+
+        # Repeat with BV
+        bv5a = mgr.BV(5, 8)
+        bv5b = mgr.BV(five, 8)
+        type_5a = type(bv5a.constant_value())
+        type_5b = type(bv5b.constant_value())
+        self.assertEqual(type_5a, type_5b)
+
+        # Note that we first create the constant using the GMPY value
+        bv6b = mgr.BV(six, 8)
+        bv6a = mgr.BV(6, 8)
+
+        type_6a = type(bv6a.constant_value())
+        type_6b = type(bv6b.constant_value())
+        self.assertEqual(type_6a, type_6b)
+        # Verify that type is the same independently of how the first
+        # node was created
+        self.assertEqual(type_5a, type_6a)
+
 
 if __name__ == '__main__':
     main()