diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-02 09:47:09 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-02 16:47:09 +0000 |
commit | 338982182dbdabecf6f3b06e659621cf43bed916 (patch) | |
tree | 37c43593a6573c443457ba55bfbd74385cae771c /test/python | |
parent | e1d476724171293d324ea9f144d1171d9b36b571 (diff) |
Move `toPythonObj` tests to the new API unit test directory (#6656)
This is the last test file that we move from the old directory to the new one, and so the old directory is deleted.
Diffstat (limited to 'test/python')
-rw-r--r-- | test/python/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/python/unit/api/test_to_python_obj.py | 118 |
2 files changed, 119 insertions, 0 deletions
diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt index 88fd817f2..54134b510 100644 --- a/test/python/CMakeLists.txt +++ b/test/python/CMakeLists.txt @@ -32,3 +32,4 @@ cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py) cvc5_add_python_api_test(pytest_term unit/api/test_term.py) cvc5_add_python_api_test(pytest_datatype_api unit/api/test_datatype_api.py) cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py) +cvc5_add_python_api_test(pytest_to_python_obj unit/api/test_to_python_obj.py) diff --git a/test/python/unit/api/test_to_python_obj.py b/test/python/unit/api/test_to_python_obj.py new file mode 100644 index 000000000..2ba685d50 --- /dev/null +++ b/test/python/unit/api/test_to_python_obj.py @@ -0,0 +1,118 @@ +############################################################################### +# Top contributors (to current version): +# Makai Mann, Andres Noetzli, Mudathir Mohamed +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +## + +from fractions import Fraction +import pytest + +import pycvc5 +from pycvc5 import kinds + + +def testGetBool(): + solver = pycvc5.Solver() + t = solver.mkTrue() + f = solver.mkFalse() + assert t.toPythonObj() == True + assert f.toPythonObj() == False + + +def testGetInt(): + solver = pycvc5.Solver() + two = solver.mkInteger(2) + assert two.toPythonObj() == 2 + + +def testGetReal(): + solver = pycvc5.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.mkInteger("-1") + assert neg1.toPythonObj() == -1 + + +def testGetBV(): + solver = pycvc5.Solver() + three = solver.mkBitVector(8, 3) + assert three.toPythonObj() == 3 + + +def testGetArray(): + solver = pycvc5.Solver() + arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort()) + zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0)) + stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(2), solver.mkInteger(3)) + stores = solver.mkTerm(kinds.Store, stores, solver.mkInteger(4), solver.mkInteger(5)) + + array_dict = stores.toPythonObj() + + 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 = pycvc5.Solver() + solver.mkConst(solver.getBooleanSort(), "x") + + +def testGetString(): + solver = pycvc5.Solver() + + s1 = '"test\n"đ\\u{a}' + t1 = solver.mkString(s1) + assert s1 == t1.toPythonObj() + + 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() == float(Fraction("8.33")) |