diff options
Diffstat (limited to 'test/unit/api')
24 files changed, 4996 insertions, 23 deletions
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index ae6db51ef..0701c3ca6 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -13,17 +13,10 @@ # The build system configuration. ## -# Add unit tests. -cvc5_add_unit_test_black(datatype_api_black api) -cvc5_add_unit_test_black(grammar_black api) -cvc5_add_unit_test_black(op_black api) -cvc5_add_unit_test_white(op_white api) -cvc5_add_unit_test_black(result_black api) -cvc5_add_unit_test_black(solver_black api) -cvc5_add_unit_test_white(solver_white api) -cvc5_add_unit_test_black(sort_black api) -cvc5_add_unit_test_black(term_black api) -cvc5_add_unit_test_white(term_white api) +add_subdirectory(cpp) +if (BUILD_BINDINGS_PYTHON) + add_subdirectory(python) +endif() if (BUILD_BINDINGS_JAVA) add_subdirectory(java) endif() diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt new file mode 100644 index 000000000..e99732ca4 --- /dev/null +++ b/test/unit/api/cpp/CMakeLists.txt @@ -0,0 +1,24 @@ +############################################################################### +# Top contributors (to current version): +# Aina Niemetz +# +# 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. +# ############################################################################# +# +# The build system configuration. +## +cvc5_add_unit_test_black(datatype_api_black api) +cvc5_add_unit_test_black(grammar_black api) +cvc5_add_unit_test_black(op_black api) +cvc5_add_unit_test_white(op_white api) +cvc5_add_unit_test_black(result_black api) +cvc5_add_unit_test_black(solver_black api) +cvc5_add_unit_test_white(solver_white api) +cvc5_add_unit_test_black(sort_black api) +cvc5_add_unit_test_black(term_black api) +cvc5_add_unit_test_white(term_white api) diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 745abc17c..745abc17c 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp index 7b7556539..7b7556539 100644 --- a/test/unit/api/grammar_black.cpp +++ b/test/unit/api/cpp/grammar_black.cpp diff --git a/test/unit/api/op_black.cpp b/test/unit/api/cpp/op_black.cpp index fd45b1c22..fd45b1c22 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp diff --git a/test/unit/api/op_white.cpp b/test/unit/api/cpp/op_white.cpp index 39952739b..39952739b 100644 --- a/test/unit/api/op_white.cpp +++ b/test/unit/api/cpp/op_white.cpp diff --git a/test/unit/api/result_black.cpp b/test/unit/api/cpp/result_black.cpp index 9bf6b8491..9bf6b8491 100644 --- a/test/unit/api/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 79a4aa63e..51a0f38b5 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -15,8 +15,8 @@ #include <algorithm> -#include "test_api.h" #include "base/output.h" +#include "test_api.h" namespace cvc5 { @@ -341,9 +341,12 @@ TEST_F(TestApiBlackSolver, mkBitVector) ASSERT_EQ(d_solver.mkBitVector(8, "0101", 2), d_solver.mkBitVector(8, "00000101", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), d_solver.mkBitVector(4, "1111", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), d_solver.mkBitVector(4, "1111", 2)); - ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 2), + d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 16), + d_solver.mkBitVector(4, "1111", 2)); + ASSERT_EQ(d_solver.mkBitVector(4, "-1", 10), + d_solver.mkBitVector(4, "1111", 2)); ASSERT_EQ(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101"); ASSERT_EQ(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111"); ASSERT_EQ(d_solver.mkBitVector(8, "-1", 10), @@ -592,12 +595,11 @@ TEST_F(TestApiBlackSolver, mkReal) ASSERT_NO_THROW(d_solver.mkReal(val4, val4)); } -TEST_F(TestApiBlackSolver, mkRegexpNone) +TEST_F(TestApiBlackSolver, mkRegexpAll) { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); - ASSERT_NO_THROW( - d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); + ASSERT_NO_THROW(d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); } TEST_F(TestApiBlackSolver, mkRegexpAllchar) @@ -608,6 +610,14 @@ TEST_F(TestApiBlackSolver, mkRegexpAllchar) d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); } +TEST_F(TestApiBlackSolver, mkRegexpNone) +{ + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + ASSERT_NO_THROW( + d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); +} + TEST_F(TestApiBlackSolver, mkSepEmp) { ASSERT_NO_THROW(d_solver.mkSepEmp()); } TEST_F(TestApiBlackSolver, mkSepNil) @@ -1351,7 +1361,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo) api::OptionInfo info = d_solver.getOptionInfo("verbosity"); EXPECT_EQ("verbosity", info.name); EXPECT_EQ(std::vector<std::string>{}, info.aliases); - EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(info.valueInfo)); + EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>( + info.valueInfo)); auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(info.valueInfo); EXPECT_EQ(0, numInfo.defaultValue); EXPECT_EQ(0, numInfo.currentValue); @@ -1362,7 +1373,8 @@ TEST_F(TestApiBlackSolver, getOptionInfo) auto info = d_solver.getOptionInfo("random-freq"); ASSERT_EQ(info.name, "random-freq"); ASSERT_EQ(info.aliases, std::vector<std::string>{"random-frequency"}); - ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>(info.valueInfo)); + ASSERT_TRUE(std::holds_alternative<api::OptionInfo::NumberInfo<double>>( + info.valueInfo)); auto ni = std::get<api::OptionInfo::NumberInfo<double>>(info.valueInfo); ASSERT_EQ(ni.currentValue, 0.0); ASSERT_EQ(ni.defaultValue, 0.0); @@ -2540,7 +2552,6 @@ TEST_F(TestApiBlackSolver, Output) ASSERT_NE(cvc5::null_os.rdbuf(), d_solver.getOutput("inst").rdbuf()); } - TEST_F(TestApiBlackSolver, issue7000) { Sort s1 = d_solver.getIntegerSort(); diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 5d7b9eacf..5d7b9eacf 100644 --- a/test/unit/api/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index d0c755cf7..d0c755cf7 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp diff --git a/test/unit/api/term_black.cpp b/test/unit/api/cpp/term_black.cpp index 9e52174b4..c76182e47 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -212,6 +212,21 @@ TEST_F(TestApiBlackTerm, getOp) ASSERT_EQ(headTerm, d_solver.mkTerm(headTerm.getOp(), children)); } +TEST_F(TestApiBlackTerm, hasGetSymbol) +{ + Term n; + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + ASSERT_THROW(n.hasSymbol(), CVC5ApiException); + ASSERT_FALSE(t.hasSymbol()); + ASSERT_TRUE(c.hasSymbol()); + + ASSERT_THROW(n.getSymbol(), CVC5ApiException); + ASSERT_THROW(t.getSymbol(), CVC5ApiException); + ASSERT_EQ(c.getSymbol(), "|\\|"); +} + TEST_F(TestApiBlackTerm, isNull) { Term x; @@ -807,10 +822,12 @@ TEST_F(TestApiBlackTerm, getReal) ASSERT_EQ((std::pair<int64_t, uint64_t>(127, 10)), real5.getReal64Value()); ASSERT_EQ("127/10", real5.getRealValue()); - ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), real6.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(1, 4294967297)), + real6.getReal64Value()); ASSERT_EQ("1/4294967297", real6.getRealValue()); - ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), real7.getReal64Value()); + ASSERT_EQ((std::pair<int64_t, uint64_t>(4294967297, 1)), + real7.getReal64Value()); ASSERT_EQ("4294967297/1", real7.getRealValue()); ASSERT_EQ("1/18446744073709551617", real8.getRealValue()); diff --git a/test/unit/api/term_white.cpp b/test/unit/api/cpp/term_white.cpp index ace5645dc..ace5645dc 100644 --- a/test/unit/api/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 161854421..6a08d79c6 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -639,6 +639,13 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); } + @Test void mkRegexpAll() + { + Sort strSort = d_solver.getStringSort(); + Term s = d_solver.mkConst(strSort, "s"); + assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); + } + @Test void mkRegexpAllchar() { Sort strSort = d_solver.getStringSort(); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index bf0beb024..b7f111428 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -219,6 +219,21 @@ class TermTest Term nilOpTerm = list.getConstructorTerm("nil"); } + @Test void hasGetSymbol() throws CVC5ApiException + { + Term n = d_solver.getNullTerm(); + Term t = d_solver.mkBoolean(true); + Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|"); + + assertThrows(CVC5ApiException.class, () -> n.hasSymbol()); + assertFalse(t.hasSymbol()); + assertTrue(c.hasSymbol()); + + assertThrows(CVC5ApiException.class, () -> n.getSymbol()); + assertThrows(CVC5ApiException.class, () -> t.getSymbol()); + assertEquals(c.getSymbol(), "|\\|"); + } + @Test void isNull() throws CVC5ApiException { Term x = d_solver.getNullTerm(); diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt new file mode 100644 index 000000000..cbf9629ce --- /dev/null +++ b/test/unit/api/python/CMakeLists.txt @@ -0,0 +1,40 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Aina Niemetz, Mathias Preiner +# +# 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. +# ############################################################################# +# +# The build system configuration. +## + +# Check if the pytest Python module is installed. +check_python_module("pytest") + +# Add Python bindings API tests. +macro(cvc5_add_python_api_unit_test name filename) +# We create test target 'python/unit/api/myapitest' and run it with +# 'ctest -R "python/unit/api/myapitest"'. + set(test_name unit/api/python/${name}) + add_test (NAME ${test_name} + COMMAND ${PYTHON_EXECUTABLE} + -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename} + # directory for importing the python bindings + WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") +endmacro() + +# add specific test files +cvc5_add_python_api_unit_test(pytest_solver test_solver.py) +cvc5_add_python_api_unit_test(pytest_sort test_sort.py) +cvc5_add_python_api_unit_test(pytest_term test_term.py) +cvc5_add_python_api_unit_test(pytest_datatype_api test_datatype_api.py) +cvc5_add_python_api_unit_test(pytest_grammar test_grammar.py) +cvc5_add_python_api_unit_test(pytest_to_python_obj test_to_python_obj.py) +cvc5_add_python_api_unit_test(pytest_op test_op.py) +cvc5_add_python_api_unit_test(pytest_result test_result.py) diff --git a/test/unit/api/python/__init__.py b/test/unit/api/python/__init__.py new file mode 100644 index 000000000..e69de29bb --- /dev/null +++ b/test/unit/api/python/__init__.py diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py new file mode 100644 index 000000000..d8a4c26f7 --- /dev/null +++ b/test/unit/api/python/test_datatype_api.py @@ -0,0 +1,566 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar +# +# 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. +# ############################################################################# +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort, Term +from pycvc5 import DatatypeDecl +from pycvc5 import Datatype +from pycvc5 import DatatypeConstructorDecl +from pycvc5 import DatatypeConstructor +from pycvc5 import DatatypeSelector + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_mk_datatype_sort(solver): + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + listSort = solver.mkDatatypeSort(dtypeSpec) + d = listSort.getDatatype() + consConstr = d[0] + nilConstr = d[1] + with pytest.raises(RuntimeError): + d[2] + consConstr.getConstructorTerm() + nilConstr.getConstructorTerm() + +def test_is_null(solver): + # creating empty (null) objects. + dtypeSpec = DatatypeDecl(solver) + cons = DatatypeConstructorDecl(solver) + d = Datatype(solver) + consConstr = DatatypeConstructor(solver) + sel = DatatypeSelector(solver) + + # verifying that the objects are considered null. + assert dtypeSpec.isNull() + assert cons.isNull() + assert d.isNull() + assert consConstr.isNull() + assert sel.isNull() + + # changing the objects to be non-null + dtypeSpec = solver.mkDatatypeDecl("list"); + cons = solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", solver.getIntegerSort()); + dtypeSpec.addConstructor(cons); + listSort = solver.mkDatatypeSort(dtypeSpec) + d = listSort.getDatatype(); + consConstr = d[0]; + sel = consConstr[0]; + + # verifying that the new objects are non-null + assert not dtypeSpec.isNull() + assert not cons.isNull() + assert not d.isNull() + assert not consConstr.isNull() + assert not sel.isNull() + +def test_mk_datatype_sorts(solver): + # Create two mutual datatypes corresponding to this definition + # block: + # + # DATATYPE + # tree = node(left: tree, right: tree) | leaf(data: list), + # list = cons(car: tree, cdr: list) | nil + # END + # + + #Make unresolved types as placeholders + unresTypes = set([]) + unresTree = solver.mkUninterpretedSort("tree") + unresList = solver.mkUninterpretedSort("list") + unresTypes.add(unresTree) + unresTypes.add(unresList) + + tree = solver.mkDatatypeDecl("tree") + node = solver.mkDatatypeConstructorDecl("node") + node.addSelector("left", unresTree) + node.addSelector("right", unresTree) + tree.addConstructor(node) + + leaf = solver.mkDatatypeConstructorDecl("leaf") + leaf.addSelector("data", unresList) + tree.addConstructor(leaf) + + llist = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("car", unresTree) + cons.addSelector("cdr", unresTree) + llist.addConstructor(cons) + + nil = solver.mkDatatypeConstructorDecl("nil") + llist.addConstructor(nil) + + dtdecls = [] + dtdecls.append(tree) + dtdecls.append(llist) + dtsorts = [] + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == len(dtdecls) + for i in range(0, len(dtdecls)): + assert dtsorts[i].isDatatype() + assert not dtsorts[i].getDatatype().isFinite() + assert dtsorts[i].getDatatype().getName() == dtdecls[i].getName() + # verify the resolution was correct + dtTree = dtsorts[0].getDatatype() + dtcTreeNode = dtTree[0] + assert dtcTreeNode.getName() == "node" + dtsTreeNodeLeft = dtcTreeNode[0] + assert dtsTreeNodeLeft.getName() == "left" + # argument type should have resolved to be recursive + assert dtsTreeNodeLeft.getRangeSort().isDatatype() + assert dtsTreeNodeLeft.getRangeSort() == dtsorts[0] + + # fails due to empty datatype + dtdeclsBad = [] + emptyD = solver.mkDatatypeDecl("emptyD") + dtdeclsBad.append(emptyD) + with pytest.raises(RuntimeError): + solver.mkDatatypeSorts(dtdeclsBad) + + +def test_datatype_structs(solver): + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + + # create datatype sort to test + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", intSort) + cons.addSelectorSelf("tail") + nullSort = Sort(solver) + with pytest.raises(RuntimeError): + cons.addSelector("null", nullSort) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + dt = dtypeSort.getDatatype() + assert not dt.isCodatatype() + assert not dt.isTuple() + assert not dt.isRecord() + assert not dt.isFinite() + assert dt.isWellFounded() + # get constructor + dcons = dt[0] + consTerm = dcons.getConstructorTerm() + assert dcons.getNumSelectors() == 2 + + # create datatype sort to test + dtypeSpecEnum = solver.mkDatatypeDecl("enum") + ca = solver.mkDatatypeConstructorDecl("A") + dtypeSpecEnum.addConstructor(ca) + cb = solver.mkDatatypeConstructorDecl("B") + dtypeSpecEnum.addConstructor(cb) + cc = solver.mkDatatypeConstructorDecl("C") + dtypeSpecEnum.addConstructor(cc) + dtypeSortEnum = solver.mkDatatypeSort(dtypeSpecEnum) + dtEnum = dtypeSortEnum.getDatatype() + assert not dtEnum.isTuple() + assert dtEnum.isFinite() + + # create codatatype + dtypeSpecStream = solver.mkDatatypeDecl("stream", True) + consStream = solver.mkDatatypeConstructorDecl("cons") + consStream.addSelector("head", intSort) + consStream.addSelectorSelf("tail") + dtypeSpecStream.addConstructor(consStream) + dtypeSortStream = solver.mkDatatypeSort(dtypeSpecStream) + dtStream = dtypeSortStream.getDatatype() + assert dtStream.isCodatatype() + assert not dtStream.isFinite() + # codatatypes may be well-founded + assert dtStream.isWellFounded() + + # create tuple + tupSort = solver.mkTupleSort([boolSort]) + dtTuple = tupSort.getDatatype() + assert dtTuple.isTuple() + assert not dtTuple.isRecord() + assert dtTuple.isFinite() + assert dtTuple.isWellFounded() + + # create record + fields = [("b", boolSort), ("i", intSort)] + recSort = solver.mkRecordSort(fields) + assert recSort.isDatatype() + dtRecord = recSort.getDatatype() + assert not dtRecord.isTuple() + assert dtRecord.isRecord() + assert not dtRecord.isFinite() + assert dtRecord.isWellFounded() + + +def test_datatype_names(solver): + intSort = solver.getIntegerSort() + + # create datatype sort to test + dtypeSpec = solver.mkDatatypeDecl("list") + dtypeSpec.getName() + assert dtypeSpec.getName() == "list" + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", intSort) + cons.addSelectorSelf("tail") + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + dt = dtypeSort.getDatatype() + assert dt.getName() == "list" + dt.getConstructor("nil") + dt["cons"] + with pytest.raises(RuntimeError): + dt.getConstructor("head") + with pytest.raises(RuntimeError): + dt.getConstructor("") + + dcons = dt[0] + assert dcons.getName() == "cons" + dcons.getSelector("head") + dcons["tail"] + with pytest.raises(RuntimeError): + dcons.getSelector("cons") + + # get selector + dselTail = dcons[1] + assert dselTail.getName() == "tail" + assert dselTail.getRangeSort() == dtypeSort + + # get selector from datatype + dt.getSelector("head") + with pytest.raises(RuntimeError): + dt.getSelector("cons") + + # possible to construct null datatype declarations if not using mkDatatypeDecl + with pytest.raises(RuntimeError): + DatatypeDecl(solver).getName() + + +def test_parametric_datatype(solver): + v = [] + t1 = solver.mkParamSort("T1") + t2 = solver.mkParamSort("T2") + v.append(t1) + v.append(t2) + pairSpec = solver.mkDatatypeDecl("pair", v) + + mkpair = solver.mkDatatypeConstructorDecl("mk-pair") + mkpair.addSelector("first", t1) + mkpair.addSelector("second", t2) + pairSpec.addConstructor(mkpair) + + pairType = solver.mkDatatypeSort(pairSpec) + + assert pairType.getDatatype().isParametric() + + v.clear() + v.append(solver.getIntegerSort()) + v.append(solver.getIntegerSort()) + pairIntInt = pairType.instantiate(v) + v.clear() + v.append(solver.getRealSort()) + v.append(solver.getRealSort()) + pairRealReal = pairType.instantiate(v) + v.clear() + v.append(solver.getRealSort()) + v.append(solver.getIntegerSort()) + pairRealInt = pairType.instantiate(v) + v.clear() + v.append(solver.getIntegerSort()) + v.append(solver.getRealSort()) + pairIntReal = pairType.instantiate(v) + + assert pairIntInt != pairRealReal + assert pairIntReal != pairRealReal + assert pairRealInt != pairRealReal + assert pairIntInt != pairIntReal + assert pairIntInt != pairRealInt + assert pairIntReal != pairRealInt + + assert pairRealReal.isComparableTo(pairRealReal) + assert not pairIntReal.isComparableTo(pairRealReal) + assert not pairRealInt.isComparableTo(pairRealReal) + assert not pairIntInt.isComparableTo(pairRealReal) + assert not pairRealReal.isComparableTo(pairRealInt) + assert not pairIntReal.isComparableTo(pairRealInt) + assert pairRealInt.isComparableTo(pairRealInt) + assert not pairIntInt.isComparableTo(pairRealInt) + assert not pairRealReal.isComparableTo(pairIntReal) + assert pairIntReal.isComparableTo(pairIntReal) + assert not pairRealInt.isComparableTo(pairIntReal) + assert not pairIntInt.isComparableTo(pairIntReal) + assert not pairRealReal.isComparableTo(pairIntInt) + assert not pairIntReal.isComparableTo(pairIntInt) + assert not pairRealInt.isComparableTo(pairIntInt) + assert pairIntInt.isComparableTo(pairIntInt) + + assert pairRealReal.isSubsortOf(pairRealReal) + assert not pairIntReal.isSubsortOf(pairRealReal) + assert not pairRealInt.isSubsortOf(pairRealReal) + assert not pairIntInt.isSubsortOf(pairRealReal) + assert not pairRealReal.isSubsortOf(pairRealInt) + assert not pairIntReal.isSubsortOf(pairRealInt) + assert pairRealInt.isSubsortOf(pairRealInt) + assert not pairIntInt.isSubsortOf(pairRealInt) + assert not pairRealReal.isSubsortOf(pairIntReal) + assert pairIntReal.isSubsortOf(pairIntReal) + assert not pairRealInt.isSubsortOf(pairIntReal) + assert not pairIntInt.isSubsortOf(pairIntReal) + assert not pairRealReal.isSubsortOf(pairIntInt) + assert not pairIntReal.isSubsortOf(pairIntInt) + assert not pairRealInt.isSubsortOf(pairIntInt) + assert pairIntInt.isSubsortOf(pairIntInt) + + +def test_datatype_simply_rec(solver): + # Create mutual datatypes corresponding to this definition block: + # + # DATATYPE + # wlist = leaf(data: list), + # list = cons(car: wlist, cdr: list) | nil, + # ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) + # END + + # Make unresolved types as placeholders + unresTypes = set([]) + unresWList = solver.mkUninterpretedSort("wlist") + unresList = solver.mkUninterpretedSort("list") + unresNs = solver.mkUninterpretedSort("ns") + unresTypes.add(unresWList) + unresTypes.add(unresList) + unresTypes.add(unresNs) + + wlist = solver.mkDatatypeDecl("wlist") + leaf = solver.mkDatatypeConstructorDecl("leaf") + leaf.addSelector("data", unresList) + wlist.addConstructor(leaf) + + llist = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("car", unresWList) + cons.addSelector("cdr", unresList) + llist.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + llist.addConstructor(nil) + + ns = solver.mkDatatypeDecl("ns") + elem = solver.mkDatatypeConstructorDecl("elem") + elem.addSelector("ndata", solver.mkSetSort(unresWList)) + ns.addConstructor(elem) + elemArray = solver.mkDatatypeConstructorDecl("elemArray") + elemArray.addSelector("ndata", solver.mkArraySort(unresList, unresList)) + ns.addConstructor(elemArray) + + dtdecls = [wlist, llist, ns] + # this is well-founded and has no nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 3 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[2].getDatatype().isWellFounded() + assert not dtsorts[0].getDatatype().hasNestedRecursion() + assert not dtsorts[1].getDatatype().hasNestedRecursion() + assert not dtsorts[2].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # ns2 = elem2(ndata: array(int,ns2)) | nil2 + # END + + unresTypes.clear() + unresNs2 = solver.mkUninterpretedSort("ns2") + unresTypes.add(unresNs2) + + ns2 = solver.mkDatatypeDecl("ns2") + elem2 = solver.mkDatatypeConstructorDecl("elem2") + elem2.addSelector("ndata", + solver.mkArraySort(solver.getIntegerSort(), unresNs2)) + ns2.addConstructor(elem2) + nil2 = solver.mkDatatypeConstructorDecl("nil2") + ns2.addConstructor(nil2) + + dtdecls.clear() + dtdecls.append(ns2) + + # this is not well-founded due to non-simple recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype()[0][0].getRangeSort().isArray() + assert dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() \ + == dtsorts[0] + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list3 = cons3(car: ns3, cdr: list3) | nil3, + # ns3 = elem3(ndata: set(list3)) + # END + + unresTypes.clear() + unresNs3 = solver.mkUninterpretedSort("ns3") + unresTypes.add(unresNs3) + unresList3 = solver.mkUninterpretedSort("list3") + unresTypes.add(unresList3) + + list3 = solver.mkDatatypeDecl("list3") + cons3 = solver.mkDatatypeConstructorDecl("cons3") + cons3.addSelector("car", unresNs3) + cons3.addSelector("cdr", unresList3) + list3.addConstructor(cons3) + nil3 = solver.mkDatatypeConstructorDecl("nil3") + list3.addConstructor(nil3) + + ns3 = solver.mkDatatypeDecl("ns3") + elem3 = solver.mkDatatypeConstructorDecl("elem3") + elem3.addSelector("ndata", solver.mkSetSort(unresList3)) + ns3.addConstructor(elem3) + + dtdecls.clear() + dtdecls.append(list3) + dtdecls.append(ns3) + + # both are well-founded and have nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 2 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + assert dtsorts[1].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list4 = cons(car: set(ns4), cdr: list4) | nil, + # ns4 = elem(ndata: list4) + # END + unresTypes.clear() + unresNs4 = solver.mkUninterpretedSort("ns4") + unresTypes.add(unresNs4) + unresList4 = solver.mkUninterpretedSort("list4") + unresTypes.add(unresList4) + + list4 = solver.mkDatatypeDecl("list4") + cons4 = solver.mkDatatypeConstructorDecl("cons4") + cons4.addSelector("car", solver.mkSetSort(unresNs4)) + cons4.addSelector("cdr", unresList4) + list4.addConstructor(cons4) + nil4 = solver.mkDatatypeConstructorDecl("nil4") + list4.addConstructor(nil4) + + ns4 = solver.mkDatatypeDecl("ns4") + elem4 = solver.mkDatatypeConstructorDecl("elem3") + elem4.addSelector("ndata", unresList4) + ns4.addConstructor(elem4) + + dtdecls.clear() + dtdecls.append(list4) + dtdecls.append(ns4) + + # both are well-founded and have nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 2 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[1].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + assert dtsorts[1].getDatatype().hasNestedRecursion() + + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil + # END + unresTypes.clear() + unresList5 = solver.mkSortConstructorSort("list5", 1) + unresTypes.add(unresList5) + + v = [] + x = solver.mkParamSort("X") + v.append(x) + list5 = solver.mkDatatypeDecl("list5", v) + + args = [x] + urListX = unresList5.instantiate(args) + args[0] = urListX + urListListX = unresList5.instantiate(args) + + cons5 = solver.mkDatatypeConstructorDecl("cons5") + cons5.addSelector("car", x) + cons5.addSelector("cdr", urListListX) + list5.addConstructor(cons5) + nil5 = solver.mkDatatypeConstructorDecl("nil5") + list5.addConstructor(nil5) + + dtdecls.clear() + dtdecls.append(list5) + + # well-founded and has nested recursion + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 1 + assert dtsorts[0].getDatatype().isWellFounded() + assert dtsorts[0].getDatatype().hasNestedRecursion() + + +def test_datatype_specialized_cons(solver): + # Create mutual datatypes corresponding to this definition block: + # DATATYPE + # plist[X] = pcons(car: X, cdr: plist[X]) | pnil + # END + + # Make unresolved types as placeholders + unresTypes = set([]) + unresList = solver.mkSortConstructorSort("plist", 1) + unresTypes.add(unresList) + + v = [] + x = solver.mkParamSort("X") + v.append(x) + plist = solver.mkDatatypeDecl("plist", v) + + args = [x] + urListX = unresList.instantiate(args) + + pcons = solver.mkDatatypeConstructorDecl("pcons") + pcons.addSelector("car", x) + pcons.addSelector("cdr", urListX) + plist.addConstructor(pcons) + nil5 = solver.mkDatatypeConstructorDecl("pnil") + plist.addConstructor(nil5) + + dtdecls = [plist] + + # make the datatype sorts + dtsorts = solver.mkDatatypeSorts(dtdecls, unresTypes) + assert len(dtsorts) == 1 + d = dtsorts[0].getDatatype() + nilc = d[0] + + isort = solver.getIntegerSort() + iargs = [isort] + listInt = dtsorts[0].instantiate(iargs) + + testConsTerm = Term(solver) + # get the specialized constructor term for list[Int] + testConsTerm = nilc.getSpecializedConstructorTerm(listInt) + assert testConsTerm != nilc.getConstructorTerm() + # error to get the specialized constructor term for Int + with pytest.raises(RuntimeError): + nilc.getSpecializedConstructorTerm(isort) diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py new file mode 100644 index 000000000..db567a6ba --- /dev/null +++ b/test/unit/api/python/test_grammar.py @@ -0,0 +1,137 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Makai Mann, 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. +# ############################################################################# +# +# Translated from test/unit/api/grammar_black.h +## + +import pytest + +import pycvc5 +from pycvc5 import kinds, Term + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_add_rule(solver): + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + null_term = Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + # expecting no error + g = solver.mkSygusGrammar([], [start]) + + g.addRule(start, solver.mkBoolean(False)) + + # expecting errors + with pytest.raises(RuntimeError): + g.addRule(null_term, solver.mkBoolean(False)) + with pytest.raises(RuntimeError): + g.addRule(start, null_term) + with pytest.raises(RuntimeError): + g.addRule(nts, solver.mkBoolean(False)) + with pytest.raises(RuntimeError): + g.addRule(start, solver.mkInteger(0)) + with pytest.raises(RuntimeError): + g.addRule(start, nts) + + # expecting no errors + solver.synthFun("f", {}, boolean, g) + + # expecting an error + with pytest.raises(RuntimeError): + g.addRule(start, solver.mkBoolean(False)) + + +def test_add_rules(solver): + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + null_term = Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar([], [start]) + + g.addRules(start, {solver.mkBoolean(False)}) + + #Expecting errors + with pytest.raises(RuntimeError): + g.addRules(null_term, [solver.mkBoolean(False)]) + with pytest.raises(RuntimeError): + g.addRules(start, [null_term]) + with pytest.raises(RuntimeError): + g.addRules(nts, [solver.mkBoolean(False)]) + with pytest.raises(RuntimeError): + g.addRules(start, [solver.mkInteger(0)]) + with pytest.raises(RuntimeError): + g.addRules(start, [nts]) + #Expecting no errors + solver.synthFun("f", {}, boolean, g) + + #Expecting an error + with pytest.raises(RuntimeError): + g.addRules(start, solver.mkBoolean(False)) + + +def test_add_any_constant(solver): + boolean = solver.getBooleanSort() + + null_term = Term(solver) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g = solver.mkSygusGrammar({}, {start}) + + g.addAnyConstant(start) + g.addAnyConstant(start) + + with pytest.raises(RuntimeError): + g.addAnyConstant(null_term) + with pytest.raises(RuntimeError): + g.addAnyConstant(nts) + + solver.synthFun("f", {}, boolean, g) + + with pytest.raises(RuntimeError): + g.addAnyConstant(start) + + +def test_add_any_variable(solver): + boolean = solver.getBooleanSort() + + null_term = Term(solver) + x = solver.mkVar(boolean) + start = solver.mkVar(boolean) + nts = solver.mkVar(boolean) + + g1 = solver.mkSygusGrammar({x}, {start}) + g2 = solver.mkSygusGrammar({}, {start}) + + g1.addAnyVariable(start) + g1.addAnyVariable(start) + g2.addAnyVariable(start) + + with pytest.raises(RuntimeError): + g1.addAnyVariable(null_term) + with pytest.raises(RuntimeError): + g1.addAnyVariable(nts) + + solver.synthFun("f", {}, boolean, g1) + + with pytest.raises(RuntimeError): + g1.addAnyVariable(start) diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py new file mode 100644 index 000000000..5126a481d --- /dev/null +++ b/test/unit/api/python/test_op.py @@ -0,0 +1,181 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar +# +# 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. +# ############################################################################# +# +# Unit tests for op API. +# +# Obtained by translating test/unit/api/op_black.cpp +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort +from pycvc5 import Op + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_get_kind(solver): + x = solver.mkOp(kinds.BVExtract, 31, 1) + x.getKind() + + +def test_is_null(solver): + x = Op(solver) + assert x.isNull() + x = solver.mkOp(kinds.BVExtract, 31, 1) + assert not x.isNull() + + +def test_op_from_kind(solver): + solver.mkOp(kinds.Plus) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract) + + +def test_get_num_indices(solver): + plus = solver.mkOp(kinds.Plus) + divisible = solver.mkOp(kinds.Divisible, 4) + bitvector_repeat = solver.mkOp(kinds.BVRepeat, 5) + bitvector_zero_extend = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_sign_extend = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_rotate_left = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_right = solver.mkOp(kinds.BVRotateRight, 9) + int_to_bitvector = solver.mkOp(kinds.IntToBV, 10) + iand = solver.mkOp(kinds.Iand, 3) + floatingpoint_to_ubv = solver.mkOp(kinds.FPToUbv, 11) + floatingopint_to_sbv = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_fp_ieee_bitvector = solver.mkOp(kinds.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_floatingpoint = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_real = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_signed_bitvector = solver.mkOp(kinds.FPToFpSignedBV, 4, + 25) + floatingpoint_to_fp_unsigned_bitvector = solver.mkOp( + kinds.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_generic = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + regexp_loop = solver.mkOp(kinds.RegexpLoop, 2, 3) + + assert 0 == plus.getNumIndices() + assert 1 == divisible.getNumIndices() + assert 1 == bitvector_repeat.getNumIndices() + assert 1 == bitvector_zero_extend.getNumIndices() + assert 1 == bitvector_sign_extend.getNumIndices() + assert 1 == bitvector_rotate_left.getNumIndices() + assert 1 == bitvector_rotate_right.getNumIndices() + assert 1 == int_to_bitvector.getNumIndices() + assert 1 == iand.getNumIndices() + assert 1 == floatingpoint_to_ubv.getNumIndices() + assert 1 == floatingopint_to_sbv.getNumIndices() + assert 2 == floatingpoint_to_fp_ieee_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_floatingpoint.getNumIndices() + assert 2 == floatingpoint_to_fp_real.getNumIndices() + assert 2 == floatingpoint_to_fp_signed_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_unsigned_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_generic.getNumIndices() + assert 2 == regexp_loop.getNumIndices() + +def test_op_indices_list(solver): + with_list = solver.mkOp(kinds.TupleProject, [4, 25]) + assert 2 == with_list.getNumIndices() + +def test_get_indices_string(solver): + x = Op(solver) + with pytest.raises(RuntimeError): + x.getIndices() + + divisible_ot = solver.mkOp(kinds.Divisible, 4) + assert divisible_ot.isIndexed() + divisible_idx = divisible_ot.getIndices() + assert divisible_idx == "4" + + +def test_get_indices_uint(solver): + bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + assert bitvector_repeat_ot.isIndexed() + bitvector_repeat_idx = bitvector_repeat_ot.getIndices() + assert bitvector_repeat_idx == 5 + + bitvector_zero_extend_ot = solver.mkOp(kinds.BVZeroExtend, 6) + bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices() + assert bitvector_zero_extend_idx == 6 + + bitvector_sign_extend_ot = solver.mkOp(kinds.BVSignExtend, 7) + bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices() + assert bitvector_sign_extend_idx == 7 + + bitvector_rotate_left_ot = solver.mkOp(kinds.BVRotateLeft, 8) + bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices() + assert bitvector_rotate_left_idx == 8 + + bitvector_rotate_right_ot = solver.mkOp(kinds.BVRotateRight, 9) + bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices() + assert bitvector_rotate_right_idx == 9 + + int_to_bitvector_ot = solver.mkOp(kinds.IntToBV, 10) + int_to_bitvector_idx = int_to_bitvector_ot.getIndices() + assert int_to_bitvector_idx == 10 + + floatingpoint_to_ubv_ot = solver.mkOp(kinds.FPToUbv, 11) + floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices() + assert floatingpoint_to_ubv_idx == 11 + + floatingpoint_to_sbv_ot = solver.mkOp(kinds.FPToSbv, 13) + floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices() + assert floatingpoint_to_sbv_idx == 13 + + +def test_get_indices_pair_uint(solver): + bitvector_extract_ot = solver.mkOp(kinds.BVExtract, 4, 0) + assert bitvector_extract_ot.isIndexed() + bitvector_extract_indices = bitvector_extract_ot.getIndices() + assert bitvector_extract_indices == (4, 0) + + floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp( + kinds.FPToFpIeeeBV, 4, 25) + floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25) + + floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(kinds.FPToFpFP, 4, 25) + floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices( + ) + assert floatingpoint_to_fp_floatingpoint_indices == (4, 25) + + floatingpoint_to_fp_real_ot = solver.mkOp(kinds.FPToFpReal, 4, 25) + floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices() + assert floatingpoint_to_fp_real_indices == (4, 25) + + floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp( + kinds.FPToFpSignedBV, 4, 25) + floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25) + + floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp( + kinds.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices( + ) + assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25) + + floatingpoint_to_fp_generic_ot = solver.mkOp(kinds.FPToFpGeneric, 4, 25) + floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices( + ) + assert floatingpoint_to_fp_generic_indices == (4, 25) + + +def test_op_scoping_to_string(solver): + bitvector_repeat_ot = solver.mkOp(kinds.BVRepeat, 5) + op_repr = str(bitvector_repeat_ot) + assert str(bitvector_repeat_ot) == op_repr diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py new file mode 100644 index 000000000..bd97646f9 --- /dev/null +++ b/test/unit/api/python/test_result.py @@ -0,0 +1,115 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar +# +# 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. +# ############################################################################# +# +# Unit tests for result API. +# +# Obtained by translating test/unit/api/result_black.cpp +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Result +from pycvc5 import UnknownExplanation + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_is_null(solver): + res_null = Result(solver) + assert res_null.isNull() + assert not res_null.isSat() + assert not res_null.isUnsat() + assert not res_null.isSatUnknown() + assert not res_null.isEntailed() + assert not res_null.isNotEntailed() + assert not res_null.isEntailmentUnknown() + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res = solver.checkSat() + assert not res.isNull() + + +def test_eq(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res2 = solver.checkSat() + res3 = solver.checkSat() + res = res2 + assert res == res2 + assert res3 == res2 + + +def test_is_sat(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x)) + res = solver.checkSat() + assert res.isSat() + assert not res.isSatUnknown() + + +def test_is_unsat(solver): + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkVar(u_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkSat() + assert res.isUnsat() + assert not res.isSatUnknown() + + +def test_is_sat_unknown(solver): + solver.setLogic("QF_NIA") + solver.setOption("incremental", "false") + solver.setOption("solve-int-as-bv", "32") + int_sort = solver.getIntegerSort() + x = solver.mkVar(int_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkSat() + assert not res.isSat() + assert res.isSatUnknown() + + +def test_is_entailed(solver): + solver.setOption("incremental", "true") + u_sort = solver.mkUninterpretedSort("u") + x = solver.mkConst(u_sort, "x") + y = solver.mkConst(u_sort, "y") + a = x.eqTerm(y).notTerm() + b = x.eqTerm(y) + solver.assertFormula(a) + entailed = solver.checkEntailed(a) + assert entailed.isEntailed() + assert not entailed.isEntailmentUnknown() + not_entailed = solver.checkEntailed(b) + assert not_entailed.isNotEntailed() + assert not not_entailed.isEntailmentUnknown() + + +def test_is_entailment_unknown(solver): + solver.setLogic("QF_NIA") + solver.setOption("incremental", "false") + solver.setOption("solve-int-as-bv", "32") + int_sort = solver.getIntegerSort() + x = solver.mkVar(int_sort, "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + res = solver.checkEntailed(x.eqTerm(x)) + assert not res.isEntailed() + assert res.isEntailmentUnknown() + print(type(pycvc5.RoundTowardZero)) + print(type(pycvc5.UnknownReason)) + assert res.getUnknownExplanation() == pycvc5.UnknownReason diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py new file mode 100644 index 000000000..89e99bd9e --- /dev/null +++ b/test/unit/api/python/test_solver.py @@ -0,0 +1,1890 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Ying Sheng +# +# 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. +# ############################################################################# +## + +import pytest +import pycvc5 +import sys + +from pycvc5 import kinds + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_recoverable_exception(solver): + solver.setOption("produce-models", "true") + x = solver.mkConst(solver.getBooleanSort(), "x") + solver.assertFormula(x.eqTerm(x).notTerm()) + with pytest.raises(RuntimeError): + c = solver.getValue(x) + + +def test_supports_floating_point(solver): + solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + + +def test_get_boolean_sort(solver): + solver.getBooleanSort() + + +def test_get_integer_sort(solver): + solver.getIntegerSort() + + +def test_get_null_sort(solver): + solver.getNullSort() + + +def test_get_real_sort(solver): + solver.getRealSort() + + +def test_get_reg_exp_sort(solver): + solver.getRegExpSort() + + +def test_get_string_sort(solver): + solver.getStringSort() + + +def test_get_rounding_mode_sort(solver): + solver.getRoundingModeSort() + + +def test_mk_array_sort(solver): + boolSort = solver.getBooleanSort() + intSort = solver.getIntegerSort() + realSort = solver.getRealSort() + bvSort = solver.mkBitVectorSort(32) + solver.mkArraySort(boolSort, boolSort) + solver.mkArraySort(intSort, intSort) + solver.mkArraySort(realSort, realSort) + solver.mkArraySort(bvSort, bvSort) + solver.mkArraySort(boolSort, intSort) + solver.mkArraySort(realSort, bvSort) + + fpSort = solver.mkFloatingPointSort(3, 5) + solver.mkArraySort(fpSort, fpSort) + solver.mkArraySort(bvSort, fpSort) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkArraySort(boolSort, boolSort) + + +def test_mk_bit_vector_sort(solver): + solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + solver.mkBitVectorSort(0) + + +def test_mk_floating_point_sort(solver): + solver.mkFloatingPointSort(4, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(0, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(4, 0) + + +def test_mk_datatype_sort(solver): + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + solver.mkDatatypeSort(dtypeSpec) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkDatatypeSort(dtypeSpec) + + throwsDtypeSpec = solver.mkDatatypeDecl("list") + with pytest.raises(RuntimeError): + solver.mkDatatypeSort(throwsDtypeSpec) + + +def test_mk_datatype_sorts(solver): + slv = pycvc5.Solver() + + dtypeSpec1 = solver.mkDatatypeDecl("list1") + cons1 = solver.mkDatatypeConstructorDecl("cons1") + cons1.addSelector("head1", solver.getIntegerSort()) + dtypeSpec1.addConstructor(cons1) + nil1 = solver.mkDatatypeConstructorDecl("nil1") + dtypeSpec1.addConstructor(nil1) + + dtypeSpec2 = solver.mkDatatypeDecl("list2") + cons2 = solver.mkDatatypeConstructorDecl("cons2") + cons2.addSelector("head2", solver.getIntegerSort()) + dtypeSpec2.addConstructor(cons2) + nil2 = solver.mkDatatypeConstructorDecl("nil2") + dtypeSpec2.addConstructor(nil2) + + decls = [dtypeSpec1, dtypeSpec2] + solver.mkDatatypeSorts(decls, set([])) + + with pytest.raises(RuntimeError): + slv.mkDatatypeSorts(decls, set([])) + + throwsDtypeSpec = solver.mkDatatypeDecl("list") + throwsDecls = [throwsDtypeSpec] + with pytest.raises(RuntimeError): + solver.mkDatatypeSorts(throwsDecls, set([])) + + # with unresolved sorts + unresList = solver.mkUninterpretedSort("ulist") + unresSorts = set([unresList]) + ulist = solver.mkDatatypeDecl("ulist") + ucons = solver.mkDatatypeConstructorDecl("ucons") + ucons.addSelector("car", unresList) + ucons.addSelector("cdr", unresList) + ulist.addConstructor(ucons) + unil = solver.mkDatatypeConstructorDecl("unil") + ulist.addConstructor(unil) + udecls = [ulist] + + solver.mkDatatypeSorts(udecls, unresSorts) + with pytest.raises(RuntimeError): + slv.mkDatatypeSorts(udecls, unresSorts) + + +def test_mk_function_sort(solver): + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + + # function arguments are allowed + solver.mkFunctionSort(funSort, solver.getIntegerSort()) + + # non-first-class arguments are not allowed + reSort = solver.getRegExpSort() + with pytest.raises(RuntimeError): + solver.mkFunctionSort(reSort, solver.getIntegerSort()) + with pytest.raises(RuntimeError): + solver.mkFunctionSort(solver.getIntegerSort(), funSort) + + solver.mkFunctionSort([solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()],\ + solver.getIntegerSort()) + funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + + # function arguments are allowed + solver.mkFunctionSort([funSort2, solver.mkUninterpretedSort("u")],\ + solver.getIntegerSort()) + + with pytest.raises(RuntimeError): + solver.mkFunctionSort([solver.getIntegerSort(),\ + solver.mkUninterpretedSort("u")],\ + funSort2) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkFunctionSort(solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + with pytest.raises(RuntimeError): + slv.mkFunctionSort(slv.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + sorts1 = [solver.getBooleanSort(),\ + slv.getIntegerSort(),\ + solver.getIntegerSort()] + sorts2 = [slv.getBooleanSort(), slv.getIntegerSort()] + slv.mkFunctionSort(sorts2, slv.getIntegerSort()) + with pytest.raises(RuntimeError): + slv.mkFunctionSort(sorts1, slv.getIntegerSort()) + with pytest.raises(RuntimeError): + slv.mkFunctionSort(sorts2, solver.getIntegerSort()) + + +def test_mk_param_sort(solver): + solver.mkParamSort("T") + solver.mkParamSort("") + + +def test_mk_predicate_sort(solver): + solver.mkPredicateSort([solver.getIntegerSort()]) + with pytest.raises(RuntimeError): + solver.mkPredicateSort([]) + + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + # functions as arguments are allowed + solver.mkPredicateSort([solver.getIntegerSort(), funSort]) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkPredicateSort([solver.getIntegerSort()]) + + +def test_mk_record_sort(solver): + fields = [("b", solver.getBooleanSort()),\ + ("bv", solver.mkBitVectorSort(8)),\ + ("i", solver.getIntegerSort())] + empty = [] + solver.mkRecordSort(fields) + solver.mkRecordSort(empty) + recSort = solver.mkRecordSort(fields) + recSort.getDatatype() + + +def test_mk_set_sort(solver): + solver.mkSetSort(solver.getBooleanSort()) + solver.mkSetSort(solver.getIntegerSort()) + solver.mkSetSort(solver.mkBitVectorSort(4)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkSetSort(solver.mkBitVectorSort(4)) + + +def test_mk_bag_sort(solver): + solver.mkBagSort(solver.getBooleanSort()) + solver.mkBagSort(solver.getIntegerSort()) + solver.mkBagSort(solver.mkBitVectorSort(4)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkBagSort(solver.mkBitVectorSort(4)) + + +def test_mk_sequence_sort(solver): + solver.mkSequenceSort(solver.getBooleanSort()) + solver.mkSequenceSort(\ + solver.mkSequenceSort(solver.getIntegerSort())) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkSequenceSort(solver.getIntegerSort()) + + +def test_mk_uninterpreted_sort(solver): + solver.mkUninterpretedSort("u") + solver.mkUninterpretedSort("") + + +def test_mk_sortConstructor_sort(solver): + solver.mkSortConstructorSort("s", 2) + solver.mkSortConstructorSort("", 2) + with pytest.raises(RuntimeError): + solver.mkSortConstructorSort("", 0) + + +def test_mk_tuple_sort(solver): + solver.mkTupleSort([solver.getIntegerSort()]) + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + with pytest.raises(RuntimeError): + solver.mkTupleSort([solver.getIntegerSort(), funSort]) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkTupleSort([solver.getIntegerSort()]) + + +def test_mk_bit_vector(solver): + solver.mkBitVector(8, 2) + solver.mkBitVector(32, 2) + + solver.mkBitVector(4, "1010", 2) + solver.mkBitVector(8, "0101", 2) + solver.mkBitVector(8, "-1111111", 2) + solver.mkBitVector(8, "00000101", 2) + solver.mkBitVector(8, "-127", 10) + solver.mkBitVector(8, "255", 10) + solver.mkBitVector(10, "1010", 10) + solver.mkBitVector(11, "1234", 10) + solver.mkBitVector(8, "-7f", 16) + solver.mkBitVector(8, "a0", 16) + solver.mkBitVector(16, "1010", 16) + solver.mkBitVector(16, "a09f", 16) + + with pytest.raises(RuntimeError): + solver.mkBitVector(0, 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(0, "-127", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(0, "a0", 16) + + with pytest.raises(RuntimeError): + solver.mkBitVector(2, "", 2) + + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "101", 5) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "127", 11) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "a0", 21) + + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "101010101", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-11111111", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-256", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "257", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-a0", 16) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "fffff", 16) + + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "10201010", 2) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "-25x", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "2x7", 10) + with pytest.raises(RuntimeError): + solver.mkBitVector(8, "fzff", 16) + + assert solver.mkBitVector(8, "0101", 2) == solver.mkBitVector(8, "00000101", 2) + assert solver.mkBitVector(4, "1010", 2) == solver.mkBitVector(4, "10", 10) + assert solver.mkBitVector(4, "1010", 2) == solver.mkBitVector(4, "a", 16) + assert str(solver.mkBitVector(8, "01010101", 2)) == "#b01010101" + assert str(solver.mkBitVector(8, "F", 16)) == "#b00001111" + assert solver.mkBitVector(8, "-1", 10) ==\ + solver.mkBitVector(8, "FF", 16) + + +def test_mk_var(solver): + boolSort = solver.getBooleanSort() + intSort = solver.getIntegerSort() + funSort = solver.mkFunctionSort(intSort, boolSort) + solver.mkVar(boolSort) + solver.mkVar(funSort) + solver.mkVar(boolSort, "b") + solver.mkVar(funSort, "") + with pytest.raises(RuntimeError): + solver.mkVar(pycvc5.Sort(solver)) + with pytest.raises(RuntimeError): + solver.mkVar(pycvc5.Sort(solver), "a") + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkVar(boolSort, "x") + + +def test_mk_boolean(solver): + solver.mkBoolean(True) + solver.mkBoolean(False) + + +def test_mk_rounding_mode(solver): + solver.mkRoundingMode(pycvc5.RoundTowardZero) + + +def test_mk_abstract_value(solver): + solver.mkAbstractValue("1") + with pytest.raises(ValueError): + solver.mkAbstractValue("0") + with pytest.raises(ValueError): + solver.mkAbstractValue("-1") + with pytest.raises(ValueError): + solver.mkAbstractValue("1.2") + with pytest.raises(ValueError): + solver.mkAbstractValue("1/2") + with pytest.raises(ValueError): + solver.mkAbstractValue("asdf") + + solver.mkAbstractValue(1) + with pytest.raises(ValueError): + solver.mkAbstractValue(-1) + with pytest.raises(ValueError): + solver.mkAbstractValue(0) + + +def test_mk_floating_point(solver): + t1 = solver.mkBitVector(8) + t2 = solver.mkBitVector(4) + t3 = solver.mkInteger(2) + solver.mkFloatingPoint(3, 5, t1) + + with pytest.raises(RuntimeError): + solver.mkFloatingPoint(0, 5, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkFloatingPoint(0, 5, t1) + with pytest.raises(RuntimeError): + solver.mkFloatingPoint(3, 0, t1) + with pytest.raises(RuntimeError): + solver.mkFloatingPoint(3, 5, t2) + with pytest.raises(RuntimeError): + solver.mkFloatingPoint(3, 5, t2) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkFloatingPoint(3, 5, t1) + +def test_mk_cardinality_constraint(solver): + su = solver.mkUninterpretedSort("u") + si = solver.getIntegerSort() + solver.mkCardinalityConstraint(su, 3) + with pytest.raises(RuntimeError): + solver.mkEmptySet(solver.mkCardinalityConstraint(si, 3)) + with pytest.raises(RuntimeError): + solver.mkEmptySet(solver.mkCardinalityConstraint(su, 0)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkCardinalityConstraint(su, 3) + +def test_mk_empty_set(solver): + slv = pycvc5.Solver() + s = solver.mkSetSort(solver.getBooleanSort()) + solver.mkEmptySet(pycvc5.Sort(solver)) + solver.mkEmptySet(s) + with pytest.raises(RuntimeError): + solver.mkEmptySet(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.mkEmptySet(s) + + +def test_mk_empty_bag(solver): + slv = pycvc5.Solver() + s = solver.mkBagSort(solver.getBooleanSort()) + solver.mkEmptyBag(pycvc5.Sort(solver)) + solver.mkEmptyBag(s) + with pytest.raises(RuntimeError): + solver.mkEmptyBag(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.mkEmptyBag(s) + + +def test_mk_empty_sequence(solver): + slv = pycvc5.Solver() + s = solver.mkSequenceSort(solver.getBooleanSort()) + solver.mkEmptySequence(s) + solver.mkEmptySequence(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.mkEmptySequence(s) + + +def test_mk_false(solver): + solver.mkFalse() + solver.mkFalse() + + +def test_mk_nan(solver): + solver.mkNaN(3, 5) + + +def test_mk_neg_zero(solver): + solver.mkNegZero(3, 5) + + +def test_mk_neg_inf(solver): + solver.mkNegInf(3, 5) + + +def test_mk_pos_inf(solver): + solver.mkPosInf(3, 5) + + +def test_mk_pos_zero(solver): + solver.mkPosZero(3, 5) + + +def test_mk_op(solver): + # mkOp(Kind kind, Kind k) + with pytest.raises(ValueError): + solver.mkOp(kinds.BVExtract, kinds.Equal) + + # mkOp(Kind kind, const std::string& arg) + solver.mkOp(kinds.Divisible, "2147483648") + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, "asdf") + + # mkOp(Kind kind, uint32_t arg) + solver.mkOp(kinds.Divisible, 1) + solver.mkOp(kinds.BVRotateLeft, 1) + solver.mkOp(kinds.BVRotateRight, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.BVExtract, 1) + + # mkOp(Kind kind, uint32_t arg1, uint32_t arg2) + solver.mkOp(kinds.BVExtract, 1, 1) + with pytest.raises(RuntimeError): + solver.mkOp(kinds.Divisible, 1, 2) + + # mkOp(Kind kind, std::vector<uint32_t> args) + args = [1, 2, 2] + solver.mkOp(kinds.TupleProject, args) + + +def test_mk_pi(solver): + solver.mkPi() + + +def test_mk_integer(solver): + solver.mkInteger("123") + with pytest.raises(RuntimeError): + solver.mkInteger("1.23") + with pytest.raises(RuntimeError): + solver.mkInteger("1/23") + with pytest.raises(RuntimeError): + solver.mkInteger("12/3") + with pytest.raises(RuntimeError): + solver.mkInteger(".2") + with pytest.raises(RuntimeError): + solver.mkInteger("2.") + with pytest.raises(RuntimeError): + solver.mkInteger("") + with pytest.raises(RuntimeError): + solver.mkInteger("asdf") + with pytest.raises(RuntimeError): + solver.mkInteger("1.2/3") + with pytest.raises(RuntimeError): + solver.mkInteger(".") + with pytest.raises(RuntimeError): + solver.mkInteger("/") + with pytest.raises(RuntimeError): + solver.mkInteger("2/") + with pytest.raises(RuntimeError): + solver.mkInteger("/2") + + solver.mkReal("123") + with pytest.raises(RuntimeError): + solver.mkInteger("1.23") + with pytest.raises(RuntimeError): + solver.mkInteger("1/23") + with pytest.raises(RuntimeError): + solver.mkInteger("12/3") + with pytest.raises(RuntimeError): + solver.mkInteger(".2") + with pytest.raises(RuntimeError): + solver.mkInteger("2.") + with pytest.raises(RuntimeError): + solver.mkInteger("") + with pytest.raises(RuntimeError): + solver.mkInteger("asdf") + with pytest.raises(RuntimeError): + solver.mkInteger("1.2/3") + with pytest.raises(RuntimeError): + solver.mkInteger(".") + with pytest.raises(RuntimeError): + solver.mkInteger("/") + with pytest.raises(RuntimeError): + solver.mkInteger("2/") + with pytest.raises(RuntimeError): + solver.mkInteger("/2") + + val1 = 1 + val2 = -1 + val3 = 1 + val4 = -1 + solver.mkInteger(val1) + solver.mkInteger(val2) + solver.mkInteger(val3) + solver.mkInteger(val4) + solver.mkInteger(val4) + + +def test_mk_real(solver): + solver.mkReal("123") + solver.mkReal("1.23") + solver.mkReal("1/23") + solver.mkReal("12/3") + solver.mkReal(".2") + solver.mkReal("2.") + with pytest.raises(RuntimeError): + solver.mkReal("") + with pytest.raises(RuntimeError): + solver.mkReal("asdf") + with pytest.raises(RuntimeError): + solver.mkReal("1.2/3") + with pytest.raises(RuntimeError): + solver.mkReal(".") + with pytest.raises(RuntimeError): + solver.mkReal("/") + with pytest.raises(RuntimeError): + solver.mkReal("2/") + with pytest.raises(RuntimeError): + solver.mkReal("/2") + + solver.mkReal("123") + solver.mkReal("1.23") + solver.mkReal("1/23") + solver.mkReal("12/3") + solver.mkReal(".2") + solver.mkReal("2.") + with pytest.raises(RuntimeError): + solver.mkReal("") + with pytest.raises(RuntimeError): + solver.mkReal("asdf") + with pytest.raises(RuntimeError): + solver.mkReal("1.2/3") + with pytest.raises(RuntimeError): + solver.mkReal(".") + with pytest.raises(RuntimeError): + solver.mkReal("/") + with pytest.raises(RuntimeError): + solver.mkReal("2/") + with pytest.raises(RuntimeError): + solver.mkReal("/2") + + val1 = 1 + val2 = -1 + val3 = 1 + val4 = -1 + solver.mkReal(val1) + solver.mkReal(val2) + solver.mkReal(val3) + solver.mkReal(val4) + solver.mkReal(val4) + solver.mkReal(val1, val1) + solver.mkReal(val2, val2) + solver.mkReal(val3, val3) + solver.mkReal(val4, val4) + + +def test_mk_regexp_none(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpNone()) + + +def test_mk_regexp_all(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAll()) + + +def test_mk_regexp_allchar(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpAllchar()) + + +def test_mk_sep_emp(solver): + solver.mkSepEmp(); + + +def test_mk_sep_nil(solver): + solver.mkSepNil(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + solver.mkSepNil(pycvc5.Sort(solver)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkSepNil(solver.getIntegerSort()) + + +def test_mk_string(solver): + solver.mkString("") + solver.mkString("asdfasdf") + str(solver.mkString("asdf\\nasdf")) == "\"asdf\\u{5c}nasdf\"" + str(solver.mkString("asdf\\u{005c}nasdf", True)) ==\ + "\"asdf\\u{5c}nasdf\"" + + +def test_mk_term(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [a, b] + v2 = [a, pycvc5.Term(solver)] + v3 = [a, solver.mkTrue()] + v4 = [solver.mkInteger(1), solver.mkInteger(2)] + v5 = [solver.mkInteger(1), pycvc5.Term(solver)] + v6 = [] + slv = pycvc5.Solver() + + # mkTerm(Kind kind) const + solver.mkPi() + solver.mkTerm(kinds.RegexpNone) + solver.mkTerm(kinds.RegexpAllchar) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ConstBV) + + # mkTerm(Kind kind, Term child) const + solver.mkTerm(kinds.Not, solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Not, a) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Not, solver.mkTrue()) + + # mkTerm(Kind kind, Term child1, Term child2) const + solver.mkTerm(kinds.Equal, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, pycvc5.Term(solver), b) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, a, solver.mkTrue()) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Equal, a, b) + + # mkTerm(Kind kind, Term child1, Term child2, Term child3) const + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, pycvc5.Term(solver), solver.mkTrue(), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), pycvc5.Term(solver), + solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), b) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), + solver.mkTrue()) + + # mkTerm(Kind kind, const std::vector<Term>& children) const + solver.mkTerm(kinds.Equal, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Equal, v3) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.Distinct, v6) + + +def test_mk_term_from_op(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + b = solver.mkConst(bv32, "b") + v1 = [solver.mkInteger(1), solver.mkInteger(2)] + v2 = [solver.mkInteger(1), pycvc5.Term(solver)] + v3 = [] + v4 = [solver.mkInteger(5)] + slv = pycvc5.Solver() + + # simple operator terms + opterm1 = solver.mkOp(kinds.BVExtract, 2, 1) + opterm2 = solver.mkOp(kinds.Divisible, 1) + + # list datatype + sort = solver.mkParamSort("T") + listDecl = solver.mkDatatypeDecl("paramlist", sort) + cons = solver.mkDatatypeConstructorDecl("cons") + nil = solver.mkDatatypeConstructorDecl("nil") + cons.addSelector("head", sort) + cons.addSelectorSelf("tail") + listDecl.addConstructor(cons) + listDecl.addConstructor(nil) + listSort = solver.mkDatatypeSort(listDecl) + intListSort =\ + listSort.instantiate([solver.getIntegerSort()]) + c = solver.mkConst(intListSort, "c") + lis = listSort.getDatatype() + + # list datatype constructor and selector operator terms + consTerm1 = lis.getConstructorTerm("cons") + consTerm2 = lis.getConstructor("cons").getConstructorTerm() + nilTerm1 = lis.getConstructorTerm("nil") + nilTerm2 = lis.getConstructor("nil").getConstructorTerm() + headTerm1 = lis["cons"].getSelectorTerm("head") + headTerm2 = lis["cons"].getSelector("head").getSelectorTerm() + tailTerm1 = lis["cons"].getSelectorTerm("tail") + tailTerm2 = lis["cons"]["tail"].getSelectorTerm() + + # mkTerm(Op op, Term term) const + solver.mkTerm(kinds.ApplyConstructor, nilTerm1) + solver.mkTerm(kinds.ApplyConstructor, nilTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, nilTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, consTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplySelector, headTerm1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor, nilTerm1) + + # mkTerm(Op op, Term child) const + solver.mkTerm(opterm1, a) + solver.mkTerm(opterm2, solver.mkInteger(1)) + solver.mkTerm(kinds.ApplySelector, headTerm1, c) + solver.mkTerm(kinds.ApplySelector, tailTerm2, c) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0)) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm1, a) + + # mkTerm(Op op, Term child1, Term child2) const + solver.mkTerm(kinds.ApplyConstructor, consTerm1, solver.mkInteger(0), + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(2)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, pycvc5.Term(solver), solver.mkInteger(1)) + with pytest.raises(RuntimeError): + slv.mkTerm(kinds.ApplyConstructor,\ + consTerm1,\ + solver.mkInteger(0),\ + solver.mkTerm(kinds.ApplyConstructor, nilTerm1)) + + # mkTerm(Op op, Term child1, Term child2, Term child3) const + with pytest.raises(RuntimeError): + solver.mkTerm(opterm1, a, b, a) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1), + pycvc5.Term(solver)) + + # mkTerm(Op op, const std::vector<Term>& children) const + solver.mkTerm(opterm2, v4) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v1) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v2) + with pytest.raises(RuntimeError): + solver.mkTerm(opterm2, v3) + with pytest.raises(RuntimeError): + slv.mkTerm(opterm2, v4) + + +def test_mk_true(solver): + solver.mkTrue() + solver.mkTrue() + + +def test_mk_tuple(solver): + solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector(3, "101", 2)]) + solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) + + with pytest.raises(RuntimeError): + solver.mkTuple([], [solver.mkBitVector(3, "101", 2)]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.mkBitVectorSort(4)], + [solver.mkBitVector(3, "101", 2)]) + with pytest.raises(RuntimeError): + solver.mkTuple([solver.getIntegerSort()], [solver.mkReal("5.3")]) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkTuple([solver.mkBitVectorSort(3)], [slv.mkBitVector(3, "101", 2)]) + with pytest.raises(RuntimeError): + slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector(3, "101", 2)]) + + +def test_mk_universe_set(solver): + solver.mkUniverseSet(solver.getBooleanSort()) + with pytest.raises(RuntimeError): + solver.mkUniverseSet(pycvc5.Sort(solver)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkUniverseSet(solver.getBooleanSort()) + + +def test_mk_const(solver): + boolSort = solver.getBooleanSort() + intSort = solver.getIntegerSort() + funSort = solver.mkFunctionSort(intSort, boolSort) + solver.mkConst(boolSort) + solver.mkConst(funSort) + solver.mkConst(boolSort, "b") + solver.mkConst(intSort, "i") + solver.mkConst(funSort, "f") + solver.mkConst(funSort, "") + with pytest.raises(RuntimeError): + solver.mkConst(pycvc5.Sort(solver)) + with pytest.raises(RuntimeError): + solver.mkConst(pycvc5.Sort(solver), "a") + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkConst(boolSort) + + +def test_mk_const_array(solver): + intSort = solver.getIntegerSort() + arrSort = solver.mkArraySort(intSort, intSort) + zero = solver.mkInteger(0) + constArr = solver.mkConstArray(arrSort, zero) + + solver.mkConstArray(arrSort, zero) + with pytest.raises(RuntimeError): + solver.mkConstArray(pycvc5.Sort(solver), zero) + with pytest.raises(RuntimeError): + solver.mkConstArray(arrSort, pycvc5.Term(solver)) + with pytest.raises(RuntimeError): + solver.mkConstArray(arrSort, solver.mkBitVector(1, 1)) + with pytest.raises(RuntimeError): + solver.mkConstArray(intSort, zero) + slv = pycvc5.Solver() + zero2 = slv.mkInteger(0) + arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort()) + with pytest.raises(RuntimeError): + slv.mkConstArray(arrSort2, zero) + with pytest.raises(RuntimeError): + slv.mkConstArray(arrSort, zero2) + + +def test_declare_fun(solver): + bvSort = solver.mkBitVectorSort(32) + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + solver.declareFun("f1", [], bvSort) + solver.declareFun("f3", [bvSort, solver.getIntegerSort()], bvSort) + with pytest.raises(RuntimeError): + solver.declareFun("f2", [], funSort) + # functions as arguments is allowed + solver.declareFun("f4", [bvSort, funSort], bvSort) + with pytest.raises(RuntimeError): + solver.declareFun("f5", [bvSort, bvSort], funSort) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.declareFun("f1", [], bvSort) + + +def test_declare_sort(solver): + solver.declareSort("s", 0) + solver.declareSort("s", 2) + solver.declareSort("", 2) + + +def test_define_fun(solver): + bvSort = solver.mkBitVectorSort(32) + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + b1 = solver.mkVar(bvSort, "b1") + b2 = solver.mkVar(solver.getIntegerSort(), "b2") + b3 = solver.mkVar(funSort, "b3") + v1 = solver.mkConst(bvSort, "v1") + v2 = solver.mkConst(funSort, "v2") + solver.defineFun("f", [], bvSort, v1) + solver.defineFun("ff", [b1, b2], bvSort, v1) + with pytest.raises(RuntimeError): + solver.defineFun("ff", [v1, b2], bvSort, v1) + with pytest.raises(RuntimeError): + solver.defineFun("fff", [b1], bvSort, v2) + with pytest.raises(RuntimeError): + solver.defineFun("ffff", [b1], funSort, v2) + # b3 has function sort, which is allowed as an argument + solver.defineFun("fffff", [b1, b3], bvSort, v1) + + slv = pycvc5.Solver() + bvSort2 = slv.mkBitVectorSort(32) + v12 = slv.mkConst(bvSort2, "v1") + b12 = slv.mkVar(bvSort2, "b1") + b22 = slv.mkVar(slv.getIntegerSort(), "b2") + with pytest.raises(RuntimeError): + slv.defineFun("f", [], bvSort, v12) + with pytest.raises(RuntimeError): + slv.defineFun("f", [], bvSort2, v1) + with pytest.raises(RuntimeError): + slv.defineFun("ff", [b1, b22], bvSort2, v12) + with pytest.raises(RuntimeError): + slv.defineFun("ff", [b12, b2], bvSort2, v12) + with pytest.raises(RuntimeError): + slv.defineFun("ff", [b12, b22], bvSort, v12) + with pytest.raises(RuntimeError): + slv.defineFun("ff", [b12, b22], bvSort2, v1) + + +def test_define_fun_rec(solver): + bvSort = solver.mkBitVectorSort(32) + funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort) + funSort2 = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),\ + solver.getIntegerSort()) + b1 = solver.mkVar(bvSort, "b1") + b11 = solver.mkVar(bvSort, "b1") + b2 = solver.mkVar(solver.getIntegerSort(), "b2") + b3 = solver.mkVar(funSort2, "b3") + v1 = solver.mkConst(bvSort, "v1") + v2 = solver.mkConst(solver.getIntegerSort(), "v2") + v3 = solver.mkConst(funSort2, "v3") + f1 = solver.mkConst(funSort1, "f1") + f2 = solver.mkConst(funSort2, "f2") + f3 = solver.mkConst(bvSort, "f3") + solver.defineFunRec("f", [], bvSort, v1) + solver.defineFunRec("ff", [b1, b2], bvSort, v1) + solver.defineFunRec(f1, [b1, b11], v1) + with pytest.raises(RuntimeError): + solver.defineFunRec("fff", [b1], bvSort, v3) + with pytest.raises(RuntimeError): + solver.defineFunRec("ff", [b1, v2], bvSort, v1) + with pytest.raises(RuntimeError): + solver.defineFunRec("ffff", [b1], funSort2, v3) + # b3 has function sort, which is allowed as an argument + solver.defineFunRec("fffff", [b1, b3], bvSort, v1) + with pytest.raises(RuntimeError): + solver.defineFunRec(f1, [b1], v1) + with pytest.raises(RuntimeError): + solver.defineFunRec(f1, [b1, b11], v2) + with pytest.raises(RuntimeError): + solver.defineFunRec(f1, [b1, b11], v3) + with pytest.raises(RuntimeError): + solver.defineFunRec(f2, [b1], v2) + with pytest.raises(RuntimeError): + solver.defineFunRec(f3, [b1], v1) + + slv = pycvc5.Solver() + bvSort2 = slv.mkBitVectorSort(32) + v12 = slv.mkConst(bvSort2, "v1") + b12 = slv.mkVar(bvSort2, "b1") + b22 = slv.mkVar(slv.getIntegerSort(), "b2") + slv.defineFunRec("f", [], bvSort2, v12) + slv.defineFunRec("ff", [b12, b22], bvSort2, v12) + with pytest.raises(RuntimeError): + slv.defineFunRec("f", [], bvSort, v12) + with pytest.raises(RuntimeError): + slv.defineFunRec("f", [], bvSort2, v1) + with pytest.raises(RuntimeError): + slv.defineFunRec("ff", [b1, b22], bvSort2, v12) + with pytest.raises(RuntimeError): + slv.defineFunRec("ff", [b12, b2], bvSort2, v12) + with pytest.raises(RuntimeError): + slv.defineFunRec("ff", [b12, b22], bvSort, v12) + with pytest.raises(RuntimeError): + slv.defineFunRec("ff", [b12, b22], bvSort2, v1) + + +def test_define_fun_rec_wrong_logic(solver): + solver.setLogic("QF_BV") + bvSort = solver.mkBitVectorSort(32) + funSort = solver.mkFunctionSort([bvSort, bvSort], bvSort) + b = solver.mkVar(bvSort, "b") + v = solver.mkConst(bvSort, "v") + f = solver.mkConst(funSort, "f") + with pytest.raises(RuntimeError): + solver.defineFunRec("f", [], bvSort, v) + with pytest.raises(RuntimeError): + solver.defineFunRec(f, [b, b], v) + + +def test_uf_iteration(solver): + intSort = solver.getIntegerSort() + funSort = solver.mkFunctionSort([intSort, intSort], intSort) + x = solver.mkConst(intSort, "x") + y = solver.mkConst(intSort, "y") + f = solver.mkConst(funSort, "f") + fxy = solver.mkTerm(kinds.ApplyUf, f, x, y) + + # Expecting the uninterpreted function to be one of the children + expected_children = [f, x, y] + idx = 0 + for c in fxy: + assert idx < 3 + assert c == expected_children[idx] + idx = idx + 1 + + +def test_get_info(solver): + solver.getInfo("name") + with pytest.raises(RuntimeError): + solver.getInfo("asdf") + + +def test_get_op(solver): + bv32 = solver.mkBitVectorSort(32) + a = solver.mkConst(bv32, "a") + ext = solver.mkOp(kinds.BVExtract, 2, 1) + exta = solver.mkTerm(ext, a) + + assert not a.hasOp() + with pytest.raises(RuntimeError): + a.getOp() + assert exta.hasOp() + assert exta.getOp() == ext + + # Test Datatypes -- more complicated + consListSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + cons.addSelectorSelf("tail") + consListSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + consListSpec.addConstructor(nil) + consListSort = solver.mkDatatypeSort(consListSpec) + consList = consListSort.getDatatype() + + consTerm = consList.getConstructorTerm("cons") + nilTerm = consList.getConstructorTerm("nil") + headTerm = consList["cons"].getSelectorTerm("head") + + listnil = solver.mkTerm(kinds.ApplyConstructor, nilTerm) + listcons1 = solver.mkTerm(kinds.ApplyConstructor, consTerm, + solver.mkInteger(1), listnil) + listhead = solver.mkTerm(kinds.ApplySelector, headTerm, listcons1) + + assert listnil.hasOp() + assert listcons1.hasOp() + assert listhead.hasOp() + + +def test_get_option(solver): + solver.getOption("incremental") + with pytest.raises(RuntimeError): + solver.getOption("asdf") + + +def test_get_unsat_assumptions1(solver): + solver.setOption("incremental", "false") + solver.checkSatAssuming(solver.mkFalse()) + with pytest.raises(RuntimeError): + solver.getUnsatAssumptions() + + +def test_get_unsat_assumptions2(solver): + solver.setOption("incremental", "true") + solver.setOption("produce-unsat-assumptions", "false") + solver.checkSatAssuming(solver.mkFalse()) + with pytest.raises(RuntimeError): + solver.getUnsatAssumptions() + + +def test_get_unsat_assumptions3(solver): + solver.setOption("incremental", "true") + solver.setOption("produce-unsat-assumptions", "true") + solver.checkSatAssuming(solver.mkFalse()) + solver.getUnsatAssumptions() + solver.checkSatAssuming(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.getUnsatAssumptions() + + +def test_get_unsat_core1(solver): + solver.setOption("incremental", "false") + solver.assertFormula(solver.mkFalse()) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getUnsatCore() + + +def test_get_unsat_core2(solver): + solver.setOption("incremental", "false") + solver.setOption("produce-unsat-cores", "false") + solver.assertFormula(solver.mkFalse()) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getUnsatCore() + + +def test_get_unsat_core3(solver): + solver.setOption("incremental", "true") + solver.setOption("produce-unsat-cores", "true") + + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + uToIntSort = solver.mkFunctionSort(uSort, intSort) + intPredSort = solver.mkFunctionSort(intSort, boolSort) + + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + f = solver.mkConst(uToIntSort, "f") + p = solver.mkConst(intPredSort, "p") + zero = solver.mkInteger(0) + one = solver.mkInteger(1) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + summ = solver.mkTerm(kinds.Plus, f_x, f_y) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + solver.assertFormula(solver.mkTerm(kinds.Gt, zero, f_x)) + solver.assertFormula(solver.mkTerm(kinds.Gt, zero, f_y)) + solver.assertFormula(solver.mkTerm(kinds.Gt, summ, one)) + solver.assertFormula(p_0) + solver.assertFormula(p_f_y.notTerm()) + assert solver.checkSat().isUnsat() + + unsat_core = solver.getUnsatCore() + + solver.resetAssertions() + for t in unsat_core: + solver.assertFormula(t) + res = solver.checkSat() + assert res.isUnsat() + + +def test_get_value1(solver): + solver.setOption("produce-models", "false") + t = solver.mkTrue() + solver.assertFormula(t) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getValue(t) + + +def test_get_value2(solver): + solver.setOption("produce-models", "true") + t = solver.mkFalse() + solver.assertFormula(t) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getValue(t) + + +def test_get_value3(solver): + solver.setOption("produce-models", "true") + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + uToIntSort = solver.mkFunctionSort(uSort, intSort) + intPredSort = solver.mkFunctionSort(intSort, boolSort) + + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + z = solver.mkConst(uSort, "z") + f = solver.mkConst(uToIntSort, "f") + p = solver.mkConst(intPredSort, "p") + zero = solver.mkInteger(0) + one = solver.mkInteger(1) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + summ = solver.mkTerm(kinds.Plus, f_x, f_y) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + + solver.assertFormula(solver.mkTerm(kinds.Leq, zero, f_x)) + solver.assertFormula(solver.mkTerm(kinds.Leq, zero, f_y)) + solver.assertFormula(solver.mkTerm(kinds.Leq, summ, one)) + solver.assertFormula(p_0.notTerm()) + solver.assertFormula(p_f_y) + assert solver.checkSat().isSat() + solver.getValue(x) + solver.getValue(y) + solver.getValue(z) + solver.getValue(summ) + solver.getValue(p_f_y) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.getValue(x) + + +def test_declare_separation_heap(solver): + solver.setLogic("ALL") + integer = solver.getIntegerSort() + solver.declareSepHeap(integer, integer) + # cannot declare separation logic heap more than once + with pytest.raises(RuntimeError): + solver.declareSepHeap(integer, integer) + + +# Helper function for test_get_separation_{heap,nil}_termX. Asserts and checks +# some simple separation logic constraints. +def checkSimpleSeparationConstraints(slv): + integer = slv.getIntegerSort() + # declare the separation heap + slv.declareSepHeap(integer, integer) + x = slv.mkConst(integer, "x") + p = slv.mkConst(integer, "p") + heap = slv.mkTerm(kinds.SepPto, p, x) + slv.assertFormula(heap) + nil = slv.mkSepNil(integer) + slv.assertFormula(nil.eqTerm(slv.mkReal(5))) + slv.checkSat() + + +def test_get_separation_heap_term1(solver): + solver.setLogic("QF_BV") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + t = solver.mkTrue() + solver.assertFormula(t) + with pytest.raises(RuntimeError): + solver.getValueSepHeap() + + +def test_get_separation_heap_term2(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "false") + checkSimpleSeparationConstraints(solver) + with pytest.raises(RuntimeError): + solver.getValueSepHeap() + + +def test_get_separation_heap_term3(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + t = solver.mkFalse() + solver.assertFormula(t) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getValueSepHeap() + + +def test_get_separation_heap_term4(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + t = solver.mkTrue() + solver.assertFormula(t) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getValueSepHeap() + + +def test_get_separation_heap_term5(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + checkSimpleSeparationConstraints(solver) + solver.getValueSepHeap() + + +def test_get_separation_nil_term1(solver): + solver.setLogic("QF_BV") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + t = solver.mkTrue() + solver.assertFormula(t) + with pytest.raises(RuntimeError): + solver.getValueSepNil() + + +def test_get_separation_nil_term2(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "false") + checkSimpleSeparationConstraints(solver) + with pytest.raises(RuntimeError): + solver.getValueSepNil() + + +def test_get_separation_nil_term3(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + t = solver.mkFalse() + solver.assertFormula(t) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getValueSepNil() + + +def test_get_separation_nil_term4(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + t = solver.mkTrue() + solver.assertFormula(t) + solver.checkSat() + with pytest.raises(RuntimeError): + solver.getValueSepNil() + + +def test_get_separation_nil_term5(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + checkSimpleSeparationConstraints(solver) + solver.getValueSepNil() + + +def test_push1(solver): + solver.setOption("incremental", "true") + solver.push(1) + with pytest.raises(RuntimeError): + solver.setOption("incremental", "false") + with pytest.raises(RuntimeError): + solver.setOption("incremental", "true") + + +def test_push2(solver): + solver.setOption("incremental", "false") + with pytest.raises(RuntimeError): + solver.push(1) + + +def test_pop1(solver): + solver.setOption("incremental", "false") + with pytest.raises(RuntimeError): + solver.pop(1) + + +def test_pop2(solver): + solver.setOption("incremental", "true") + with pytest.raises(RuntimeError): + solver.pop(1) + + +def test_pop3(solver): + solver.setOption("incremental", "true") + solver.push(1) + solver.pop(1) + with pytest.raises(RuntimeError): + solver.pop(1) + + +def test_setInfo(solver): + with pytest.raises(RuntimeError): + solver.setInfo("cvc5-lagic", "QF_BV") + with pytest.raises(RuntimeError): + solver.setInfo("cvc2-logic", "QF_BV") + with pytest.raises(RuntimeError): + solver.setInfo("cvc5-logic", "asdf") + + solver.setInfo("source", "asdf") + solver.setInfo("category", "asdf") + solver.setInfo("difficulty", "asdf") + solver.setInfo("filename", "asdf") + solver.setInfo("license", "asdf") + solver.setInfo("name", "asdf") + solver.setInfo("notes", "asdf") + + solver.setInfo("smt-lib-version", "2") + solver.setInfo("smt-lib-version", "2.0") + solver.setInfo("smt-lib-version", "2.5") + solver.setInfo("smt-lib-version", "2.6") + with pytest.raises(RuntimeError): + solver.setInfo("smt-lib-version", ".0") + + solver.setInfo("status", "sat") + solver.setInfo("status", "unsat") + solver.setInfo("status", "unknown") + with pytest.raises(RuntimeError): + solver.setInfo("status", "asdf") + + +def test_simplify(solver): + with pytest.raises(RuntimeError): + solver.simplify(pycvc5.Term(solver)) + + bvSort = solver.mkBitVectorSort(32) + uSort = solver.mkUninterpretedSort("u") + funSort1 = solver.mkFunctionSort([bvSort, bvSort], bvSort) + funSort2 = solver.mkFunctionSort(uSort, solver.getIntegerSort()) + consListSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + cons.addSelectorSelf("tail") + consListSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + consListSpec.addConstructor(nil) + consListSort = solver.mkDatatypeSort(consListSpec) + + x = solver.mkConst(bvSort, "x") + solver.simplify(x) + a = solver.mkConst(bvSort, "a") + solver.simplify(a) + b = solver.mkConst(bvSort, "b") + solver.simplify(b) + x_eq_x = solver.mkTerm(kinds.Equal, x, x) + solver.simplify(x_eq_x) + assert solver.mkTrue() != x_eq_x + assert solver.mkTrue() == solver.simplify(x_eq_x) + x_eq_b = solver.mkTerm(kinds.Equal, x, b) + solver.simplify(x_eq_b) + assert solver.mkTrue() != x_eq_b + assert solver.mkTrue() != solver.simplify(x_eq_b) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.simplify(x) + + i1 = solver.mkConst(solver.getIntegerSort(), "i1") + solver.simplify(i1) + i2 = solver.mkTerm(kinds.Mult, i1, solver.mkInteger("23")) + solver.simplify(i2) + assert i1 != i2 + assert i1 != solver.simplify(i2) + i3 = solver.mkTerm(kinds.Plus, i1, solver.mkInteger(0)) + solver.simplify(i3) + assert i1 != i3 + assert i1 == solver.simplify(i3) + + consList = consListSort.getDatatype() + dt1 = solver.mkTerm(\ + kinds.ApplyConstructor,\ + consList.getConstructorTerm("cons"),\ + solver.mkInteger(0),\ + solver.mkTerm(kinds.ApplyConstructor, consList.getConstructorTerm("nil"))) + solver.simplify(dt1) + dt2 = solver.mkTerm(\ + kinds.ApplySelector, consList["cons"].getSelectorTerm("head"), dt1) + solver.simplify(dt2) + + b1 = solver.mkVar(bvSort, "b1") + solver.simplify(b1) + b2 = solver.mkVar(bvSort, "b1") + solver.simplify(b2) + b3 = solver.mkVar(uSort, "b3") + solver.simplify(b3) + v1 = solver.mkConst(bvSort, "v1") + solver.simplify(v1) + v2 = solver.mkConst(solver.getIntegerSort(), "v2") + solver.simplify(v2) + f1 = solver.mkConst(funSort1, "f1") + solver.simplify(f1) + f2 = solver.mkConst(funSort2, "f2") + solver.simplify(f2) + solver.defineFunsRec([f1, f2], [[b1, b2], [b3]], [v1, v2]) + solver.simplify(f1) + solver.simplify(f2) + + +def test_assert_formula(solver): + solver.assertFormula(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.assertFormula(pycvc5.Term(solver)) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.assertFormula(solver.mkTrue()) + + +def test_check_entailed(solver): + solver.setOption("incremental", "false") + solver.checkEntailed(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.checkEntailed(solver.mkTrue()) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.checkEntailed(solver.mkTrue()) + + +def test_check_entailed1(solver): + boolSort = solver.getBooleanSort() + x = solver.mkConst(boolSort, "x") + y = solver.mkConst(boolSort, "y") + z = solver.mkTerm(kinds.And, x, y) + solver.setOption("incremental", "true") + solver.checkEntailed(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.checkEntailed(pycvc5.Term(solver)) + solver.checkEntailed(solver.mkTrue()) + solver.checkEntailed(z) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.checkEntailed(solver.mkTrue()) + + +def test_check_entailed2(solver): + solver.setOption("incremental", "true") + + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + uToIntSort = solver.mkFunctionSort(uSort, intSort) + intPredSort = solver.mkFunctionSort(intSort, boolSort) + + n = pycvc5.Term(solver) + # Constants + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + # Functions + f = solver.mkConst(uToIntSort, "f") + p = solver.mkConst(intPredSort, "p") + # Values + zero = solver.mkInteger(0) + one = solver.mkInteger(1) + # Terms + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + summ = solver.mkTerm(kinds.Plus, f_x, f_y) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + # Assertions + assertions =\ + solver.mkTerm(kinds.And,\ + [solver.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) + solver.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) + solver.mkTerm(kinds.Leq, summ, one), # f(x) + f(y) <= 1 + p_0.notTerm(), # not p(0) + p_f_y # p(f(y)) + ]) + + solver.checkEntailed(solver.mkTrue()) + solver.assertFormula(assertions) + solver.checkEntailed(solver.mkTerm(kinds.Distinct, x, y)) + solver.checkEntailed(\ + [solver.mkFalse(), solver.mkTerm(kinds.Distinct, x, y)]) + with pytest.raises(RuntimeError): + solver.checkEntailed(n) + with pytest.raises(RuntimeError): + solver.checkEntailed([n, solver.mkTerm(kinds.Distinct, x, y)]) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.checkEntailed(solver.mkTrue()) + + +def test_check_sat(solver): + solver.setOption("incremental", "false") + solver.checkSat() + with pytest.raises(RuntimeError): + solver.checkSat() + + +def test_check_sat_assuming(solver): + solver.setOption("incremental", "false") + solver.checkSatAssuming(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.checkSatAssuming(solver.mkTrue()) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.checkSatAssuming(solver.mkTrue()) + + +def test_check_sat_assuming1(solver): + boolSort = solver.getBooleanSort() + x = solver.mkConst(boolSort, "x") + y = solver.mkConst(boolSort, "y") + z = solver.mkTerm(kinds.And, x, y) + solver.setOption("incremental", "true") + solver.checkSatAssuming(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.checkSatAssuming(pycvc5.Term(solver)) + solver.checkSatAssuming(solver.mkTrue()) + solver.checkSatAssuming(z) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.checkSatAssuming(solver.mkTrue()) + + +def test_check_sat_assuming2(solver): + solver.setOption("incremental", "true") + + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + uToIntSort = solver.mkFunctionSort(uSort, intSort) + intPredSort = solver.mkFunctionSort(intSort, boolSort) + + n = pycvc5.Term(solver) + # Constants + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + # Functions + f = solver.mkConst(uToIntSort, "f") + p = solver.mkConst(intPredSort, "p") + # Values + zero = solver.mkInteger(0) + one = solver.mkInteger(1) + # Terms + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + summ = solver.mkTerm(kinds.Plus, f_x, f_y) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + # Assertions + assertions =\ + solver.mkTerm(kinds.And,\ + [solver.mkTerm(kinds.Leq, zero, f_x), # 0 <= f(x) + solver.mkTerm(kinds.Leq, zero, f_y), # 0 <= f(y) + solver.mkTerm(kinds.Leq, summ, one), # f(x) + f(y) <= 1 + p_0.notTerm(), # not p(0) + p_f_y # p(f(y)) + ]) + + solver.checkSatAssuming(solver.mkTrue()) + solver.assertFormula(assertions) + solver.checkSatAssuming(solver.mkTerm(kinds.Distinct, x, y)) + solver.checkSatAssuming( + [solver.mkFalse(), + solver.mkTerm(kinds.Distinct, x, y)]) + with pytest.raises(RuntimeError): + solver.checkSatAssuming(n) + with pytest.raises(RuntimeError): + solver.checkSatAssuming([n, solver.mkTerm(kinds.Distinct, x, y)]) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.checkSatAssuming(solver.mkTrue()) + + +def test_set_logic(solver): + solver.setLogic("AUFLIRA") + with pytest.raises(RuntimeError): + solver.setLogic("AF_BV") + solver.assertFormula(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.setLogic("AUFLIRA") + + +def test_set_option(solver): + solver.setOption("bv-sat-solver", "minisat") + with pytest.raises(RuntimeError): + solver.setOption("bv-sat-solver", "1") + solver.assertFormula(solver.mkTrue()) + with pytest.raises(RuntimeError): + solver.setOption("bv-sat-solver", "minisat") + + +def test_reset_assertions(solver): + solver.setOption("incremental", "true") + + bvSort = solver.mkBitVectorSort(4) + one = solver.mkBitVector(4, 1) + x = solver.mkConst(bvSort, "x") + ule = solver.mkTerm(kinds.BVUle, x, one) + srem = solver.mkTerm(kinds.BVSrem, one, x) + solver.push(4) + slt = solver.mkTerm(kinds.BVSlt, srem, one) + solver.resetAssertions() + solver.checkSatAssuming([slt, ule]) + + +def test_mk_sygus_grammar(solver): + nullTerm = pycvc5.Term(solver) + boolTerm = solver.mkBoolean(True) + boolVar = solver.mkVar(solver.getBooleanSort()) + intVar = solver.mkVar(solver.getIntegerSort()) + + solver.mkSygusGrammar([], [intVar]) + solver.mkSygusGrammar([boolVar], [intVar]) + with pytest.raises(RuntimeError): + solver.mkSygusGrammar([], []) + with pytest.raises(RuntimeError): + solver.mkSygusGrammar([], [nullTerm]) + with pytest.raises(RuntimeError): + solver.mkSygusGrammar([], [boolTerm]) + with pytest.raises(RuntimeError): + solver.mkSygusGrammar([boolTerm], [intVar]) + slv = pycvc5.Solver() + boolVar2 = slv.mkVar(slv.getBooleanSort()) + intVar2 = slv.mkVar(slv.getIntegerSort()) + slv.mkSygusGrammar([boolVar2], [intVar2]) + with pytest.raises(RuntimeError): + slv.mkSygusGrammar([boolVar], [intVar2]) + with pytest.raises(RuntimeError): + slv.mkSygusGrammar([boolVar2], [intVar]) + + +def test_synth_inv(solver): + boolean = solver.getBooleanSort() + integer = solver.getIntegerSort() + + nullTerm = pycvc5.Term(solver) + x = solver.mkVar(boolean) + + start1 = solver.mkVar(boolean) + start2 = solver.mkVar(integer) + + g1 = solver.mkSygusGrammar([x], [start1]) + g1.addRule(start1, solver.mkBoolean(False)) + + g2 = solver.mkSygusGrammar([x], [start2]) + g2.addRule(start2, solver.mkInteger(0)) + + solver.synthInv("", []) + solver.synthInv("i1", [x]) + solver.synthInv("i2", [x], g1) + + with pytest.raises(RuntimeError): + solver.synthInv("i3", [nullTerm]) + with pytest.raises(RuntimeError): + solver.synthInv("i4", [x], g2) + + +def test_add_sygus_constraint(solver): + nullTerm = pycvc5.Term(solver) + boolTerm = solver.mkBoolean(True) + intTerm = solver.mkInteger(1) + + solver.addSygusConstraint(boolTerm) + with pytest.raises(RuntimeError): + solver.addSygusConstraint(nullTerm) + with pytest.raises(RuntimeError): + solver.addSygusConstraint(intTerm) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.addSygusConstraint(boolTerm) + + +def test_add_sygus_inv_constraint(solver): + boolean = solver.getBooleanSort() + real = solver.getRealSort() + + nullTerm = pycvc5.Term(solver) + intTerm = solver.mkInteger(1) + + inv = solver.declareFun("inv", [real], boolean) + pre = solver.declareFun("pre", [real], boolean) + trans = solver.declareFun("trans", [real, real], boolean) + post = solver.declareFun("post", [real], boolean) + + inv1 = solver.declareFun("inv1", [real], real) + + trans1 = solver.declareFun("trans1", [boolean, real], boolean) + trans2 = solver.declareFun("trans2", [real, boolean], boolean) + trans3 = solver.declareFun("trans3", [real, real], real) + + solver.addSygusInvConstraint(inv, pre, trans, post) + + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(nullTerm, pre, trans, post) + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, nullTerm, trans, post) + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, nullTerm, post) + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, trans, nullTerm) + + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(intTerm, pre, trans, post) + + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv1, pre, trans, post) + + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, trans, trans, post) + + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, intTerm, post) + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, pre, post) + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, trans1, post) + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, trans2, post) + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, trans3, post) + + with pytest.raises(RuntimeError): + solver.addSygusInvConstraint(inv, pre, trans, trans) + slv = pycvc5.Solver() + boolean2 = slv.getBooleanSort() + real2 = slv.getRealSort() + inv22 = slv.declareFun("inv", [real2], boolean2) + pre22 = slv.declareFun("pre", [real2], boolean2) + trans22 = slv.declareFun("trans", [real2, real2], boolean2) + post22 = slv.declareFun("post", [real2], boolean2) + slv.addSygusInvConstraint(inv22, pre22, trans22, post22) + with pytest.raises(RuntimeError): + slv.addSygusInvConstraint(inv, pre22, trans22, post22) + with pytest.raises(RuntimeError): + slv.addSygusInvConstraint(inv22, pre, trans22, post22) + with pytest.raises(RuntimeError): + slv.addSygusInvConstraint(inv22, pre22, trans, post22) + with pytest.raises(RuntimeError): + slv.addSygusInvConstraint(inv22, pre22, trans22, post) + + +def test_get_synth_solution(solver): + solver.setOption("lang", "sygus2") + solver.setOption("incremental", "false") + + nullTerm = pycvc5.Term(solver) + x = solver.mkBoolean(False) + f = solver.synthFun("f", [], solver.getBooleanSort()) + + with pytest.raises(RuntimeError): + solver.getSynthSolution(f) + + solver.checkSynth() + + solver.getSynthSolution(f) + solver.getSynthSolution(f) + + with pytest.raises(RuntimeError): + solver.getSynthSolution(nullTerm) + with pytest.raises(RuntimeError): + solver.getSynthSolution(x) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.getSynthSolution(f) diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py new file mode 100644 index 000000000..98cf76d76 --- /dev/null +++ b/test/unit/api/python/test_sort.py @@ -0,0 +1,575 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Makai Mann +# +# 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. +# ############################################################################# +# +# Unit tests for sort API. +# +# Obtained by translating test/unit/api/sort_black.cpp +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def create_datatype_sort(solver): + intSort = solver.getIntegerSort() + # create datatype sort to test + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", intSort) + cons.addSelectorSelf("tail") + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + return dtypeSort + + +def create_param_datatype_sort(solver): + sort = solver.mkParamSort("T") + paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) + paramCons = solver.mkDatatypeConstructorDecl("cons") + paramNil = solver.mkDatatypeConstructorDecl("nil") + paramCons.addSelector("head", sort) + paramDtypeSpec.addConstructor(paramCons) + paramDtypeSpec.addConstructor(paramNil) + paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) + return paramDtypeSort + + +def test_operators_comparison(solver): + solver.getIntegerSort() == Sort(solver) + solver.getIntegerSort() != Sort(solver) + solver.getIntegerSort() < Sort(solver) + solver.getIntegerSort() <= Sort(solver) + solver.getIntegerSort() > Sort(solver) + solver.getIntegerSort() >= Sort(solver) + +def test_is_null(solver): + x = Sort(solver) + assert x.isNull() + x = solver.getBooleanSort() + assert not x.isNull() + +def test_is_boolean(solver): + assert solver.getBooleanSort().isBoolean() + Sort(solver).isBoolean() + + +def test_is_integer(solver): + assert solver.getIntegerSort().isInteger() + assert not solver.getRealSort().isInteger() + Sort(solver).isInteger() + + +def test_is_real(solver): + assert solver.getRealSort().isReal() + assert not solver.getIntegerSort().isReal() + Sort(solver).isReal() + + +def test_is_string(solver): + assert solver.getStringSort().isString() + Sort(solver).isString() + + +def test_is_reg_exp(solver): + assert solver.getRegExpSort().isRegExp() + Sort(solver).isRegExp() + + +def test_is_rounding_mode(solver): + assert solver.getRoundingModeSort().isRoundingMode() + Sort(solver).isRoundingMode() + + +def test_is_bit_vector(solver): + assert solver.mkBitVectorSort(8).isBitVector() + Sort(solver).isBitVector() + + +def test_is_floating_point(solver): + assert solver.mkFloatingPointSort(8, 24).isFloatingPoint() + Sort(solver).isFloatingPoint() + + +def test_is_datatype(solver): + dt_sort = create_datatype_sort(solver) + assert dt_sort.isDatatype() + Sort(solver).isDatatype() + + +def test_is_parametric_datatype(solver): + param_dt_sort = create_param_datatype_sort(solver) + assert param_dt_sort.isParametricDatatype() + Sort(solver).isParametricDatatype() + + +def test_is_constructor(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + cons_sort = dt[0].getConstructorTerm().getSort() + assert cons_sort.isConstructor() + Sort(solver).isConstructor() + + +def test_is_selector(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + dt0 = dt[0] + dt01 = dt0[1] + cons_sort = dt01.getSelectorTerm().getSort() + assert cons_sort.isSelector() + Sort(solver).isSelector() + + +def test_is_tester(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + cons_sort = dt[0].getTesterTerm().getSort() + assert cons_sort.isTester() + Sort(solver).isTester() + +def test_is_updater(solver): + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + updater_sort = dt[0][0].getUpdaterTerm().getSort() + assert updater_sort.isUpdater() + Sort(solver).isUpdater() + +def test_is_function(solver): + fun_sort = solver.mkFunctionSort(solver.getRealSort(), + solver.getIntegerSort()) + assert fun_sort.isFunction() + Sort(solver).isFunction() + + +def test_is_predicate(solver): + pred_sort = solver.mkPredicateSort(solver.getRealSort()) + assert pred_sort.isPredicate() + Sort(solver).isPredicate() + + +def test_is_tuple(solver): + tup_sort = solver.mkTupleSort(solver.getRealSort()) + assert tup_sort.isTuple() + Sort(solver).isTuple() + + +def test_is_record(solver): + rec_sort = solver.mkRecordSort([("asdf", solver.getRealSort())]) + assert rec_sort.isRecord() + Sort(solver).isRecord() + + +def test_is_array(solver): + arr_sort = solver.mkArraySort(solver.getRealSort(), + solver.getIntegerSort()) + assert arr_sort.isArray() + Sort(solver).isArray() + + +def test_is_set(solver): + set_sort = solver.mkSetSort(solver.getRealSort()) + assert set_sort.isSet() + Sort(solver).isSet() + + +def test_is_bag(solver): + bag_sort = solver.mkBagSort(solver.getRealSort()) + assert bag_sort.isBag() + Sort(solver).isBag() + + +def test_is_sequence(solver): + seq_sort = solver.mkSequenceSort(solver.getRealSort()) + assert seq_sort.isSequence() + Sort(solver).isSequence() + + +def test_is_uninterpreted(solver): + un_sort = solver.mkUninterpretedSort("asdf") + assert un_sort.isUninterpretedSort() + Sort(solver).isUninterpretedSort() + + +def test_is_sort_constructor(solver): + sc_sort = solver.mkSortConstructorSort("asdf", 1) + assert sc_sort.isSortConstructor() + Sort(solver).isSortConstructor() + + +def test_is_first_class(solver): + fun_sort = solver.mkFunctionSort(solver.getRealSort(), + solver.getIntegerSort()) + assert solver.getIntegerSort().isFirstClass() + assert fun_sort.isFirstClass() + reSort = solver.getRegExpSort() + assert not reSort.isFirstClass() + Sort(solver).isFirstClass() + + +def test_is_function_like(solver): + fun_sort = solver.mkFunctionSort(solver.getRealSort(), + solver.getIntegerSort()) + assert not solver.getIntegerSort().isFunctionLike() + assert fun_sort.isFunctionLike() + + dt_sort = create_datatype_sort(solver) + dt = dt_sort.getDatatype() + cons_sort = dt[0][1].getSelectorTerm().getSort() + assert cons_sort.isFunctionLike() + + Sort(solver).isFunctionLike() + + +def test_is_subsort_of(solver): + assert solver.getIntegerSort().isSubsortOf(solver.getIntegerSort()) + assert solver.getIntegerSort().isSubsortOf(solver.getRealSort()) + assert not solver.getIntegerSort().isSubsortOf(solver.getBooleanSort()) + Sort(solver).isSubsortOf(Sort(solver)) + + +def test_is_comparable_to(solver): + assert solver.getIntegerSort().isComparableTo(solver.getIntegerSort()) + assert solver.getIntegerSort().isComparableTo(solver.getRealSort()) + assert not solver.getIntegerSort().isComparableTo(solver.getBooleanSort()) + Sort(solver).isComparableTo(Sort(solver)) + + +def test_get_datatype(solver): + dtypeSort = create_datatype_sort(solver) + dtypeSort.getDatatype() + # create bv sort, check should fail + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getDatatype() + + +def test_datatype_sorts(solver): + intSort = solver.getIntegerSort() + dtypeSort = create_datatype_sort(solver) + dt = dtypeSort.getDatatype() + assert not dtypeSort.isConstructor() + with pytest.raises(RuntimeError): + dtypeSort.getConstructorCodomainSort() + with pytest.raises(RuntimeError): + dtypeSort.getConstructorDomainSorts() + with pytest.raises(RuntimeError): + dtypeSort.getConstructorArity() + + # get constructor + dcons = dt[0] + consTerm = dcons.getConstructorTerm() + consSort = consTerm.getSort() + assert consSort.isConstructor() + assert not consSort.isTester() + assert not consSort.isSelector() + assert consSort.getConstructorArity() == 2 + consDomSorts = consSort.getConstructorDomainSorts() + assert consDomSorts[0] == intSort + assert consDomSorts[1] == dtypeSort + assert consSort.getConstructorCodomainSort() == dtypeSort + + # get tester + isConsTerm = dcons.getTesterTerm() + assert isConsTerm.getSort().isTester() + booleanSort = solver.getBooleanSort() + + assert isConsTerm.getSort().getTesterDomainSort() == dtypeSort + assert isConsTerm.getSort().getTesterCodomainSort() == booleanSort + with pytest.raises(RuntimeError): + booleanSort.getTesterDomainSort() + with pytest.raises(RuntimeError): + booleanSort.getTesterCodomainSort() + + # get selector + dselTail = dcons[1] + tailTerm = dselTail.getSelectorTerm() + assert tailTerm.getSort().isSelector() + assert tailTerm.getSort().getSelectorDomainSort() == dtypeSort + assert tailTerm.getSort().getSelectorCodomainSort() == dtypeSort + with pytest.raises(RuntimeError): + booleanSort.getSelectorDomainSort() + with pytest.raises(RuntimeError): + booleanSort.getSelectorCodomainSort() + + +def test_instantiate(solver): + # instantiate parametric datatype, check should not fail + paramDtypeSort = create_param_datatype_sort(solver) + paramDtypeSort.instantiate([solver.getIntegerSort()]) + # instantiate non-parametric datatype sort, check should fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + with pytest.raises(RuntimeError): + dtypeSort.instantiate([solver.getIntegerSort()]) + + +def test_get_function_arity(solver): + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionArity() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getFunctionArity() + + +def test_get_function_domain_sorts(solver): + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionDomainSorts() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getFunctionDomainSorts() + + +def test_get_function_codomain_sort(solver): + funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"), + solver.getIntegerSort()) + funSort.getFunctionCodomainSort() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getFunctionCodomainSort() + + +def test_get_array_index_sort(solver): + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayIndexSort() + with pytest.raises(RuntimeError): + indexSort.getArrayIndexSort() + + +def test_get_array_element_sort(solver): + elementSort = solver.mkBitVectorSort(32) + indexSort = solver.mkBitVectorSort(32) + arraySort = solver.mkArraySort(indexSort, elementSort) + arraySort.getArrayElementSort() + with pytest.raises(RuntimeError): + indexSort.getArrayElementSort() + + +def test_get_set_element_sort(solver): + setSort = solver.mkSetSort(solver.getIntegerSort()) + setSort.getSetElementSort() + elementSort = setSort.getSetElementSort() + assert elementSort == solver.getIntegerSort() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getSetElementSort() + + +def test_get_bag_element_sort(solver): + bagSort = solver.mkBagSort(solver.getIntegerSort()) + bagSort.getBagElementSort() + elementSort = bagSort.getBagElementSort() + assert elementSort == solver.getIntegerSort() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getBagElementSort() + + +def test_get_sequence_element_sort(solver): + seqSort = solver.mkSequenceSort(solver.getIntegerSort()) + assert seqSort.isSequence() + seqSort.getSequenceElementSort() + bvSort = solver.mkBitVectorSort(32) + assert not bvSort.isSequence() + with pytest.raises(RuntimeError): + bvSort.getSequenceElementSort() + + +def test_get_uninterpreted_sort_name(solver): + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortName() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getUninterpretedSortName() + + +def test_is_uninterpreted_sort_parameterized(solver): + uSort = solver.mkUninterpretedSort("u") + assert not uSort.isUninterpretedSortParameterized() + sSort = solver.mkSortConstructorSort("s", 1) + siSort = sSort.instantiate([uSort]) + assert siSort.isUninterpretedSortParameterized() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.isUninterpretedSortParameterized() + + +def test_get_uninterpreted_sort_paramsorts(solver): + uSort = solver.mkUninterpretedSort("u") + uSort.getUninterpretedSortParamSorts() + sSort = solver.mkSortConstructorSort("s", 2) + siSort = sSort.instantiate([uSort, uSort]) + assert len(siSort.getUninterpretedSortParamSorts()) == 2 + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getUninterpretedSortParamSorts() + + +def test_get_uninterpreted_sort_constructor_name(solver): + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorName() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getSortConstructorName() + + +def test_get_uninterpreted_sort_constructor_arity(solver): + sSort = solver.mkSortConstructorSort("s", 2) + sSort.getSortConstructorArity() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getSortConstructorArity() + + +def test_get_bv_size(solver): + bvSort = solver.mkBitVectorSort(32) + bvSort.getBitVectorSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getBitVectorSize() + + +def test_get_fp_exponent_size(solver): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFloatingPointExponentSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFloatingPointExponentSize() + + +def test_get_fp_significand_size(solver): + fpSort = solver.mkFloatingPointSort(4, 8) + fpSort.getFloatingPointSignificandSize() + setSort = solver.mkSetSort(solver.getIntegerSort()) + with pytest.raises(RuntimeError): + setSort.getFloatingPointSignificandSize() + + +def test_get_datatype_paramsorts(solver): + # create parametric datatype, check should not fail + sort = solver.mkParamSort("T") + paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort) + paramCons = solver.mkDatatypeConstructorDecl("cons") + paramNil = solver.mkDatatypeConstructorDecl("nil") + paramCons.addSelector("head", sort) + paramDtypeSpec.addConstructor(paramCons) + paramDtypeSpec.addConstructor(paramNil) + paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec) + paramDtypeSort.getDatatypeParamSorts() + # create non-parametric datatype sort, check should fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + with pytest.raises(RuntimeError): + dtypeSort.getDatatypeParamSorts() + + +def test_get_datatype_arity(solver): + # create datatype sort, check should not fail + dtypeSpec = solver.mkDatatypeDecl("list") + cons = solver.mkDatatypeConstructorDecl("cons") + cons.addSelector("head", solver.getIntegerSort()) + dtypeSpec.addConstructor(cons) + nil = solver.mkDatatypeConstructorDecl("nil") + dtypeSpec.addConstructor(nil) + dtypeSort = solver.mkDatatypeSort(dtypeSpec) + dtypeSort.getDatatypeArity() + # create bv sort, check should fail + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getDatatypeArity() + + +def test_get_tuple_length(solver): + tupleSort = solver.mkTupleSort( + [solver.getIntegerSort(), + solver.getIntegerSort()]) + tupleSort.getTupleLength() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getTupleLength() + + +def test_get_tuple_sorts(solver): + tupleSort = solver.mkTupleSort( + [solver.getIntegerSort(), + solver.getIntegerSort()]) + tupleSort.getTupleSorts() + bvSort = solver.mkBitVectorSort(32) + with pytest.raises(RuntimeError): + bvSort.getTupleSorts() + + +def test_sort_compare(solver): + boolSort = solver.getBooleanSort() + intSort = solver.getIntegerSort() + bvSort = solver.mkBitVectorSort(32) + bvSort2 = solver.mkBitVectorSort(32) + assert bvSort >= bvSort2 + assert bvSort <= bvSort2 + assert (intSort > boolSort) != (intSort < boolSort) + assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort) + + +def test_sort_subtyping(solver): + intSort = solver.getIntegerSort() + realSort = solver.getRealSort() + assert intSort.isSubsortOf(realSort) + assert not realSort.isSubsortOf(intSort) + assert intSort.isComparableTo(realSort) + assert realSort.isComparableTo(intSort) + + arraySortII = solver.mkArraySort(intSort, intSort) + arraySortIR = solver.mkArraySort(intSort, realSort) + assert not arraySortII.isComparableTo(intSort) + # we do not support subtyping for arrays + assert not arraySortII.isComparableTo(arraySortIR) + + setSortI = solver.mkSetSort(intSort) + setSortR = solver.mkSetSort(realSort) + # we don't support subtyping for sets + assert not setSortI.isComparableTo(setSortR) + assert not setSortI.isSubsortOf(setSortR) + assert not setSortR.isComparableTo(setSortI) + assert not setSortR.isSubsortOf(setSortI) + + +def test_sort_scoped_tostring(solver): + name = "uninterp-sort" + bvsort8 = solver.mkBitVectorSort(8) + uninterp_sort = solver.mkUninterpretedSort(name) + assert str(bvsort8) == "(_ BitVec 8)" + assert str(uninterp_sort) == name + solver2 = pycvc5.Solver() + assert str(bvsort8) == "(_ BitVec 8)" + assert str(uninterp_sort) == name diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py new file mode 100644 index 000000000..49314638f --- /dev/null +++ b/test/unit/api/python/test_term.py @@ -0,0 +1,1284 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Makai Mann, Andres Noetzli +# +# 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. +# ############################################################################# +## + +import pytest +import pycvc5 +from pycvc5 import kinds +from pycvc5 import Sort, Term +from fractions import Fraction + + +@pytest.fixture +def solver(): + return pycvc5.Solver() + + +def test_eq(solver): + uSort = solver.mkUninterpretedSort("u") + x = solver.mkVar(uSort, "x") + y = solver.mkVar(uSort, "y") + z = Term(solver) + + assert x == x + assert not x != x + assert not x == y + assert x != y + assert not (x == z) + assert x != z + + +def test_get_id(solver): + n = Term(solver) + with pytest.raises(RuntimeError): + n.getId() + x = solver.mkVar(solver.getIntegerSort(), "x") + x.getId() + y = x + assert x.getId() == y.getId() + + z = solver.mkVar(solver.getIntegerSort(), "z") + assert x.getId() != z.getId() + + +def test_get_kind(solver): + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(uSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + n = Term(solver) + with pytest.raises(RuntimeError): + n.getKind() + x = solver.mkVar(uSort, "x") + x.getKind() + y = solver.mkVar(uSort, "y") + y.getKind() + + f = solver.mkVar(funSort1, "f") + f.getKind() + p = solver.mkVar(funSort2, "p") + p.getKind() + + zero = solver.mkInteger(0) + zero.getKind() + + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x.getKind() + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y.getKind() + sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum.getKind() + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.getKind() + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y.getKind() + + # Sequence kinds do not exist internally, test that the API properly + # converts them back. + seqSort = solver.mkSequenceSort(intSort) + s = solver.mkConst(seqSort, "s") + ss = solver.mkTerm(kinds.SeqConcat, s, s) + assert ss.getKind() == kinds.SeqConcat + + +def test_get_sort(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + n = Term(solver) + with pytest.raises(RuntimeError): + n.getSort() + x = solver.mkVar(bvSort, "x") + x.getSort() + assert x.getSort() == bvSort + y = solver.mkVar(bvSort, "y") + y.getSort() + assert y.getSort() == bvSort + + f = solver.mkVar(funSort1, "f") + f.getSort() + assert f.getSort() == funSort1 + p = solver.mkVar(funSort2, "p") + p.getSort() + assert p.getSort() == funSort2 + + zero = solver.mkInteger(0) + zero.getSort() + assert zero.getSort() == intSort + + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + f_x.getSort() + assert f_x.getSort() == intSort + f_y = solver.mkTerm(kinds.ApplyUf, f, y) + f_y.getSort() + assert f_y.getSort() == intSort + sum = solver.mkTerm(kinds.Plus, f_x, f_y) + sum.getSort() + assert sum.getSort() == intSort + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.getSort() + assert p_0.getSort() == boolSort + p_f_y = solver.mkTerm(kinds.ApplyUf, p, f_y) + p_f_y.getSort() + assert p_f_y.getSort() == boolSort + + +def test_get_op(solver): + intsort = solver.getIntegerSort() + bvsort = solver.mkBitVectorSort(8) + arrsort = solver.mkArraySort(bvsort, intsort) + funsort = solver.mkFunctionSort(intsort, bvsort) + + x = solver.mkConst(intsort, "x") + a = solver.mkConst(arrsort, "a") + b = solver.mkConst(bvsort, "b") + + assert not x.hasOp() + with pytest.raises(RuntimeError): + x.getOp() + + ab = solver.mkTerm(kinds.Select, a, b) + ext = solver.mkOp(kinds.BVExtract, 4, 0) + extb = solver.mkTerm(ext, b) + + assert ab.hasOp() + assert not ab.getOp().isIndexed() + # can compare directly to a Kind (will invoke constructor) + assert extb.hasOp() + assert extb.getOp().isIndexed() + assert extb.getOp() == ext + + f = solver.mkConst(funsort, "f") + fx = solver.mkTerm(kinds.ApplyUf, f, x) + + assert not f.hasOp() + with pytest.raises(RuntimeError): + f.getOp() + assert fx.hasOp() + children = [c for c in fx] + # testing rebuild from op and children + assert fx == solver.mkTerm(fx.getOp(), children) + + # Test Datatypes Ops + sort = solver.mkParamSort("T") + listDecl = solver.mkDatatypeDecl("paramlist", sort) + cons = solver.mkDatatypeConstructorDecl("cons") + nil = solver.mkDatatypeConstructorDecl("nil") + cons.addSelector("head", sort) + cons.addSelectorSelf("tail") + listDecl.addConstructor(cons) + listDecl.addConstructor(nil) + listSort = solver.mkDatatypeSort(listDecl) + intListSort = listSort.instantiate([solver.getIntegerSort()]) + c = solver.mkConst(intListSort, "c") + list1 = listSort.getDatatype() + # list datatype constructor and selector operator terms + consOpTerm = list1.getConstructorTerm("cons") + nilOpTerm = list1.getConstructorTerm("nil") + headOpTerm = list1["cons"].getSelectorTerm("head") + tailOpTerm = list1["cons"].getSelectorTerm("tail") + + nilTerm = solver.mkTerm(kinds.ApplyConstructor, nilOpTerm) + consTerm = solver.mkTerm(kinds.ApplyConstructor, consOpTerm, + solver.mkInteger(0), nilTerm) + headTerm = solver.mkTerm(kinds.ApplySelector, headOpTerm, consTerm) + tailTerm = solver.mkTerm(kinds.ApplySelector, tailOpTerm, consTerm) + + assert nilTerm.hasOp() + assert consTerm.hasOp() + assert headTerm.hasOp() + assert tailTerm.hasOp() + + # Test rebuilding + children = [c for c in headTerm] + assert headTerm == solver.mkTerm(headTerm.getOp(), children) + + +def test_has_get_symbol(solver): + n = Term(solver) + t = solver.mkBoolean(True) + c = solver.mkConst(solver.getBooleanSort(), "|\\|") + + with pytest.raises(RuntimeError): + n.hasSymbol() + assert not t.hasSymbol() + assert c.hasSymbol() + + with pytest.raises(RuntimeError): + n.getSymbol() + with pytest.raises(RuntimeError): + t.getSymbol() + assert c.getSymbol() == "|\\|" + + +def test_is_null(solver): + x = Term(solver) + assert x.isNull() + x = solver.mkVar(solver.mkBitVectorSort(4), "x") + assert not x.isNull() + + +def test_not_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + with pytest.raises(RuntimeError): + Term(solver).notTerm() + b = solver.mkTrue() + b.notTerm() + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.notTerm() + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.notTerm() + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.notTerm() + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.notTerm() + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.notTerm() + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.notTerm() + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.notTerm() + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.notTerm() + + +def test_and_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).andTerm(b) + with pytest.raises(RuntimeError): + b.andTerm(Term(solver)) + b.andTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.andTerm(b) + with pytest.raises(RuntimeError): + x.andTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.andTerm(b) + with pytest.raises(RuntimeError): + f.andTerm(x) + with pytest.raises(RuntimeError): + f.andTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.andTerm(b) + with pytest.raises(RuntimeError): + p.andTerm(x) + with pytest.raises(RuntimeError): + p.andTerm(f) + with pytest.raises(RuntimeError): + p.andTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.andTerm(b) + with pytest.raises(RuntimeError): + zero.andTerm(x) + with pytest.raises(RuntimeError): + zero.andTerm(f) + with pytest.raises(RuntimeError): + zero.andTerm(p) + with pytest.raises(RuntimeError): + zero.andTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.andTerm(b) + with pytest.raises(RuntimeError): + f_x.andTerm(x) + with pytest.raises(RuntimeError): + f_x.andTerm(f) + with pytest.raises(RuntimeError): + f_x.andTerm(p) + with pytest.raises(RuntimeError): + f_x.andTerm(zero) + with pytest.raises(RuntimeError): + f_x.andTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.andTerm(b) + with pytest.raises(RuntimeError): + sum.andTerm(x) + with pytest.raises(RuntimeError): + sum.andTerm(f) + with pytest.raises(RuntimeError): + sum.andTerm(p) + with pytest.raises(RuntimeError): + sum.andTerm(zero) + with pytest.raises(RuntimeError): + sum.andTerm(f_x) + with pytest.raises(RuntimeError): + sum.andTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.andTerm(b) + with pytest.raises(RuntimeError): + p_0.andTerm(x) + with pytest.raises(RuntimeError): + p_0.andTerm(f) + with pytest.raises(RuntimeError): + p_0.andTerm(p) + with pytest.raises(RuntimeError): + p_0.andTerm(zero) + with pytest.raises(RuntimeError): + p_0.andTerm(f_x) + with pytest.raises(RuntimeError): + p_0.andTerm(sum) + p_0.andTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.andTerm(b) + with pytest.raises(RuntimeError): + p_f_x.andTerm(x) + with pytest.raises(RuntimeError): + p_f_x.andTerm(f) + with pytest.raises(RuntimeError): + p_f_x.andTerm(p) + with pytest.raises(RuntimeError): + p_f_x.andTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.andTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.andTerm(sum) + p_f_x.andTerm(p_0) + p_f_x.andTerm(p_f_x) + + +def test_or_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).orTerm(b) + with pytest.raises(RuntimeError): + b.orTerm(Term(solver)) + b.orTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.orTerm(b) + with pytest.raises(RuntimeError): + x.orTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.orTerm(b) + with pytest.raises(RuntimeError): + f.orTerm(x) + with pytest.raises(RuntimeError): + f.orTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.orTerm(b) + with pytest.raises(RuntimeError): + p.orTerm(x) + with pytest.raises(RuntimeError): + p.orTerm(f) + with pytest.raises(RuntimeError): + p.orTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.orTerm(b) + with pytest.raises(RuntimeError): + zero.orTerm(x) + with pytest.raises(RuntimeError): + zero.orTerm(f) + with pytest.raises(RuntimeError): + zero.orTerm(p) + with pytest.raises(RuntimeError): + zero.orTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.orTerm(b) + with pytest.raises(RuntimeError): + f_x.orTerm(x) + with pytest.raises(RuntimeError): + f_x.orTerm(f) + with pytest.raises(RuntimeError): + f_x.orTerm(p) + with pytest.raises(RuntimeError): + f_x.orTerm(zero) + with pytest.raises(RuntimeError): + f_x.orTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.orTerm(b) + with pytest.raises(RuntimeError): + sum.orTerm(x) + with pytest.raises(RuntimeError): + sum.orTerm(f) + with pytest.raises(RuntimeError): + sum.orTerm(p) + with pytest.raises(RuntimeError): + sum.orTerm(zero) + with pytest.raises(RuntimeError): + sum.orTerm(f_x) + with pytest.raises(RuntimeError): + sum.orTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.orTerm(b) + with pytest.raises(RuntimeError): + p_0.orTerm(x) + with pytest.raises(RuntimeError): + p_0.orTerm(f) + with pytest.raises(RuntimeError): + p_0.orTerm(p) + with pytest.raises(RuntimeError): + p_0.orTerm(zero) + with pytest.raises(RuntimeError): + p_0.orTerm(f_x) + with pytest.raises(RuntimeError): + p_0.orTerm(sum) + p_0.orTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.orTerm(b) + with pytest.raises(RuntimeError): + p_f_x.orTerm(x) + with pytest.raises(RuntimeError): + p_f_x.orTerm(f) + with pytest.raises(RuntimeError): + p_f_x.orTerm(p) + with pytest.raises(RuntimeError): + p_f_x.orTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.orTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.orTerm(sum) + p_f_x.orTerm(p_0) + p_f_x.orTerm(p_f_x) + + +def test_xor_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).xorTerm(b) + with pytest.raises(RuntimeError): + b.xorTerm(Term(solver)) + b.xorTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.xorTerm(b) + with pytest.raises(RuntimeError): + x.xorTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.xorTerm(b) + with pytest.raises(RuntimeError): + f.xorTerm(x) + with pytest.raises(RuntimeError): + f.xorTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.xorTerm(b) + with pytest.raises(RuntimeError): + p.xorTerm(x) + with pytest.raises(RuntimeError): + p.xorTerm(f) + with pytest.raises(RuntimeError): + p.xorTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.xorTerm(b) + with pytest.raises(RuntimeError): + zero.xorTerm(x) + with pytest.raises(RuntimeError): + zero.xorTerm(f) + with pytest.raises(RuntimeError): + zero.xorTerm(p) + with pytest.raises(RuntimeError): + zero.xorTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.xorTerm(b) + with pytest.raises(RuntimeError): + f_x.xorTerm(x) + with pytest.raises(RuntimeError): + f_x.xorTerm(f) + with pytest.raises(RuntimeError): + f_x.xorTerm(p) + with pytest.raises(RuntimeError): + f_x.xorTerm(zero) + with pytest.raises(RuntimeError): + f_x.xorTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.xorTerm(b) + with pytest.raises(RuntimeError): + sum.xorTerm(x) + with pytest.raises(RuntimeError): + sum.xorTerm(f) + with pytest.raises(RuntimeError): + sum.xorTerm(p) + with pytest.raises(RuntimeError): + sum.xorTerm(zero) + with pytest.raises(RuntimeError): + sum.xorTerm(f_x) + with pytest.raises(RuntimeError): + sum.xorTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.xorTerm(b) + with pytest.raises(RuntimeError): + p_0.xorTerm(x) + with pytest.raises(RuntimeError): + p_0.xorTerm(f) + with pytest.raises(RuntimeError): + p_0.xorTerm(p) + with pytest.raises(RuntimeError): + p_0.xorTerm(zero) + with pytest.raises(RuntimeError): + p_0.xorTerm(f_x) + with pytest.raises(RuntimeError): + p_0.xorTerm(sum) + p_0.xorTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.xorTerm(b) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(x) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(f) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(p) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.xorTerm(sum) + p_f_x.xorTerm(p_0) + p_f_x.xorTerm(p_f_x) + + +def test_eq_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).eqTerm(b) + with pytest.raises(RuntimeError): + b.eqTerm(Term(solver)) + b.eqTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.eqTerm(b) + x.eqTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.eqTerm(b) + with pytest.raises(RuntimeError): + f.eqTerm(x) + f.eqTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.eqTerm(b) + with pytest.raises(RuntimeError): + p.eqTerm(x) + with pytest.raises(RuntimeError): + p.eqTerm(f) + p.eqTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.eqTerm(b) + with pytest.raises(RuntimeError): + zero.eqTerm(x) + with pytest.raises(RuntimeError): + zero.eqTerm(f) + with pytest.raises(RuntimeError): + zero.eqTerm(p) + zero.eqTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.eqTerm(b) + with pytest.raises(RuntimeError): + f_x.eqTerm(x) + with pytest.raises(RuntimeError): + f_x.eqTerm(f) + with pytest.raises(RuntimeError): + f_x.eqTerm(p) + f_x.eqTerm(zero) + f_x.eqTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.eqTerm(b) + with pytest.raises(RuntimeError): + sum.eqTerm(x) + with pytest.raises(RuntimeError): + sum.eqTerm(f) + with pytest.raises(RuntimeError): + sum.eqTerm(p) + sum.eqTerm(zero) + sum.eqTerm(f_x) + sum.eqTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.eqTerm(b) + with pytest.raises(RuntimeError): + p_0.eqTerm(x) + with pytest.raises(RuntimeError): + p_0.eqTerm(f) + with pytest.raises(RuntimeError): + p_0.eqTerm(p) + with pytest.raises(RuntimeError): + p_0.eqTerm(zero) + with pytest.raises(RuntimeError): + p_0.eqTerm(f_x) + with pytest.raises(RuntimeError): + p_0.eqTerm(sum) + p_0.eqTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.eqTerm(b) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(x) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(f) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(p) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.eqTerm(sum) + p_f_x.eqTerm(p_0) + p_f_x.eqTerm(p_f_x) + + +def test_imp_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).impTerm(b) + with pytest.raises(RuntimeError): + b.impTerm(Term(solver)) + b.impTerm(b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + with pytest.raises(RuntimeError): + x.impTerm(b) + with pytest.raises(RuntimeError): + x.impTerm(x) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.impTerm(b) + with pytest.raises(RuntimeError): + f.impTerm(x) + with pytest.raises(RuntimeError): + f.impTerm(f) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.impTerm(b) + with pytest.raises(RuntimeError): + p.impTerm(x) + with pytest.raises(RuntimeError): + p.impTerm(f) + with pytest.raises(RuntimeError): + p.impTerm(p) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.impTerm(b) + with pytest.raises(RuntimeError): + zero.impTerm(x) + with pytest.raises(RuntimeError): + zero.impTerm(f) + with pytest.raises(RuntimeError): + zero.impTerm(p) + with pytest.raises(RuntimeError): + zero.impTerm(zero) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.impTerm(b) + with pytest.raises(RuntimeError): + f_x.impTerm(x) + with pytest.raises(RuntimeError): + f_x.impTerm(f) + with pytest.raises(RuntimeError): + f_x.impTerm(p) + with pytest.raises(RuntimeError): + f_x.impTerm(zero) + with pytest.raises(RuntimeError): + f_x.impTerm(f_x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.impTerm(b) + with pytest.raises(RuntimeError): + sum.impTerm(x) + with pytest.raises(RuntimeError): + sum.impTerm(f) + with pytest.raises(RuntimeError): + sum.impTerm(p) + with pytest.raises(RuntimeError): + sum.impTerm(zero) + with pytest.raises(RuntimeError): + sum.impTerm(f_x) + with pytest.raises(RuntimeError): + sum.impTerm(sum) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.impTerm(b) + with pytest.raises(RuntimeError): + p_0.impTerm(x) + with pytest.raises(RuntimeError): + p_0.impTerm(f) + with pytest.raises(RuntimeError): + p_0.impTerm(p) + with pytest.raises(RuntimeError): + p_0.impTerm(zero) + with pytest.raises(RuntimeError): + p_0.impTerm(f_x) + with pytest.raises(RuntimeError): + p_0.impTerm(sum) + p_0.impTerm(p_0) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.impTerm(b) + with pytest.raises(RuntimeError): + p_f_x.impTerm(x) + with pytest.raises(RuntimeError): + p_f_x.impTerm(f) + with pytest.raises(RuntimeError): + p_f_x.impTerm(p) + with pytest.raises(RuntimeError): + p_f_x.impTerm(zero) + with pytest.raises(RuntimeError): + p_f_x.impTerm(f_x) + with pytest.raises(RuntimeError): + p_f_x.impTerm(sum) + p_f_x.impTerm(p_0) + p_f_x.impTerm(p_f_x) + + +def test_ite_term(solver): + bvSort = solver.mkBitVectorSort(8) + intSort = solver.getIntegerSort() + boolSort = solver.getBooleanSort() + funSort1 = solver.mkFunctionSort(bvSort, intSort) + funSort2 = solver.mkFunctionSort(intSort, boolSort) + + b = solver.mkTrue() + with pytest.raises(RuntimeError): + Term(solver).iteTerm(b, b) + with pytest.raises(RuntimeError): + b.iteTerm(Term(solver), b) + with pytest.raises(RuntimeError): + b.iteTerm(b, Term(solver)) + b.iteTerm(b, b) + x = solver.mkVar(solver.mkBitVectorSort(8), "x") + b.iteTerm(x, x) + b.iteTerm(b, b) + with pytest.raises(RuntimeError): + b.iteTerm(x, b) + with pytest.raises(RuntimeError): + x.iteTerm(x, x) + with pytest.raises(RuntimeError): + x.iteTerm(x, b) + f = solver.mkVar(funSort1, "f") + with pytest.raises(RuntimeError): + f.iteTerm(b, b) + with pytest.raises(RuntimeError): + x.iteTerm(b, x) + p = solver.mkVar(funSort2, "p") + with pytest.raises(RuntimeError): + p.iteTerm(b, b) + with pytest.raises(RuntimeError): + p.iteTerm(x, b) + zero = solver.mkInteger(0) + with pytest.raises(RuntimeError): + zero.iteTerm(x, x) + with pytest.raises(RuntimeError): + zero.iteTerm(x, b) + f_x = solver.mkTerm(kinds.ApplyUf, f, x) + with pytest.raises(RuntimeError): + f_x.iteTerm(b, b) + with pytest.raises(RuntimeError): + f_x.iteTerm(b, x) + sum = solver.mkTerm(kinds.Plus, f_x, f_x) + with pytest.raises(RuntimeError): + sum.iteTerm(x, x) + with pytest.raises(RuntimeError): + sum.iteTerm(b, x) + p_0 = solver.mkTerm(kinds.ApplyUf, p, zero) + p_0.iteTerm(b, b) + p_0.iteTerm(x, x) + with pytest.raises(RuntimeError): + p_0.iteTerm(x, b) + p_f_x = solver.mkTerm(kinds.ApplyUf, p, f_x) + p_f_x.iteTerm(b, b) + p_f_x.iteTerm(x, x) + with pytest.raises(RuntimeError): + p_f_x.iteTerm(x, b) + + +def test_term_assignment(solver): + t1 = solver.mkInteger(1) + t2 = t1 + t2 = solver.mkInteger(2) + assert t1 == solver.mkInteger(1) + + +def test_substitute(solver): + x = solver.mkConst(solver.getIntegerSort(), "x") + one = solver.mkInteger(1) + ttrue = solver.mkTrue() + xpx = solver.mkTerm(kinds.Plus, x, x) + onepone = solver.mkTerm(kinds.Plus, one, one) + + assert xpx.substitute(x, one) == onepone + assert onepone.substitute(one, x) == xpx + # incorrect due to type + with pytest.raises(RuntimeError): + xpx.substitute(one, ttrue) + + # simultaneous substitution + y = solver.mkConst(solver.getIntegerSort(), "y") + xpy = solver.mkTerm(kinds.Plus, x, y) + xpone = solver.mkTerm(kinds.Plus, y, one) + es = [] + rs = [] + es.append(x) + rs.append(y) + es.append(y) + rs.append(one) + assert xpy.substitute(es, rs) == xpone + + # incorrect substitution due to arity + rs.pop() + with pytest.raises(RuntimeError): + xpy.substitute(es, rs) + + # incorrect substitution due to types + rs.append(ttrue) + with pytest.raises(RuntimeError): + xpy.substitute(es, rs) + + # null cannot substitute + tnull = Term(solver) + with pytest.raises(RuntimeError): + tnull.substitute(one, x) + with pytest.raises(RuntimeError): + xpx.substitute(tnull, x) + with pytest.raises(RuntimeError): + xpx.substitute(x, tnull) + rs.pop() + rs.append(tnull) + with pytest.raises(RuntimeError): + xpy.substitute(es, rs) + es.clear() + rs.clear() + es.append(x) + rs.append(y) + with pytest.raises(RuntimeError): + tnull.substitute(es, rs) + es.append(tnull) + rs.append(one) + with pytest.raises(RuntimeError): + xpx.substitute(es, rs) + + +def test_term_compare(solver): + t1 = solver.mkInteger(1) + t2 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) + t3 = solver.mkTerm(kinds.Plus, solver.mkInteger(2), solver.mkInteger(2)) + assert t2 >= t3 + assert t2 <= t3 + assert (t1 > t2) != (t1 < t2) + assert (t1 > t2 or t1 == t2) == (t1 >= t2) + + +def test_term_children(solver): + # simple term 2+3 + two = solver.mkInteger(2) + t1 = solver.mkTerm(kinds.Plus, two, solver.mkInteger(3)) + assert t1[0] == two + assert t1.getNumChildren() == 2 + tnull = Term(solver) + with pytest.raises(RuntimeError): + tnull.getNumChildren() + + # apply term f(2) + intSort = solver.getIntegerSort() + fsort = solver.mkFunctionSort(intSort, intSort) + f = solver.mkConst(fsort, "f") + t2 = solver.mkTerm(kinds.ApplyUf, f, two) + # due to our higher-order view of terms, we treat f as a child of kinds.ApplyUf + assert t2.getNumChildren() == 2 + assert t2[0] == f + assert t2[1] == two + with pytest.raises(RuntimeError): + tnull[0] + + +def test_get_const_array_base(solver): + intsort = solver.getIntegerSort() + arrsort = solver.mkArraySort(intsort, intsort) + one = solver.mkInteger(1) + constarr = solver.mkConstArray(arrsort, one) + + assert constarr.isConstArray() + assert one == constarr.getConstArrayBase() + + +def test_get_abstract_value(solver): + v1 = solver.mkAbstractValue(1) + v2 = solver.mkAbstractValue("15") + v3 = solver.mkAbstractValue("18446744073709551617") + + assert v1.isAbstractValue() + assert v2.isAbstractValue() + assert v3.isAbstractValue() + assert "1" == v1.getAbstractValue() + assert "15" == v2.getAbstractValue() + assert "18446744073709551617" == v3.getAbstractValue() + + +def test_get_tuple(solver): + s1 = solver.getIntegerSort() + s2 = solver.getRealSort() + s3 = solver.getStringSort() + + t1 = solver.mkInteger(15) + t2 = solver.mkReal(17, 25) + t3 = solver.mkString("abc") + + tup = solver.mkTuple([s1, s2, s3], [t1, t2, t3]) + + assert tup.isTupleValue() + assert [t1, t2, t3] == tup.getTupleValue() + + +def test_get_set(solver): + s = solver.mkSetSort(solver.getIntegerSort()) + + i1 = solver.mkInteger(5) + i2 = solver.mkInteger(7) + + s1 = solver.mkEmptySet(s) + s2 = solver.mkTerm(kinds.SetSingleton, i1) + s3 = solver.mkTerm(kinds.SetSingleton, i1) + s4 = solver.mkTerm(kinds.SetSingleton, i2) + s5 = solver.mkTerm( + kinds.SetUnion, s2, solver.mkTerm(kinds.SetUnion, s3, s4)) + + assert s1.isSetValue() + assert s2.isSetValue() + assert s3.isSetValue() + assert s4.isSetValue() + assert not s5.isSetValue() + s5 = solver.simplify(s5) + assert s5.isSetValue() + + assert set([]) == s1.getSetValue() + assert set([i1]) == s2.getSetValue() + assert set([i1]) == s3.getSetValue() + assert set([i2]) == s4.getSetValue() + assert set([i1, i2]) == s5.getSetValue() + + +def test_get_sequence(solver): + s = solver.mkSequenceSort(solver.getIntegerSort()) + + i1 = solver.mkInteger(5) + i2 = solver.mkInteger(7) + + s1 = solver.mkEmptySequence(s) + s2 = solver.mkTerm(kinds.SeqUnit, i1) + s3 = solver.mkTerm(kinds.SeqUnit, i1) + s4 = solver.mkTerm(kinds.SeqUnit, i2) + s5 = solver.mkTerm(kinds.SeqConcat, s2, + solver.mkTerm(kinds.SeqConcat, s3, s4)) + + assert s1.isSequenceValue() + assert not s2.isSequenceValue() + assert not s3.isSequenceValue() + assert not s4.isSequenceValue() + assert not s5.isSequenceValue() + + s2 = solver.simplify(s2) + s3 = solver.simplify(s3) + s4 = solver.simplify(s4) + s5 = solver.simplify(s5) + + assert [] == s1.getSequenceValue() + assert [i1] == s2.getSequenceValue() + assert [i1] == s3.getSequenceValue() + assert [i2] == s4.getSequenceValue() + assert [i1, i1, i2] == s5.getSequenceValue() + + +def test_get_uninterpreted_const(solver): + s = solver.mkUninterpretedSort("test") + t1 = solver.mkUninterpretedConst(s, 3) + t2 = solver.mkUninterpretedConst(s, 5) + + assert t1.isUninterpretedValue() + assert t2.isUninterpretedValue() + + assert (s, 3) == t1.getUninterpretedValue() + assert (s, 5) == t2.getUninterpretedValue() + + +def test_get_floating_point(solver): + bvval = solver.mkBitVector(16, "0000110000000011", 2) + fp = solver.mkFloatingPoint(5, 11, bvval) + + assert fp.isFloatingPointValue() + assert not fp.isFloatingPointPosZero() + assert not fp.isFloatingPointNegZero() + assert not fp.isFloatingPointPosInf() + assert not fp.isFloatingPointNegInf() + assert not fp.isFloatingPointNaN() + assert (5, 11, bvval) == fp.getFloatingPointValue() + + assert solver.mkPosZero(5, 11).isFloatingPointPosZero() + assert solver.mkNegZero(5, 11).isFloatingPointNegZero() + assert solver.mkPosInf(5, 11).isFloatingPointPosInf() + assert solver.mkNegInf(5, 11).isFloatingPointNegInf() + assert solver.mkNaN(5, 11).isFloatingPointNaN() + + +def test_is_integer(solver): + int1 = solver.mkInteger("-18446744073709551616") + int2 = solver.mkInteger("-18446744073709551615") + int3 = solver.mkInteger("-4294967296") + int4 = solver.mkInteger("-4294967295") + int5 = solver.mkInteger("-10") + int6 = solver.mkInteger("0") + int7 = solver.mkInteger("10") + int8 = solver.mkInteger("4294967295") + int9 = solver.mkInteger("4294967296") + int10 = solver.mkInteger("18446744073709551615") + int11 = solver.mkInteger("18446744073709551616") + int12 = solver.mkInteger("-0") + + with pytest.raises(RuntimeError): + solver.mkInteger("") + with pytest.raises(RuntimeError): + solver.mkInteger("-") + with pytest.raises(RuntimeError): + solver.mkInteger("-1-") + with pytest.raises(RuntimeError): + solver.mkInteger("0.0") + with pytest.raises(RuntimeError): + solver.mkInteger("-0.1") + with pytest.raises(RuntimeError): + solver.mkInteger("012") + with pytest.raises(RuntimeError): + solver.mkInteger("0000") + with pytest.raises(RuntimeError): + solver.mkInteger("-01") + with pytest.raises(RuntimeError): + solver.mkInteger("-00") + + assert int1.isIntegerValue() + assert int2.isIntegerValue() + assert int3.isIntegerValue() + assert int4.isIntegerValue() + assert int5.isIntegerValue() + assert int6.isIntegerValue() + assert int7.isIntegerValue() + assert int8.isIntegerValue() + assert int9.isIntegerValue() + assert int10.isIntegerValue() + assert int11.isIntegerValue() + + assert int1.getIntegerValue() == -18446744073709551616 + assert int2.getIntegerValue() == -18446744073709551615 + assert int3.getIntegerValue() == -4294967296 + assert int4.getIntegerValue() == -4294967295 + assert int5.getIntegerValue() == -10 + assert int6.getIntegerValue() == 0 + assert int7.getIntegerValue() == 10 + assert int8.getIntegerValue() == 4294967295 + assert int9.getIntegerValue() == 4294967296 + assert int10.getIntegerValue() == 18446744073709551615 + assert int11.getIntegerValue() == 18446744073709551616 + + +def test_get_string(solver): + s1 = solver.mkString("abcde") + assert s1.isStringValue() + assert s1.getStringValue() == str("abcde") + + +def test_get_real(solver): + real1 = solver.mkReal("0") + real2 = solver.mkReal(".0") + real3 = solver.mkReal("-17") + real4 = solver.mkReal("-3/5") + real5 = solver.mkReal("12.7") + real6 = solver.mkReal("1/4294967297") + real7 = solver.mkReal("4294967297") + real8 = solver.mkReal("1/18446744073709551617") + real9 = solver.mkReal("18446744073709551617") + + assert real1.isRealValue() + assert real2.isRealValue() + assert real3.isRealValue() + assert real4.isRealValue() + assert real5.isRealValue() + assert real6.isRealValue() + assert real7.isRealValue() + assert real8.isRealValue() + assert real9.isRealValue() + + assert 0 == real1.getRealValue() + assert 0 == real2.getRealValue() + assert -17 == real3.getRealValue() + assert Fraction(-3, 5) == real4.getRealValue() + assert Fraction(127, 10) == real5.getRealValue() + assert Fraction(1, 4294967297) == real6.getRealValue() + assert 4294967297 == real7.getRealValue() + assert Fraction(1, 18446744073709551617) == real8.getRealValue() + assert Fraction(18446744073709551617, 1) == real9.getRealValue() + + # Check denominator too large for float + num = 1 + den = 2 ** 64 + 1 + real_big = solver.mkReal(num, den) + assert real_big.isRealValue() + assert Fraction(num, den) == real_big.getRealValue() + + # Check that we're treating floats as decimal aproximations rather than + # IEEE-754-specified values. + real_decimal = solver.mkReal(0.3) + assert real_decimal.isRealValue() + assert Fraction("0.3") == real_decimal.getRealValue() + assert Fraction(0.3) == Fraction(5404319552844595, 18014398509481984) + assert Fraction(0.3) != real_decimal.getRealValue() + + +def test_get_boolean(solver): + b1 = solver.mkBoolean(True) + b2 = solver.mkBoolean(False) + + assert b1.isBooleanValue() + assert b2.isBooleanValue() + assert b1.getBooleanValue() + assert not b2.getBooleanValue() + + +def test_get_bit_vector(solver): + b1 = solver.mkBitVector(8, 15) + b2 = solver.mkBitVector(8, "00001111", 2) + b3 = solver.mkBitVector(8, "15", 10) + b4 = solver.mkBitVector(8, "0f", 16) + b5 = solver.mkBitVector(9, "00001111", 2); + b6 = solver.mkBitVector(9, "15", 10); + b7 = solver.mkBitVector(9, "0f", 16); + + assert b1.isBitVectorValue() + assert b2.isBitVectorValue() + assert b3.isBitVectorValue() + assert b4.isBitVectorValue() + assert b5.isBitVectorValue() + assert b6.isBitVectorValue() + assert b7.isBitVectorValue() + + assert "00001111" == b1.getBitVectorValue(2) + assert "15" == b1.getBitVectorValue(10) + assert "f" == b1.getBitVectorValue(16) + assert "00001111" == b2.getBitVectorValue(2) + assert "15" == b2.getBitVectorValue(10) + assert "f" == b2.getBitVectorValue(16) + assert "00001111" == b3.getBitVectorValue(2) + assert "15" == b3.getBitVectorValue(10) + assert "f" == b3.getBitVectorValue(16) + assert "00001111" == b4.getBitVectorValue(2) + assert "15" == b4.getBitVectorValue(10) + assert "f" == b4.getBitVectorValue(16) + assert "000001111" == b5.getBitVectorValue(2) + assert "15" == b5.getBitVectorValue(10) + assert "f" == b5.getBitVectorValue(16) + assert "000001111" == b6.getBitVectorValue(2) + assert "15" == b6.getBitVectorValue(10) + assert "f" == b6.getBitVectorValue(16) + assert "000001111" == b7.getBitVectorValue(2) + assert "15" == b7.getBitVectorValue(10) + assert "f" == b7.getBitVectorValue(16) + + +def test_const_array(solver): + intsort = solver.getIntegerSort() + arrsort = solver.mkArraySort(intsort, intsort) + a = solver.mkConst(arrsort, "a") + one = solver.mkInteger(1) + constarr = solver.mkConstArray(arrsort, one) + + assert constarr.getKind() == kinds.ConstArray + assert constarr.getConstArrayBase() == one + with pytest.raises(RuntimeError): + a.getConstArrayBase() + + 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)) + + +def test_const_sequence_elements(solver): + realsort = solver.getRealSort() + seqsort = solver.mkSequenceSort(realsort) + s = solver.mkEmptySequence(seqsort) + + assert s.getKind() == kinds.ConstSequence + # empty sequence has zero elements + cs = s.getSequenceValue() + assert len(cs) == 0 + + # A seq.unit app is not a constant sequence (regardless of whether it is + # applied to a constant). + su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1)) + with pytest.raises(RuntimeError): + su.getSequenceValue() + + +def test_term_scoped_to_string(solver): + intsort = solver.getIntegerSort() + x = solver.mkConst(intsort, "x") + assert str(x) == "x" + solver2 = pycvc5.Solver() + assert str(x) == "x" 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..bb30fae8f --- /dev/null +++ b/test/unit/api/python/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() is True + assert f.toPythonObj() is 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() == Fraction("8.33") |