diff options
| -rw-r--r-- | src/api/python/cvc5.pxi | 14 | ||||
| -rw-r--r-- | test/api/python/test_to_python_obj.py | 34 |
2 files changed, 45 insertions, 3 deletions
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") |