From 626a1634fc21aed6e1149e5579ce112c1efc72bc Mon Sep 17 00:00:00 2001 From: Ying Sheng Date: Tue, 18 May 2021 10:11:16 -0700 Subject: [PATCH] Adding python API test part 2 (#6551) This commit (follow #6546) adds more unit tests for python API. Subsequent commits will include additional missing functions and unit tests. --- test/python/unit/api/test_solver.py | 461 ++++++++++++++++++++++++++++ 1 file changed, 461 insertions(+) diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index 15e669f02..85594d530 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -423,3 +423,464 @@ def test_mk_pos_zero(solver): 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_empty(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpEmpty()) + + +def test_mk_regexp_sigma(solver): + strSort = solver.getStringSort() + s = solver.mkConst(strSort, "s") + solver.mkTerm(kinds.StringInRegexp, s, solver.mkRegexpSigma()) + + +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_true(solver): + solver.mkTrue() + solver.mkTrue() + + +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) + 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.defineFun("f", [], bvSort, v1) + solver.defineFun("ff", [b1, b2], bvSort, v1) + solver.defineFun(f1, [b1, b11], v1) + with pytest.raises(RuntimeError): + solver.defineFun("ff", [v1, b2], bvSort, v1) + with pytest.raises(RuntimeError): + solver.defineFun("fff", [b1], bvSort, v3) + with pytest.raises(RuntimeError): + solver.defineFun("ffff", [b1], funSort2, v3) + # b3 has function sort, which is allowed as an argument + solver.defineFun("fffff", [b1, b3], bvSort, v1) + with pytest.raises(RuntimeError): + solver.defineFun(f1, [v1, b11], v1) + with pytest.raises(RuntimeError): + solver.defineFun(f1, [b1], v1) + with pytest.raises(RuntimeError): + solver.defineFun(f1, [b1, b11], v2) + with pytest.raises(RuntimeError): + solver.defineFun(f1, [b1, b11], v3) + with pytest.raises(RuntimeError): + solver.defineFun(f2, [b1], v2) + with pytest.raises(RuntimeError): + solver.defineFun(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") + 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() -- 2.30.2