From 30f91833dea7f31156dafa401d17522b7fd87bc7 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Wed, 1 Dec 2021 01:38:44 +0200 Subject: [PATCH] Translating more cpp API unit tests to python (#7669) This translates the majority of the tests from https://github.com/cvc5/cvc5/blob/master/test/unit/api/cpp/solver_black.cpp that were not translated yet, to python. Additionally, some minor renames and `yapf` formatting is done the the existing tests. --- test/unit/api/python/test_solver.py | 406 ++++++++++++++++++++++++++-- 1 file changed, 381 insertions(+), 25 deletions(-) diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 4abfe0697..b6520e0d3 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -271,7 +271,7 @@ def test_mk_uninterpreted_sort(solver): solver.mkUninterpretedSort("") -def test_mk_sortConstructor_sort(solver): +def test_mk_sort_constructor_sort(solver): solver.mkSortConstructorSort("s", 2) solver.mkSortConstructorSort("", 2) with pytest.raises(RuntimeError): @@ -346,7 +346,8 @@ def test_mk_bit_vector(solver): with pytest.raises(RuntimeError): solver.mkBitVector(8, "fzff", 16) - assert solver.mkBitVector(8, "0101", 2) == solver.mkBitVector(8, "00000101", 2) + 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" @@ -422,6 +423,7 @@ def test_mk_floating_point(solver): with pytest.raises(RuntimeError): slv.mkFloatingPoint(3, 5, t1) + def test_mk_cardinality_constraint(solver): su = solver.mkUninterpretedSort("u") si = solver.getIntegerSort() @@ -434,6 +436,7 @@ def test_mk_cardinality_constraint(solver): with pytest.raises(RuntimeError): slv.mkCardinalityConstraint(su, 3) + def test_mk_empty_set(solver): slv = pycvc5.Solver() s = solver.mkSetSort(solver.getBooleanSort()) @@ -491,28 +494,23 @@ def test_mk_pos_zero(solver): 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 args) args = [1, 2, 2] solver.mkOp(kinds.TupleProject, args) @@ -662,7 +660,7 @@ def test_mk_regexp_allchar(solver): def test_mk_sep_emp(solver): - solver.mkSepEmp(); + solver.mkSepEmp() def test_mk_sep_nil(solver): @@ -752,7 +750,6 @@ def test_mk_term(solver): slv.mkTerm(kinds.Ite, solver.mkTrue(), solver.mkTrue(), solver.mkTrue()) - # mkTerm(Kind kind, const std::vector& children) const solver.mkTerm(kinds.Equal, v1) with pytest.raises(RuntimeError): solver.mkTerm(kinds.Equal, v2) @@ -887,7 +884,6 @@ def test_mk_term_from_op(solver): solver.mkTerm(opterm2, solver.mkInteger(1), solver.mkInteger(1), pycvc5.Term(solver)) - # mkTerm(Op op, const std::vector& children) const solver.mkTerm(opterm2, v4) with pytest.raises(RuntimeError): solver.mkTerm(opterm2, v1) @@ -905,7 +901,8 @@ def test_mk_true(solver): def test_mk_tuple(solver): - solver.mkTuple([solver.mkBitVectorSort(3)], [solver.mkBitVector(3, "101", 2)]) + solver.mkTuple([solver.mkBitVectorSort(3)], + [solver.mkBitVector(3, "101", 2)]) solver.mkTuple([solver.getRealSort()], [solver.mkInteger("5")]) with pytest.raises(RuntimeError): @@ -917,9 +914,11 @@ def test_mk_tuple(solver): 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)]) + slv.mkTuple([solver.mkBitVectorSort(3)], + [slv.mkBitVector(3, "101", 2)]) with pytest.raises(RuntimeError): - slv.mkTuple([slv.mkBitVectorSort(3)], [solver.mkBitVector(3, "101", 2)]) + slv.mkTuple([slv.mkBitVectorSort(3)], + [solver.mkBitVector(3, "101", 2)]) def test_mk_universe_set(solver): @@ -1309,7 +1308,7 @@ def test_get_value3(solver): slv.getValue(x) -def test_declare_separation_heap(solver): +def test_declare_sep_heap(solver): solver.setLogic("ALL") integer = solver.getIntegerSort() solver.declareSepHeap(integer, integer) @@ -1333,7 +1332,7 @@ def checkSimpleSeparationConstraints(slv): slv.checkSat() -def test_get_separation_heap_term1(solver): +def test_get_value_sep_heap_1(solver): solver.setLogic("QF_BV") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1343,7 +1342,7 @@ def test_get_separation_heap_term1(solver): solver.getValueSepHeap() -def test_get_separation_heap_term2(solver): +def test_get_value_sep_heap_2(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "false") @@ -1352,7 +1351,7 @@ def test_get_separation_heap_term2(solver): solver.getValueSepHeap() -def test_get_separation_heap_term3(solver): +def test_get_value_sep_heap_3(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1363,7 +1362,7 @@ def test_get_separation_heap_term3(solver): solver.getValueSepHeap() -def test_get_separation_heap_term4(solver): +def test_get_value_sep_heap_4(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1374,7 +1373,7 @@ def test_get_separation_heap_term4(solver): solver.getValueSepHeap() -def test_get_separation_heap_term5(solver): +def test_get_value_sep_heap_5(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1382,7 +1381,7 @@ def test_get_separation_heap_term5(solver): solver.getValueSepHeap() -def test_get_separation_nil_term1(solver): +def test_get_value_sep_nil_1(solver): solver.setLogic("QF_BV") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1392,7 +1391,7 @@ def test_get_separation_nil_term1(solver): solver.getValueSepNil() -def test_get_separation_nil_term2(solver): +def test_get_value_sep_nil_2(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "false") @@ -1401,7 +1400,7 @@ def test_get_separation_nil_term2(solver): solver.getValueSepNil() -def test_get_separation_nil_term3(solver): +def test_get_value_sep_nil_3(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1412,7 +1411,7 @@ def test_get_separation_nil_term3(solver): solver.getValueSepNil() -def test_get_separation_nil_term4(solver): +def test_get_value_sep_nil_4(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1423,7 +1422,7 @@ def test_get_separation_nil_term4(solver): solver.getValueSepNil() -def test_get_separation_nil_term5(solver): +def test_get_value_sep_nil_5(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") @@ -1466,7 +1465,7 @@ def test_pop3(solver): solver.pop(1) -def test_setInfo(solver): +def test_set_info(solver): with pytest.raises(RuntimeError): solver.setInfo("cvc5-lagic", "QF_BV") with pytest.raises(RuntimeError): @@ -1932,3 +1931,360 @@ def test_get_synth_solution(solver): slv = pycvc5.Solver() with pytest.raises(RuntimeError): slv.getSynthSolution(f) + + +def test_declare_pool(solver): + intSort = solver.getIntegerSort() + setSort = solver.mkSetSort(intSort) + zero = solver.mkInteger(0) + x = solver.mkConst(intSort, "x") + y = solver.mkConst(intSort, "y") + # declare a pool with initial value 0, x, y + p = solver.declarePool("p", intSort, [zero, x, y]) + # pool should have the same sort + assert p.getSort() == setSort + # cannot pass null sort + nullSort = pycvc5.Sort(solver) + with pytest.raises(RuntimeError): + solver.declarePool("i", nullSort, []) + + +def test_declare_sep_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) + + +def test_define_fun_global(solver): + bSort = solver.getBooleanSort() + + bTrue = solver.mkBoolean(True) + # (define-fun f () Bool true) + f = solver.defineFun("f", [], bSort, bTrue, True) + b = solver.mkVar(bSort, "b") + # (define-fun g (b Bool) Bool b) + g = solver.defineFun("g", [b], bSort, b, True) + + # (assert (or (not f) (not (g true)))) + solver.assertFormula( + solver.mkTerm(kinds.Or, f.notTerm(), + solver.mkTerm(kinds.ApplyUf, g, bTrue).notTerm())) + assert solver.checkSat().isUnsat() + solver.resetAssertions() + # (assert (or (not f) (not (g true)))) + solver.assertFormula( + solver.mkTerm(kinds.Or, f.notTerm(), + solver.mkTerm(kinds.ApplyUf, g, bTrue).notTerm())) + assert solver.checkSat().isUnsat() + + +def test_define_sort(solver): + sortVar0 = solver.mkParamSort("T0") + sortVar1 = solver.mkParamSort("T1") + intSort = solver.getIntegerSort() + realSort = solver.getRealSort() + arraySort0 = solver.mkArraySort(sortVar0, sortVar0) + arraySort1 = solver.mkArraySort(sortVar0, sortVar1) + # Now create instantiations of the defined sorts + arraySort0.substitute(sortVar0, intSort) + + arraySort1.substitute([sortVar0, sortVar1], [intSort, realSort]) + + +def test_get_model_domain_elements(solver): + solver.setOption("produce-models", "true") + uSort = solver.mkUninterpretedSort("u") + intSort = solver.getIntegerSort() + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + z = solver.mkConst(uSort, "z") + f = solver.mkTerm(kinds.Distinct, x, y, z) + solver.assertFormula(f) + solver.checkSat() + solver.getModelDomainElements(uSort) + assert len(solver.getModelDomainElements(uSort)) >= 3 + with pytest.raises(RuntimeError): + solver.getModelDomainElements(intSort) + + +def test_get_synth_solutions(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.getSynthSolutions([]) + with pytest.raises(RuntimeError): + solver.getSynthSolutions([f]) + + solver.checkSynth() + + solver.getSynthSolutions([f]) + solver.getSynthSolutions([f, f]) + + with pytest.raises(RuntimeError): + solver.getSynthSolutions([]) + with pytest.raises(RuntimeError): + solver.getSynthSolutions([nullTerm]) + with pytest.raises(RuntimeError): + solver.getSynthSolutions([x]) + + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.getSynthSolutions([x]) + + +def test_get_value_sep_heap1(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_value_sep_heap2(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "false") + checkSimpleSeparationConstraints(solver) + with pytest.raises(RuntimeError): + solver.getValueSepHeap() + + +def test_get_value_sep_heap3(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_value_sep_heap4(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_value_sep_heap5(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + checkSimpleSeparationConstraints(solver) + solver.getValueSepHeap() + + +def test_get_value_sep_nil1(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_value_sep_nil2(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "false") + checkSimpleSeparationConstraints(solver) + with pytest.raises(RuntimeError): + solver.getValueSepNil() + + +def test_get_value_sep_nil3(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_value_sep_nil4(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_value_sep_nil5(solver): + solver.setLogic("ALL") + solver.setOption("incremental", "false") + solver.setOption("produce-models", "true") + checkSimpleSeparationConstraints(solver) + solver.getValueSepNil() + + +def test_is_model_core_symbol(solver): + solver.setOption("produce-models", "true") + solver.setOption("model-cores", "simple") + uSort = solver.mkUninterpretedSort("u") + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + z = solver.mkConst(uSort, "z") + zero = solver.mkInteger(0) + f = solver.mkTerm(kinds.Not, solver.mkTerm(kinds.Equal, x, y)) + solver.assertFormula(f) + solver.checkSat() + assert solver.isModelCoreSymbol(x) + assert solver.isModelCoreSymbol(y) + assert not solver.isModelCoreSymbol(z) + with pytest.raises(RuntimeError): + solver.isModelCoreSymbol(zero) + + +def test_issue5893(solver): + slv = pycvc5.Solver() + bvsort4 = solver.mkBitVectorSort(4) + bvsort8 = solver.mkBitVectorSort(8) + arrsort = solver.mkArraySort(bvsort4, bvsort8) + arr = solver.mkConst(arrsort, "arr") + idx = solver.mkConst(bvsort4, "idx") + ten = solver.mkBitVector(8, "10", 10) + sel = solver.mkTerm(kinds.Select, arr, idx) + distinct = solver.mkTerm(kinds.Distinct, sel, ten) + distinct.getOp() + + +def test_issue7000(solver): + s1 = solver.getIntegerSort() + s2 = solver.mkFunctionSort(s1, s1) + s3 = solver.getRealSort() + t4 = solver.mkPi() + t7 = solver.mkConst(s3, "_x5") + t37 = solver.mkConst(s2, "_x32") + t59 = solver.mkConst(s2, "_x51") + t72 = solver.mkTerm(kinds.Equal, t37, t59) + t74 = solver.mkTerm(kinds.Gt, t4, t7) + # throws logic exception since logic is not higher order by default + with pytest.raises(RuntimeError): + solver.checkEntailed(t72, t74, t72, t72) + + +def test_mk_sygus_var(solver): + boolSort = solver.getBooleanSort() + intSort = solver.getIntegerSort() + funSort = solver.mkFunctionSort(intSort, boolSort) + + solver.mkSygusVar(boolSort) + solver.mkSygusVar(funSort) + solver.mkSygusVar(boolSort, "b") + solver.mkSygusVar(funSort, "") + with pytest.raises(RuntimeError): + solver.mkSygusVar(pycvc5.Sort(solver)) + with pytest.raises(RuntimeError): + solver.mkSygusVar(solver.getNullSort(), "a") + slv = pycvc5.Solver() + with pytest.raises(RuntimeError): + slv.mkSygusVar(boolSort) + + +def test_synth_fun(solver): + null = solver.getNullSort() + 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.synthFun("", [], boolean) + solver.synthFun("f1", [x], boolean) + solver.synthFun("f2", [x], boolean, g1) + + with pytest.raises(RuntimeError): + solver.synthFun("f3", [nullTerm], boolean) + with pytest.raises(RuntimeError): + solver.synthFun("f4", [], null) + with pytest.raises(RuntimeError): + solver.synthFun("f6", [x], boolean, g2) + slv = pycvc5.Solver() + x2 = slv.mkVar(slv.getBooleanSort()) + slv.synthFun("f1", [x2], slv.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.synthFun("", [], solver.getBooleanSort()) + with pytest.raises(RuntimeError): + slv.synthFun("f1", [x], solver.getBooleanSort()) + + +def test_tuple_project(solver): + sorts = [solver.getBooleanSort(),\ + solver.getIntegerSort(),\ + solver.getStringSort(),\ + solver.mkSetSort(solver.getStringSort())] + elements = [\ + solver.mkBoolean(True), \ + solver.mkInteger(3),\ + solver.mkString("C"),\ + solver.mkTerm(kinds.SetSingleton, solver.mkString("Z"))] + + tuple = solver.mkTuple(sorts, elements) + + indices1 = [] + indices2 = [0] + indices3 = [0, 1] + indices4 = [0, 0, 2, 2, 3, 3, 0] + indices5 = [4] + indices6 = [0, 4] + + solver.mkTerm(solver.mkOp(kinds.TupleProject, indices1), tuple) + + solver.mkTerm(solver.mkOp(kinds.TupleProject, indices2), tuple) + + solver.mkTerm(solver.mkOp(kinds.TupleProject, indices3), tuple) + + solver.mkTerm(solver.mkOp(kinds.TupleProject, indices4), tuple) + + with pytest.raises(RuntimeError): + solver.mkTerm(solver.mkOp(kinds.TupleProject, indices5), tuple) + with pytest.raises(RuntimeError): + solver.mkTerm(solver.mkOp(kinds.TupleProject, indices6), tuple) + + indices = [0, 3, 2, 0, 1, 2] + + op = solver.mkOp(kinds.TupleProject, indices) + projection = solver.mkTerm(op, tuple) + + datatype = tuple.getSort().getDatatype() + constructor = datatype[0] + + for i in indices: + + selectorTerm = constructor[i].getSelectorTerm() + selectedTerm = solver.mkTerm(kinds.ApplySelector, selectorTerm, tuple) + simplifiedTerm = solver.simplify(selectedTerm) + assert elements[i] == simplifiedTerm + + assert "((_ tuple_project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton \"Z\")))" == str( + projection) -- 2.30.2