From: makaimann <makaim@stanford.edu>
Date: Fri, 7 May 2021 18:01:16 +0000 (-0400)
Subject: Fix for toPythonObj of integer value with real sort (#6505)
X-Git-Tag: cvc5-1.0.0~1785
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50ff9213e6e6d36cea5a745e5c85ecbf1ca1ab62;p=cvc5.git

Fix for toPythonObj of integer value with real sort (#6505)
---

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 73dd7baee..135eeb165 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1574,6 +1574,7 @@ cdef class Term:
             else:
                 assert string_repr == "false"
                 res = False
+
         elif sort.isInteger():
             updated_string_repr = string_repr.strip('()').replace(' ', '')
             try:
@@ -1581,10 +1582,11 @@ cdef class Term:
             except:
                 raise ValueError("Failed to convert"
                                  " {} to an int".format(string_repr))
+
         elif sort.isReal():
             updated_string_repr = string_repr
             try:
-                # expecting format (/ a b)
+                # rational format (/ a b) most likely
                 # note: a or b could be negated: (- a)
                 splits = [s.strip('()/')
                           for s in updated_string_repr.strip('()/') \
@@ -1594,8 +1596,12 @@ cdef class Term:
                 den = int(splits[1])
                 res = Fraction(num, den)
             except:
-                raise ValueError("Failed to convert "
-                                 "{} to a Fraction".format(string_repr))
+                try:
+                    # could be exact: e.g., 1.0
+                    res = Fraction(updated_string_repr)
+                except:
+                    raise ValueError("Failed to convert "
+                                     "{} to a Fraction".format(string_repr))
 
         elif sort.isBitVector():
             # expecting format #b<bits>
@@ -1606,6 +1612,7 @@ cdef class Term:
             except:
                 raise ValueError("Failed to convert bitvector "
                                  "{} to an int".format(string_repr))
+
         elif sort.isArray():
             keys = []
             values = []
@@ -1632,6 +1639,7 @@ cdef class Term:
             res = defaultdict(lambda : base_value)
             for k, v in zip(keys, values):
                 res[k] = v
+
         elif sort.isString():
             # Strip leading and trailing double quotes and replace double
             # double quotes by single quotes
diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py
index d8094f801..572453670 100644
--- a/test/api/python/test_to_python_obj.py
+++ b/test/api/python/test_to_python_obj.py
@@ -82,3 +82,37 @@ def testGetString():
     s2 = '❤️cvc5❤️'
     t2 = solver.mkString(s2)
     assert s2 == t2.toPythonObj()
+
+
+def testGetValueInt():
+    solver = pycvc5.Solver()
+    solver.setOption("produce-models", "true")
+
+    intsort = solver.getIntegerSort()
+    x = solver.mkConst(intsort, "x")
+    solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkInteger(6)))
+
+    r = solver.checkSat()
+    assert r.isSat()
+
+    xval = solver.getValue(x)
+    assert xval.toPythonObj() == 6
+
+
+def testGetValueReal():
+    solver = pycvc5.Solver()
+    solver.setOption("produce-models", "true")
+
+    realsort = solver.getRealSort()
+    x = solver.mkConst(realsort, "x")
+    y = solver.mkConst(realsort, "y")
+    solver.assertFormula(solver.mkTerm(kinds.Equal, x, solver.mkReal("6")))
+    solver.assertFormula(solver.mkTerm(kinds.Equal, y, solver.mkReal("8.33")))
+
+    r = solver.checkSat()
+    assert r.isSat()
+
+    xval = solver.getValue(x)
+    yval = solver.getValue(y)
+    assert xval.toPythonObj() == Fraction("6")
+    assert yval.toPythonObj() == Fraction("8.33")