diff options
Diffstat (limited to 'test/api/python')
-rw-r--r-- | test/api/python/CMakeLists.txt | 10 | ||||
-rw-r--r-- | test/api/python/test_datatype_api.py | 6 | ||||
-rw-r--r-- | test/api/python/test_grammar.py | 20 | ||||
-rw-r--r-- | test/api/python/test_term.py | 16 | ||||
-rw-r--r-- | test/api/python/test_to_python_obj.py | 20 |
5 files changed, 36 insertions, 36 deletions
diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index d6d14b310..246755492 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -27,7 +27,7 @@ if(RET_PYTEST) "Could not find Python module pytest. Install via `pip install pytest'.") endif() -macro(cvc4_add_python_api_test name filename) +macro(cvc5_add_python_api_test name filename) # we create test target 'api/<output_dir>/myapitest' # and run it with 'ctest -R "api/<output_dir>/myapitest"'. @@ -38,7 +38,7 @@ macro(cvc4_add_python_api_test name filename) endmacro() -cvc4_add_python_api_test(pytest_datatype_api test_datatype_api.py) -cvc4_add_python_api_test(pytest_grammar test_grammar.py) -cvc4_add_python_api_test(pytest_term test_term.py) -cvc4_add_python_api_test(pytest_to_python_obj test_to_python_obj.py) +cvc5_add_python_api_test(pytest_datatype_api test_datatype_api.py) +cvc5_add_python_api_test(pytest_grammar test_grammar.py) +cvc5_add_python_api_test(pytest_term test_term.py) +cvc5_add_python_api_test(pytest_to_python_obj test_to_python_obj.py) diff --git a/test/api/python/test_datatype_api.py b/test/api/python/test_datatype_api.py index 81c5478e8..06f4e0f3d 100644 --- a/test/api/python/test_datatype_api.py +++ b/test/api/python/test_datatype_api.py @@ -13,12 +13,12 @@ import pytest -import pycvc4 -from pycvc4 import kinds +import pycvc5 +from pycvc5 import kinds def test_datatype_simply_rec(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() # Create mutual datatypes corresponding to this definition block: # diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py index 30f01b59f..f83bee548 100644 --- a/test/api/python/test_grammar.py +++ b/test/api/python/test_grammar.py @@ -15,15 +15,15 @@ import pytest -import pycvc4 -from pycvc4 import kinds +import pycvc5 +from pycvc5 import kinds def test_add_rule(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() boolean = solver.getBooleanSort() integer = solver.getIntegerSort() - nullTerm = pycvc4.Term(solver) + nullTerm = pycvc5.Term(solver) start = solver.mkVar(boolean) nts = solver.mkVar(boolean) @@ -50,11 +50,11 @@ def test_add_rule(): g.addRule(start, solver.mkBoolean(false)) def test_add_rules(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() boolean = solver.getBooleanSort() integer = solver.getIntegerSort() - nullTerm = pycvc4.Term(solver) + nullTerm = pycvc5.Term(solver) start = solver.mkVar(boolean) nts = solver.mkVar(boolean) @@ -79,10 +79,10 @@ def test_add_rules(): g.addRules(start, solver.mkBoolean(False)) def testAddAnyConstant(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() boolean = solver.getBooleanSort() - nullTerm = pycvc4.Term(solver) + nullTerm = pycvc5.Term(solver) start = solver.mkVar(boolean) nts = solver.mkVar(boolean) @@ -103,10 +103,10 @@ def testAddAnyConstant(): def testAddAnyVariable(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() boolean = solver.getBooleanSort() - nullTerm = pycvc4.Term(solver) + nullTerm = pycvc5.Term(solver) x = solver.mkVar(boolean) start = solver.mkVar(boolean) nts = solver.mkVar(boolean) diff --git a/test/api/python/test_term.py b/test/api/python/test_term.py index e47caaf5c..c0625095b 100644 --- a/test/api/python/test_term.py +++ b/test/api/python/test_term.py @@ -13,12 +13,12 @@ import pytest -import pycvc4 -from pycvc4 import kinds +import pycvc5 +from pycvc5 import kinds def test_getitem(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() intsort = solver.getIntegerSort() x = solver.mkConst(intsort, 'x') y = solver.mkConst(intsort, 'y') @@ -29,7 +29,7 @@ def test_getitem(): def test_get_kind(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() intsort = solver.getIntegerSort() x = solver.mkConst(intsort, 'x') y = solver.mkConst(intsort, 'y') @@ -52,7 +52,7 @@ def test_get_kind(): def test_eq(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() usort = solver.mkUninterpretedSort('u') x = solver.mkConst(usort, 'x') y = solver.mkConst(usort, 'y') @@ -66,7 +66,7 @@ def test_eq(): def test_get_sort(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() intsort = solver.getIntegerSort() bvsort8 = solver.mkBitVectorSort(8) @@ -83,7 +83,7 @@ def test_get_sort(): assert solver.mkTerm(kinds.BVConcat, a, b).getSort() == solver.mkBitVectorSort(16) def test_get_op(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() intsort = solver.getIntegerSort() funsort = solver.mkFunctionSort(intsort, intsort) @@ -107,7 +107,7 @@ def test_get_op(): def test_const_sequence_elements(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() realsort = solver.getRealSort() seqsort = solver.mkSequenceSort(realsort) s = solver.mkEmptySequence(seqsort) diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py index 5d55201de..d8094f801 100644 --- a/test/api/python/test_to_python_obj.py +++ b/test/api/python/test_to_python_obj.py @@ -14,12 +14,12 @@ from fractions import Fraction import pytest -import pycvc4 -from pycvc4 import kinds +import pycvc5 +from pycvc5 import kinds def testGetBool(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() t = solver.mkTrue() f = solver.mkFalse() assert t.toPythonObj() == True @@ -27,13 +27,13 @@ def testGetBool(): def testGetInt(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() two = solver.mkInteger(2) assert two.toPythonObj() == 2 def testGetReal(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() half = solver.mkReal("1/2") assert half.toPythonObj() == Fraction(1, 2) @@ -45,13 +45,13 @@ def testGetReal(): def testGetBV(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() three = solver.mkBitVector(8, 3) assert three.toPythonObj() == 3 def testGetArray(): - solver = pycvc4.Solver() + 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)) @@ -68,17 +68,17 @@ def testGetArray(): def testGetSymbol(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() solver.mkConst(solver.getBooleanSort(), "x") def testGetString(): - solver = pycvc4.Solver() + solver = pycvc5.Solver() s1 = '"test\n"đ\\u{a}' t1 = solver.mkString(s1) assert s1 == t1.toPythonObj() - s2 = 'â¤ď¸CVC4â¤ď¸' + s2 = 'â¤ď¸cvc5â¤ď¸' t2 = solver.mkString(s2) assert s2 == t2.toPythonObj() |