summaryrefslogtreecommitdiff
path: root/test/api/python
diff options
context:
space:
mode:
Diffstat (limited to 'test/api/python')
-rw-r--r--test/api/python/CMakeLists.txt10
-rw-r--r--test/api/python/test_datatype_api.py6
-rw-r--r--test/api/python/test_grammar.py20
-rw-r--r--test/api/python/test_term.py16
-rw-r--r--test/api/python/test_to_python_obj.py20
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()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback