From ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 21 Apr 2021 10:21:34 -0700 Subject: Goodbye CVC4, hello cvc5! (#6371) This commits changes the build system to cvc5 and removes the remaining occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/. --- test/api/CMakeLists.txt | 21 ++++++++++----------- test/api/boilerplate.cpp | 2 +- test/api/interactive_shell.py | 2 +- test/api/python/CMakeLists.txt | 10 +++++----- test/api/python/test_datatype_api.py | 6 +++--- test/api/python/test_grammar.py | 20 ++++++++++---------- test/api/python/test_term.py | 16 ++++++++-------- test/api/python/test_to_python_obj.py | 20 ++++++++++---------- test/api/sep_log_api.cpp | 4 ++-- 9 files changed, 50 insertions(+), 51 deletions(-) (limited to 'test/api') diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 48318012f..b340ec8ba 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -29,10 +29,9 @@ add_custom_target(apitests COMMAND ctest --output-on-failure -L "api" -j${CTEST_NTHREADS} $$ARGS DEPENDS build-apitests) -set(CVC5_API_TEST_FLAGS - -D__BUILDING_CVC5_API_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) +set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST) -macro(cvc4_add_api_test name) +macro(cvc5_add_api_test name) set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/) add_executable(${name} ${name}.cpp) target_link_libraries(${name} PUBLIC main-test) @@ -44,14 +43,14 @@ macro(cvc4_add_api_test name) add_dependencies(build-apitests ${name}) endmacro() -cvc4_add_api_test(boilerplate) -cvc4_add_api_test(ouroborous) -cvc4_add_api_test(reset_assertions) -cvc4_add_api_test(sep_log_api) -cvc4_add_api_test(smt2_compliance) -cvc4_add_api_test(two_solvers) -cvc4_add_api_test(issue5074) -cvc4_add_api_test(issue4889) +cvc5_add_api_test(boilerplate) +cvc5_add_api_test(ouroborous) +cvc5_add_api_test(reset_assertions) +cvc5_add_api_test(sep_log_api) +cvc5_add_api_test(smt2_compliance) +cvc5_add_api_test(two_solvers) +cvc5_add_api_test(issue5074) +cvc5_add_api_test(issue4889) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) diff --git a/test/api/boilerplate.cpp b/test/api/boilerplate.cpp index 74714a753..0f561e7cf 100644 --- a/test/api/boilerplate.cpp +++ b/test/api/boilerplate.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple start-up/tear-down test for CVC4. + * A simple start-up/tear-down test for cvc5. * * This simple test just makes sure that the public interface is * minimally functional. It is useful as a template to use for other diff --git a/test/api/interactive_shell.py b/test/api/interactive_shell.py index 3c8a1d5a8..c09f5f08b 100644 --- a/test/api/interactive_shell.py +++ b/test/api/interactive_shell.py @@ -24,7 +24,7 @@ def check_iteractive_shell(): """ # Open cvc5 - child = pexpect.spawnu("bin/cvc4", timeout=1) + child = pexpect.spawnu("bin/cvc5", timeout=1) # We expect to see the cvc5 prompt child.expect("cvc5>") 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//myapitest' # and run it with 'ctest -R "api//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() diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp index c01d16bfc..04d4ce41d 100644 --- a/test/api/sep_log_api.cpp +++ b/test/api/sep_log_api.cpp @@ -37,7 +37,7 @@ int validate_exception(void) Solver slv; /* - * Setup some options for CVC4 -- we explictly want to use a simplistic + * Setup some options for cvc5 -- we explictly want to use a simplistic * theory (e.g., QF_IDL) */ slv.setLogic("QF_IDL"); @@ -129,7 +129,7 @@ int validate_getters(void) { Solver slv; - /* Setup some options for CVC4 */ + /* Setup some options for cvc5 */ slv.setLogic("QF_ALL_SUPPORTED"); slv.setOption("produce-models", "true"); slv.setOption("incremental", "false"); -- cgit v1.2.3