diff options
-rw-r--r-- | test/api/python/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/api/python/test_grammar.py | 130 | ||||
-rw-r--r-- | test/python/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/python/unit/api/test_grammar.py | 137 | ||||
-rw-r--r-- | test/python/unit/api/test_solver.py | 398 |
5 files changed, 530 insertions, 137 deletions
diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index 87ddbb5d6..7f05bf130 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -39,5 +39,4 @@ macro(cvc5_add_python_api_test name filename) endmacro() cvc5_add_python_api_test(pytest_datatype_api test_datatype_api.py) -cvc5_add_python_api_test(pytest_grammar test_grammar.py) cvc5_add_python_api_test(pytest_to_python_obj test_to_python_obj.py) diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py deleted file mode 100644 index f83bee548..000000000 --- a/test/api/python/test_grammar.py +++ /dev/null @@ -1,130 +0,0 @@ -############################################################################### -# 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 - -def test_add_rule(): - solver = pycvc5.Solver() - boolean = solver.getBooleanSort() - integer = solver.getIntegerSort() - - nullTerm = pycvc5.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(Exception): - g.addRule(nullTerm, solver.mkBoolean(false)) - with pytest.raises(Exception): - g.addRule(start, nullTerm) - with pytest.raises(Exception): - g.addRule(nts, solver.mkBoolean(false)) - with pytest.raises(Exception): - g.addRule(start, solver.mkInteger(0)) - - # expecting no errors - solver.synthFun("f", {}, boolean, g) - - # expecting an error - with pytest.raises(Exception): - g.addRule(start, solver.mkBoolean(false)) - -def test_add_rules(): - solver = pycvc5.Solver() - boolean = solver.getBooleanSort() - integer = solver.getIntegerSort() - - nullTerm = pycvc5.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(Exception): - g.addRules(nullTerm, solver.mkBoolean(False)) - with pytest.raises(Exception): - g.addRules(start, {nullTerm}) - with pytest.raises(Exception): - g.addRules(nts, {solver.mkBoolean(False)}) - with pytest.raises(Exception): - g.addRules(start, {solver.mkInteger(0)}) - #Expecting no errors - solver.synthFun("f", {}, boolean, g) - - #Expecting an error - with pytest.raises(Exception): - g.addRules(start, solver.mkBoolean(False)) - -def testAddAnyConstant(): - solver = pycvc5.Solver() - boolean = solver.getBooleanSort() - - nullTerm = pycvc5.Term(solver) - start = solver.mkVar(boolean) - nts = solver.mkVar(boolean) - - g = solver.mkSygusGrammar({}, {start}) - - g.addAnyConstant(start) - g.addAnyConstant(start) - - with pytest.raises(Exception): - g.addAnyConstant(nullTerm) - with pytest.raises(Exception): - g.addAnyConstant(nts) - - solver.synthFun("f", {}, boolean, g) - - with pytest.raises(Exception): - g.addAnyConstant(start) - - -def testAddAnyVariable(): - solver = pycvc5.Solver() - boolean = solver.getBooleanSort() - - nullTerm = pycvc5.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(Exception): - g1.addAnyVariable(nullTerm) - with pytest.raises(Exception): - g1.addAnyVariable(nts) - - solver.synthFun("f", {}, boolean, g1) - - with pytest.raises(Exception): - g1.addAnyVariable(start) - diff --git a/test/python/CMakeLists.txt b/test/python/CMakeLists.txt index b7de1cbb0..6091e3275 100644 --- a/test/python/CMakeLists.txt +++ b/test/python/CMakeLists.txt @@ -30,3 +30,4 @@ endmacro() cvc5_add_python_api_test(pytest_solver unit/api/test_solver.py) cvc5_add_python_api_test(pytest_sort unit/api/test_sort.py) cvc5_add_python_api_test(pytest_term unit/api/test_term.py) +cvc5_add_python_api_test(pytest_grammar unit/api/test_grammar.py) diff --git a/test/python/unit/api/test_grammar.py b/test/python/unit/api/test_grammar.py new file mode 100644 index 000000000..db567a6ba --- /dev/null +++ b/test/python/unit/api/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/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 74eda63bc..15e669f02 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -1,6 +1,6 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Ying Sheng # # This file is part of the cvc5 project. # @@ -17,10 +17,12 @@ 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") @@ -28,12 +30,396 @@ def test_recoverable_exception(solver): with pytest.raises(RuntimeError): c = solver.getValue(x) + def test_supports_floating_point(solver): if solver.supportsFloatingPoint(): - try: - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) - except RuntimeError: - pytest.fail() + solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + else: + with pytest.raises(RuntimeError): + solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + + +def test_get_boolean_sort(solver): + solver.getBooleanSort() + + +def test_get_integer_sort(solver): + solver.getIntegerSort() + + +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): + if solver.supportsFloatingPoint(): + solver.getRoundingModeSort() + else: + with pytest.raises(RuntimeError): + 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) + + if (solver.supportsFloatingPoint()): + 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): + if solver.supportsFloatingPoint(): + solver.mkFloatingPointSort(4, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(0, 8) + with pytest.raises(RuntimeError): + solver.mkFloatingPointSort(4, 0) else: with pytest.raises(RuntimeError): - solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven) + solver.mkFloatingPointSort(4, 8) + + +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, []) + + with pytest.raises(RuntimeError): + slv.mkDatatypeSorts(decls, []) + + throwsDtypeSpec = solver.mkDatatypeDecl("list") + throwsDecls = [throwsDtypeSpec] + with pytest.raises(RuntimeError): + solver.mkDatatypeSorts(throwsDecls, []) + + # with unresolved sorts + unresList = solver.mkUninterpretedSort("ulist") + unresSorts = [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_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_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): + if solver.supportsFloatingPoint(): + solver.mkRoundingMode(pycvc5.RoundTowardZero) + else: + with pytest.raises(RuntimeError): + solver.mkRoundingMode(pycvc5.RoundTowardZero) + + +def test_mk_uninterpreted_const(solver): + solver.mkUninterpretedConst(solver.getBooleanSort(), 1) + with pytest.raises(RuntimeError): + solver.mkUninterpretedConst(pycvc5.Sort(solver), 1) + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkUninterpretedConst(solver.getBooleanSort(), 1) + + +def test_mk_floating_point(solver): + t1 = solver.mkBitVector(8) + t2 = solver.mkBitVector(4) + t3 = solver.mkInteger(2) + if (solver.supportsFloatingPoint()): + solver.mkFloatingPoint(3, 5, t1) + else: + with pytest.raises(RuntimeError): + 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) + + if (solver.supportsFloatingPoint()): + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkFloatingPoint(3, 5, t1) + + +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_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): + if (solver.supportsFloatingPoint()): + solver.mkNaN(3, 5) + else: + with pytest.raises(RuntimeError): + solver.mkNaN(3, 5) + + +def test_mk_neg_zero(solver): + if (solver.supportsFloatingPoint()): + solver.mkNegZero(3, 5) + else: + with pytest.raises(RuntimeError): + solver.mkNegZero(3, 5) + + +def test_mk_neg_inf(solver): + if (solver.supportsFloatingPoint()): + solver.mkNegInf(3, 5) + else: + with pytest.raises(RuntimeError): + solver.mkNegInf(3, 5) + + +def test_mk_pos_inf(solver): + if (solver.supportsFloatingPoint()): + solver.mkPosInf(3, 5) + else: + with pytest.raises(RuntimeError): + solver.mkPosInf(3, 5) + + +def test_mk_pos_zero(solver): + if (solver.supportsFloatingPoint()): + solver.mkPosZero(3, 5) + else: + with pytest.raises(RuntimeError): + solver.mkPosZero(3, 5) + + +def test_mk_pi(solver): + solver.mkPi() |