From: makaimann Date: Tue, 22 Sep 2020 18:58:03 +0000 (-0700) Subject: Add method to get Python object from constant value term in Python API (#5083) X-Git-Tag: cvc5-1.0.0~2826 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2e2424a1a8ce19a3c4e357cf491ca027a5d1b4cc;p=cvc5.git Add method to get Python object from constant value term in Python API (#5083) This PR addresses issue https://github.com/CVC4/CVC4/issues/5014. It simply interprets the SMT-LIB string representation and produces a Python object. It currently supports booleans, ints, reals, bit-vectors, and arrays. The method (`toPythonObj`) is only valid to call if `isConst` returns true. --- diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 8c4bfe5e5..9e4102b90 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -1,3 +1,5 @@ +from collections import defaultdict +from fractions import Fraction import sys from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t @@ -1503,6 +1505,99 @@ cdef class Term: term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm) return term + def toPythonObj(self): + ''' + Converts a constant value Term to a Python object. + Requires isConst to hold. + + Currently supports: + Boolean -- returns a Python bool + Int -- returns a Python int + Real -- returns a Python Fraction + BV -- returns a Python int (treats BV as unsigned) + Array -- returns a Python dict mapping indices to values + -- the constant base is returned as the default value + ''' + + if not self.isConst(): + raise RuntimeError("Cannot call toPythonObj on a non-const Term") + + string_repr = self.cterm.toString().decode() + assert string_repr + sort = self.getSort() + res = None + if sort.isBoolean(): + if string_repr == "true": + res = True + else: + assert string_repr == "false" + res = False + elif sort.isInteger(): + updated_string_repr = string_repr.strip('()').replace(' ', '') + try: + res = int(updated_string_repr) + 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) + # note: a or b could be negated: (- a) + splits = [s.strip('()/') + for s in updated_string_repr.strip('()/') \ + .replace('(- ', '(-').split()] + assert len(splits) == 2 + num = int(splits[0]) + den = int(splits[1]) + res = Fraction(num, den) + except: + raise ValueError("Failed to convert " + "{} to a Fraction".format(string_repr)) + + elif sort.isBitVector(): + # expecting format #b + assert string_repr[:2] == "#b" + python_bin_repr = "0" + string_repr[1:] + try: + res = int(python_bin_repr, 2) + except: + raise ValueError("Failed to convert bitvector " + "{} to an int".format(string_repr)) + elif sort.isArray(): + keys = [] + values = [] + base_value = None + to_visit = [self] + # Array models are represented as a series of store operations + # on a constant array + while to_visit: + t = to_visit.pop() + if t.getKind() == kinds.Store: + # save the mappings + keys.append(t[1].toPythonObj()) + values.append(t[2].toPythonObj()) + to_visit.append(t[0]) + else: + assert t.getKind() == kinds.ConstArray + base_value = t.getConstArrayBase().toPythonObj() + + assert len(keys) == len(values) + assert base_value is not None + + # put everything in a dictionary with the constant + # base as the result for any index not included in the stores + res = defaultdict(lambda : base_value) + for k, v in zip(keys, values): + res[k] = v + else: + raise ValueError("Cannot convert term {}" + " of sort {} to Python object".format(string_repr, + sort)) + + assert res is not None + return res + # Generate rounding modes cdef __rounding_modes = { diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py new file mode 100644 index 000000000..69b7b9228 --- /dev/null +++ b/test/unit/api/python/test_to_python_obj.py @@ -0,0 +1,66 @@ +from fractions import Fraction +import pytest + +import pycvc4 +from pycvc4 import kinds + + +def testGetBool(): + solver = pycvc4.Solver() + t = solver.mkTrue() + f = solver.mkFalse() + assert t.toPythonObj() == True + assert f.toPythonObj() == False + + +def testGetInt(): + solver = pycvc4.Solver() + two = solver.mkReal(2) + assert two.toPythonObj() == 2 + + +def testGetReal(): + solver = pycvc4.Solver() + half = solver.mkReal("1/2") + assert half.toPythonObj() == Fraction(1, 2) + + neg34 = solver.mkReal("-3/4") + assert neg34.toPythonObj() == Fraction(-3, 4) + + neg1 = solver.mkReal("-1") + assert neg1.toPythonObj() == -1 + + +def testGetBV(): + solver = pycvc4.Solver() + three = solver.mkBitVector(8, 3) + assert three.toPythonObj() == 3 + + +def testGetArray(): + solver = pycvc4.Solver() + arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) + zero_array = solver.mkConstArray(arrsort, solver.mkReal(0)) + stores = solver.mkTerm(kinds.Store, zero_array, solver.mkReal(1), solver.mkReal(2)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(2), solver.mkReal(3)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkReal(4), solver.mkReal(5)) + + assert stores.isConst() + + array_dict = stores.toPythonObj() + + print(array_dict) + + assert array_dict[1] == 2 + assert array_dict[2] == 3 + assert array_dict[4] == 5 + # an index that wasn't stored at should give zero + assert array_dict[8] == 0 + + +def testGetSymbol(): + solver = pycvc4.Solver() + x = solver.mkConst(solver.getBooleanSort(), "x") + + with pytest.raises(RuntimeError): + x.toPythonObj()