############################################################################### # Top contributors (to current version): # Aina Niemetz, Ying Sheng, Yoni Zohar # # This file is part of the cvc5 project. # # Copyright (c) 2009-2025 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 cvc5 import sys from math import isnan from cvc5 import Kind, OptionCategory, SortKind, TermManager, Solver, Plugin from cvc5 import RoundingMode from cvc5 import BlockModelsMode, LearnedLitType, FindSynthTarget from cvc5 import ProofComponent, ProofFormat @pytest.fixture def tm(): return TermManager() @pytest.fixture def solver(tm): return Solver(tm) def test_recoverable_exception(tm, solver): solver.setOption("produce-models", "true") x = tm.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x).notTerm()) with pytest.raises(RuntimeError): c = solver.getValue(x) def test_declare_fun_fresh(tm, solver): boolSort = tm.getBooleanSort() intSort = tm.getIntegerSort() t1 = solver.declareFun("b", [], boolSort, True) t2 = solver.declareFun("b", [], boolSort, False) t3 = solver.declareFun("b", [], boolSort, False) assert not t1 == t2 assert not t1 == t3 assert t2 == t3 t4 = solver.declareFun("c", [], boolSort, False) assert not t2 == t4 t5 = solver.declareFun("b", [], intSort, False) assert not t2 == t5 ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): slv.declareFun("b", [], intSort, False) def test_declare_fun(tm, solver): bvSort = tm.mkBitVectorSort(32) funSort = tm.mkFunctionSort(tm.mkUninterpretedSort("u"),\ tm.getIntegerSort()) solver.declareFun("f1", [], bvSort) solver.declareFun("f3", [bvSort, tm.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 = Solver(tm) slv.declareFun("f1", [], bvSort) ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): slv.declareFun("f1", [], bvSort) def decalre_datatype(tm, solver): lin = tm.mkDatatypeConstructorDecl("lin") solver.declareDatatype("", [lin]) nil = tm.mkDatatypeConstructorDecl("nil") solver.declareDatatype("a", [nil]) cons = tm.mkDatatypeConstructorDecl("cons") nil2 = tm.mkDatatypeConstructorDecl("nil") solver.declareDatatype("b", [cons, nil2]) cons2 = tm.mkDatatypeConstructorDecl("cons") nil3 = tm.mkDatatypeConstructorDecl("nil") solver.declareDatatype("", [cons2, nil3]) # must have at least one constructor with pytest.raises(RuntimeError): solver.declareDatatype("c", []) # constructors may not be reused ctor1 = tm.mkDatatypeConstructorDecl("_x21") ctor2 = tm.mkDatatypeConstructorDecl("_x31") s3 = solver.declareDatatype("_x17", [ctor1, ctor2]) with pytest.raises(RuntimeError): solver.declareDatatype("_x86", [ctor1, ctor2]) ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): nnil = tm.mkDatatypeConstructorDecl("nil") slv.declareDatatype("a", [nnil]) def test_declare_sort(solver): solver.declareSort("s", 0) solver.declareSort("s", 2) solver.declareSort("", 2) def test_declare_sort_fresh(solver): t1 = solver.declareSort("b", 0, True) t2 = solver.declareSort("b", 0, False) t3 = solver.declareSort("b", 0, False) assert t1!=t2 assert t1!=t3 assert t2==t3 t4 = solver.declareSort("c", 0, False) assert t2!=t4 t5 = solver.declareSort("b", 1, False) assert t2!=t5 def test_define_fun(tm, solver): bvSort = tm.mkBitVectorSort(32) funSort = tm.mkFunctionSort(tm.mkUninterpretedSort("u"), tm.getIntegerSort()) b1 = tm.mkVar(bvSort, "b1") b2 = tm.mkVar(tm.getIntegerSort(), "b2") b3 = tm.mkVar(funSort, "b3") v1 = tm.mkConst(bvSort, "v1") v2 = tm.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) ttm = TermManager() slv = Solver(ttm) bvSort2 = ttm.mkBitVectorSort(32) v12 = ttm.mkConst(bvSort2, "v1") b12 = ttm.mkVar(bvSort2, "b1") b22 = ttm.mkVar(ttm.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_global(tm, solver): bSort = solver.getBooleanSort() bTrue = tm.mkBoolean(True) # (define-fun f () Bool true) f = solver.defineFun("f", [], bSort, bTrue, True) b = tm.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( tm.mkTerm(Kind.OR, f.notTerm(), tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() solver.resetAssertions() # (assert (or (not f) (not (g true)))) solver.assertFormula( tm.mkTerm(Kind.OR, f.notTerm(), tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): slv.defineFun("f", [], bSort, bTrue, True) def test_define_fun_rec(tm, solver): bvSort = tm.mkBitVectorSort(32) funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort) funSort2 = tm.mkFunctionSort( tm.mkUninterpretedSort("u"), tm.getIntegerSort()) b1 = tm.mkVar(bvSort, "b1") b11 = tm.mkVar(bvSort, "b1") b2 = tm.mkVar(tm.getIntegerSort(), "b2") b3 = tm.mkVar(funSort2, "b3") v1 = tm.mkConst(bvSort, "v1") v2 = tm.mkConst(tm.getIntegerSort(), "v2") v3 = tm.mkConst(funSort2, "v3") f1 = tm.mkConst(funSort1, "f1") f2 = tm.mkConst(funSort2, "f2") f3 = tm.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) ttm = TermManager() slv = Solver(ttm) bvSort2 = ttm.mkBitVectorSort(32) v12 = ttm.mkConst(bvSort2, "v1") b12 = ttm.mkVar(bvSort2, "b1") b22 = ttm.mkVar(ttm.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(tm, solver): solver.setLogic("QF_BV") bvSort = tm.mkBitVectorSort(32) funSort = tm.mkFunctionSort([bvSort, bvSort], bvSort) b = tm.mkVar(bvSort, "b") v = tm.mkConst(bvSort, "v") f = tm.mkConst(funSort, "f") with pytest.raises(RuntimeError): solver.defineFunRec("f", [], bvSort, v) with pytest.raises(RuntimeError): solver.defineFunRec(f, [b, b], v) def test_define_fun_rec_global(tm, solver): bSort = tm.getBooleanSort() fSort = tm.mkFunctionSort([bSort], bSort) solver.push() bTrue = tm.mkBoolean(True) # (define-fun f () Bool true) f = solver.defineFunRec("f", [], bSort, bTrue, True) b = tm.mkVar(bSort, "b") gSym = tm.mkConst(fSort, "g") # (define-fun g (b Bool) Bool b) g = solver.defineFunRec(gSym, [b], b, glbl=True) # (assert (or (not f) (not (g true)))) solver.assertFormula(tm.mkTerm( Kind.OR, f.notTerm(), tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() solver.pop() # (assert (or (not f) (not (g true)))) solver.assertFormula(tm.mkTerm( Kind.OR, f.notTerm(), tm.mkTerm(Kind.APPLY_UF, g, bTrue).notTerm())) assert solver.checkSat().isUnsat() ttm = TermManager() slv = Solver(ttm) bb = ttm.mkVar(ttm.getBooleanSort(), "b") with pytest.raises(RuntimeError): slv.defineFunRec( tm.mkConst( tm.mkFunctionSort({tm.getBooleanSort()}, tm.getBooleanSort()), "g"), [bb], bb, True) with pytest.raises(RuntimeError): slv.defineFunRec( ttm.mkConst( ttm.mkFunctionSort({ttm.getBooleanSort()}, ttm.getBooleanSort()), "g"), [b], b, True) def test_define_funs_rec(tm, solver): uSort = tm.mkUninterpretedSort("u") bvSort = tm.mkBitVectorSort(32) funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort) funSort2 = tm.mkFunctionSort([uSort], tm.getIntegerSort()) b1 = tm.mkVar(bvSort, "b1") b11 = tm.mkVar(bvSort, "b1") b2 = tm.mkVar(tm.getIntegerSort(), "b2") b3 = tm.mkVar(funSort2, "b3") b4 = tm.mkVar(uSort, "b4") v1 = tm.mkConst(bvSort, "v1") v2 = tm.mkConst(tm.getIntegerSort(), "v2") v3 = tm.mkConst(funSort2, "v3") v4 = tm.mkConst(uSort, "v4") f1 = tm.mkConst(funSort1, "f1") f2 = tm.mkConst(funSort2, "f2") f3 = tm.mkConst(bvSort, "f3") solver.defineFunsRec([f1, f2], [[b1, b11], [b4]], [v1, v2]) with pytest.raises(RuntimeError): solver.defineFunsRec([f1, f2], [[v1, b11], [b4]], [v1, v2]) with pytest.raises(RuntimeError): solver.defineFunsRec([f1, f3], [[b1, b11], [b4]], [v1, v2]) with pytest.raises(RuntimeError): solver.defineFunsRec([f1, f2], [[b1], [b4]], [v1, v2]) with pytest.raises(RuntimeError): solver.defineFunsRec([f1, f2], [[b1, b2], [b4]], [v1, v2]) with pytest.raises(RuntimeError): solver.defineFunsRec([f1, f2], [[b1, b11], [b4]], [v1, v4]) ttm = TermManager() slv = Solver(ttm) bb = ttm.mkVar(ttm.getBooleanSort(), "b") uSort2 = ttm.mkUninterpretedSort("u") bvSort2 = ttm.mkBitVectorSort(32) funSort12 = ttm.mkFunctionSort([bvSort2, bvSort2], bvSort2) funSort22 = ttm.mkFunctionSort([uSort2], ttm.getIntegerSort()) b12 = ttm.mkVar(bvSort2, "b1") b112 = ttm.mkVar(bvSort2, "b1") b42 = ttm.mkVar(uSort2, "b4") v12 = ttm.mkConst(bvSort2, "v1") v22 = ttm.mkConst(ttm.getIntegerSort(), "v2") f12 = ttm.mkConst(funSort12, "f1") f22 = ttm.mkConst(funSort22, "f2") slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v12, v22]) with pytest.raises(RuntimeError): slv.defineFunsRec([f1, f22], [[b12, b112], [b42]], [v12, v22]) with pytest.raises(RuntimeError): slv.defineFunsRec([f12, f22], [[b1, b112], [b42]], [v12, v22]) with pytest.raises(RuntimeError): slv.defineFunsRec([f12, f22], [[b12, b11], [b42]], [v12, v22]) with pytest.raises(RuntimeError): slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v1, v22]) with pytest.raises(RuntimeError): slv.defineFunsRec([f12, f22], [[b12, b112], [b42]], [v12, v2]) with pytest.raises(RuntimeError): slv.defineFunsRec([f12, f2], [[b12, b112], [b42]], [v12, v22]) with pytest.raises(RuntimeError): slv.defineFunsRec([f12, f22], [[b12, b112], [b4]], [v12, v22]) def test_define_funs_rec_wrong_logic(tm, solver): solver.setLogic("QF_BV") uSort = tm.mkUninterpretedSort("u") bvSort = tm.mkBitVectorSort(32) funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort) funSort2 = tm.mkFunctionSort([uSort], tm.getIntegerSort()) b = tm.mkVar(bvSort, "b") u = tm.mkVar(uSort, "u") v1 = tm.mkConst(bvSort, "v1") v2 = tm.mkConst(tm.getIntegerSort(), "v2") f1 = tm.mkConst(funSort1, "f1") f2 = tm.mkConst(funSort2, "f2") with pytest.raises(RuntimeError): solver.defineFunsRec([f1, f2], [[b, b], [u]], [v1, v2]) def test_define_funs_rec_global(tm, solver): bSort = tm.getBooleanSort() fSort = tm.mkFunctionSort([bSort], bSort) solver.push() bTrue = tm.mkBoolean(True) b = tm.mkVar(bSort, "b") gSym = tm.mkConst(fSort, "g") # (define-funs-rec ((g ((b Bool)) Bool)) (b)) solver.defineFunsRec([gSym], [[b]], [b], True) # (assert (not (g true))) solver.assertFormula(tm.mkTerm(Kind.APPLY_UF, gSym, bTrue).notTerm()) assert solver.checkSat().isUnsat() solver.pop() # (assert (not (g true))) solver.assertFormula(tm.mkTerm(Kind.APPLY_UF, gSym, bTrue).notTerm()) assert solver.checkSat().isUnsat() def test_get_assertions(tm, solver): a = tm.mkConst(tm.getBooleanSort(), 'a') b = tm.mkConst(tm.getBooleanSort(), 'b') solver.assertFormula(a) solver.assertFormula(b) asserts = [a,b] assert solver.getAssertions() == asserts def test_get_info(solver): solver.getInfo("name") with pytest.raises(RuntimeError): solver.getInfo("asdf") def test_get_option(solver): solver.setOption("incremental", "true") assert solver.getOption("incremental") == "true" with pytest.raises(RuntimeError): solver.getOption("asdf") def test_get_option_names(solver): opts = solver.getOptionNames() assert len(opts) > 100 assert "verbose" in opts assert "foobar" not in opts def test_get_option_info(solver): with pytest.raises(RuntimeError): solver.getOptionInfo("asdf-invalid") info = solver.getOptionInfo("verbose") assert info['name'] == "verbose" assert info['category'] == OptionCategory.COMMON assert info['aliases'] == [] assert not info['setByUser'] assert info['type'] is None info = solver.getOptionInfo("print-success") assert info['name'] == "print-success" assert info['category'] == OptionCategory.COMMON assert info['aliases'] == [] assert not info['setByUser'] assert info['type'] is bool assert info['current'] == False assert info['default'] == False info = solver.getOptionInfo("verbosity") assert info['name'] == "verbosity" assert info['category'] == OptionCategory.COMMON assert info['aliases'] == [] assert not info['setByUser'] assert info['type'] is int assert info['current'] == 0 assert info['default'] == 0 assert info['minimum'] is None and info['maximum'] is None info = solver.getOptionInfo("rlimit") assert info['name'] == "rlimit" assert info['category'] == OptionCategory.COMMON assert info['aliases'] == [] assert not info['setByUser'] assert info['type'] is int assert info['current'] == 0 assert info['default'] == 0 assert info['minimum'] is None and info['maximum'] is None info = solver.getOptionInfo("random-freq") assert info['name'] == "random-freq" assert info['category'] == OptionCategory.EXPERT assert info['aliases'] == ["random-frequency"] assert not info['setByUser'] assert info['type'] is float assert info['current'] == 0.0 assert info['default'] == 0.0 assert info['minimum'] == 0.0 and info['maximum'] == 1.0 info = solver.getOptionInfo("force-logic") assert info['name'] == "force-logic" assert info['category'] == OptionCategory.COMMON assert info['aliases'] == [] assert not info['setByUser'] assert info['type'] is str assert info['current'] == "" assert info['default'] == "" info = solver.getOptionInfo("simplification") assert info['name'] == "simplification" assert info['category'] == OptionCategory.REGULAR assert info['aliases'] == ["simplification-mode"] assert not info['setByUser'] assert info['type'] == 'mode' assert info['current'] == 'batch' assert info['default'] == 'batch' assert info['modes'] == ['batch', 'none'] 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_core_and_proof(tm, solver): solver.setOption("incremental", "true") solver.setOption("produce-unsat-cores", "true") solver.setOption("produce-proofs", "true"); uSort = solver.mkUninterpretedSort("u") intSort = tm.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(Kind.APPLY_UF, f, x) f_y = solver.mkTerm(Kind.APPLY_UF, f, y) summ = solver.mkTerm(Kind.ADD, f_x, f_y) p_0 = solver.mkTerm(Kind.APPLY_UF, p, zero) p_f_y = solver.mkTerm(Kind.APPLY_UF, p, f_y) solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_x)) solver.assertFormula(solver.mkTerm(Kind.GT, zero, f_y)) solver.assertFormula(solver.mkTerm(Kind.GT, summ, one)) solver.assertFormula(p_0) solver.assertFormula(p_f_y.notTerm()) assert solver.checkSat().isUnsat() unsat_core = solver.getUnsatCore() solver.getProof() solver.getProof(ProofComponent.SAT) solver.resetAssertions() for t in unsat_core: solver.assertFormula(t) res = solver.checkSat() assert res.isUnsat() solver.getProof() def test_get_unsat_core_and_proof_to_string(tm, solver): solver.setOption("produce-proofs", "true") uSort = tm.mkUninterpretedSort("u") intSort = tm.getIntegerSort() boolSort = tm.getBooleanSort() uToIntSort = tm.mkFunctionSort(uSort, intSort) intPredSort = tm.mkFunctionSort(intSort, boolSort) x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") f = tm.mkConst(uToIntSort, "f") p = tm.mkConst(intPredSort, "p") zero = tm.mkInteger(0) one = tm.mkInteger(1) f_x = tm.mkTerm(Kind.APPLY_UF, f, x) f_y = tm.mkTerm(Kind.APPLY_UF, f, y) summ = tm.mkTerm(Kind.ADD, f_x, f_y) p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero) p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y) solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_x)) solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_y)) solver.assertFormula(tm.mkTerm(Kind.GT, summ, one)) solver.assertFormula(p_0) solver.assertFormula(p_f_y.notTerm()) assert solver.checkSat().isUnsat() proofs = solver.getProof() assert len(proofs) > 0 printedProof = solver.proofToString(proofs[0]) assert len(printedProof) > 0 printedProof = solver.proofToString(proofs[0], ProofFormat.ALETHE) assert len(printedProof) > 0 proofs = solver.getProof(ProofComponent.SAT) printedProof = solver.proofToString(proofs[0], ProofFormat.NONE) assert len(printedProof) > 0 def test_proof_to_string_assertion_names(tm, solver): solver.setOption("produce-proofs", "true") uSort = tm.mkUninterpretedSort("u") x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") x_eq_y = tm.mkTerm(Kind.EQUAL, x, y) not_x_eq_y = tm.mkTerm(Kind.NOT, x_eq_y) names = {x_eq_y: "as1", not_x_eq_y: "as2"} solver.assertFormula(x_eq_y) solver.assertFormula(not_x_eq_y) assert solver.checkSat().isUnsat() proofs = solver.getProof() assert len(proofs) > 0 printedProof = solver.proofToString(proofs[0], ProofFormat.ALETHE, names) assert len(printedProof) > 0 assert b"as1" in printedProof assert b"as2" in printedProof def test_learned_literals(solver): solver.setOption("produce-learned-literals", "true") with pytest.raises(RuntimeError): solver.getLearnedLiterals() solver.checkSat() solver.getLearnedLiterals() solver.getLearnedLiterals(LearnedLitType.PREPROCESS) def test_learned_literals2(tm, solver): solver.setOption("produce-learned-literals", "true") intSort = tm.getIntegerSort() x = tm.mkConst(intSort, "x") y = tm.mkConst(intSort, "y") zero = tm.mkInteger(0) ten = tm.mkInteger(10) f0 = tm.mkTerm(Kind.GEQ, x, ten) f1 = tm.mkTerm( Kind.OR, tm.mkTerm(Kind.GEQ, zero, x), tm.mkTerm(Kind.GEQ, y, zero)) solver.assertFormula(f0) solver.assertFormula(f1) solver.checkSat() solver.getLearnedLiterals(LearnedLitType.INPUT) def test_get_timeout_core_unsat(tm, solver): solver.setOption("timeout-core-timeout", "100") solver.setOption("produce-unsat-cores", "true") intSort = tm.getIntegerSort() x = tm.mkConst(intSort, "x") tt = tm.mkBoolean(True) hard = tm.mkTerm(Kind.EQUAL, tm.mkTerm(Kind.MULT, x, x), tm.mkInteger("501240912901901249014210220059591")) solver.assertFormula(tt) solver.assertFormula(hard) res = solver.getTimeoutCore() assert res[0].isUnknown() assert len(res[1]) == 1 assert res[1][0] == hard def test_get_timeout_core(tm, solver): solver.setOption("produce-unsat-cores", "true") ff = tm.mkBoolean(False) tt = tm.mkBoolean(True) solver.assertFormula(tt) solver.assertFormula(ff) solver.assertFormula(tt) res = solver.getTimeoutCore() assert res[0].isUnsat() assert len(res[1]) == 1 assert res[1][0] == ff def test_get_timeout_core_assuming(tm, solver): solver.setOption("produce-unsat-cores", "true") ff = tm.mkBoolean(False) tt = tm.mkBoolean(True) solver.assertFormula(tt) res = solver.getTimeoutCoreAssuming(ff, tt) assert res[0].isUnsat() assert len(res[1]) == 1 assert res[1][0] == ff def test_get_timeout_core_assuming_empty(solver): solver.setOption("produce-unsat-cores", "true") with pytest.raises(RuntimeError): res = solver.getTimeoutCoreAssuming() def test_get_value1(tm, solver): solver.setOption("produce-models", "false") t = tm.mkTrue() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValue(t) def test_get_value2(tm, solver): solver.setOption("produce-models", "true") t = tm.mkFalse() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValue(t) def test_get_value3(tm, solver): solver.setOption("produce-models", "true") uSort = tm.mkUninterpretedSort("u") intSort = tm.getIntegerSort() boolSort = tm.getBooleanSort() uToIntSort = tm.mkFunctionSort(uSort, intSort) intPredSort = tm.mkFunctionSort(intSort, boolSort) x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") z = tm.mkConst(uSort, "z") f = tm.mkConst(uToIntSort, "f") p = tm.mkConst(intPredSort, "p") zero = tm.mkInteger(0) one = tm.mkInteger(1) f_x = tm.mkTerm(Kind.APPLY_UF, f, x) f_y = tm.mkTerm(Kind.APPLY_UF, f, y) summ = tm.mkTerm(Kind.ADD, f_x, f_y) p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero) p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y) solver.assertFormula(tm.mkTerm(Kind.LEQ, zero, f_x)) solver.assertFormula(tm.mkTerm(Kind.LEQ, zero, f_y)) solver.assertFormula(tm.mkTerm(Kind.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) a = [solver.getValue(x), solver.getValue(y), solver.getValue(z)] b = solver.getValue([x,y,z]) assert a == b with pytest.raises(RuntimeError): Solver(tm).getValue(x) slv = Solver(tm) slv.setOption("produce-models", "true") slv.checkSat() slv.getValue(x) ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-models", "true") slv.checkSat() with pytest.raises(RuntimeError): slv.getValue(tm.mkConst(tm.getBooleanSort(), "x")) def test_declare_sep_heap(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") integer = tm.getIntegerSort() solver.declareSepHeap(integer, integer) # cannot declare separation logic heap more than once with pytest.raises(RuntimeError): solver.declareSepHeap(integer, integer) with pytest.raises(RuntimeError): # no logic set yet Solver(tm).declareSepHeap(tm.getIntegerSort(), tm.getIntegerSort()) ttm = TermManager() slv = Solver(ttm) slv.setLogic("ALL") with pytest.raises(RuntimeError): slv.declareSepHeap(integer, ttm.getRealSort()) slv = Solver(ttm) slv.setLogic("ALL"); with pytest.raises(RuntimeError): slv.declareSepHeap(ttm.getBooleanSort(), integer) # Helper function for test_get_separation_{heap,nil}_termX. Asserts and checks # some simple separation logic constraints. def checkSimpleSeparationConstraints(slv): tm = slv.getTermManager() integer = tm.getIntegerSort() # declare the separation heap slv.declareSepHeap(integer, integer) x = tm.mkConst(integer, "x") p = tm.mkConst(integer, "p") heap = tm.mkTerm(Kind.SEP_PTO, p, x) slv.assertFormula(heap) nil = tm.mkSepNil(integer) slv.assertFormula(nil.eqTerm(tm.mkInteger(5))) slv.checkSat() def test_get_value_sep_heap_1(tm, solver): solver.setLogic("QF_BV") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkTrue() solver.assertFormula(t) with pytest.raises(RuntimeError): solver.getValueSepHeap() def test_get_value_sep_heap_2(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_heap_3(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkFalse() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValueSepHeap() def test_get_value_sep_heap_4(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkTrue() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValueSepHeap() def test_get_value_sep_heap_5(solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") checkSimpleSeparationConstraints(solver) solver.getValueSepHeap() def test_get_value_sep_nil_1(tm, solver): solver.setLogic("QF_BV") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkTrue() solver.assertFormula(t) with pytest.raises(RuntimeError): solver.getValueSepNil() def test_get_value_sep_nil_2(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_nil_3(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkFalse() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValueSepNil() def test_get_value_sep_nil_4(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkTrue() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValueSepNil() def test_get_value_sep_nil_5(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_block_model1(tm, solver): x = tm.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) solver.checkSat() with pytest.raises(RuntimeError): solver.blockModel(BlockModelsMode.LITERALS) def test_block_model2(tm, solver): solver.setOption("produce-models", "true") x = tm.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) with pytest.raises(RuntimeError): solver.blockModel(BlockModelsMode.LITERALS) def test_block_model3(tm, solver): solver.setOption("produce-models", "true") x = tm.mkConst(solver.getBooleanSort(), "x"); solver.assertFormula(x.eqTerm(x)) solver.checkSat() solver.blockModel(BlockModelsMode.LITERALS) def test_block_model_values1(tm, solver): solver.setOption("produce-models", "true") x = tm.mkConst(solver.getBooleanSort(), "x"); solver.assertFormula(x.eqTerm(x)) solver.checkSat() with pytest.raises(RuntimeError): solver.blockModelValues([]) solver.blockModelValues([tm.mkBoolean(False)]) ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-models", "true") slv.checkSat() with pytest.raises(RuntimeError): slv.blockModelValues([tm.mkFalse()]) def test_block_model_values2(tm, solver): solver.setOption("produce-models", "true") x = tm.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) solver.checkSat() solver.blockModelValues([x]) def test_block_model_values3(tm, solver): x = tm.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) solver.checkSat() with pytest.raises(RuntimeError): solver.blockModelValues([x]) def test_block_model_values4(tm, solver): solver.setOption("produce-models", "true") x = tm.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) with pytest.raises(RuntimeError): solver.blockModelValues([x]) def test_block_model_values5(tm, solver): solver.setOption("produce-models", "true") x = tm.mkConst(solver.getBooleanSort(), "x") solver.assertFormula(x.eqTerm(x)) solver.checkSat() solver.blockModelValues([x]) def test_get_instantiations(tm, solver): iSort = tm.getIntegerSort() boolSort = solver.getBooleanSort() p = solver.declareFun("p", [iSort], boolSort) x = tm.mkVar(iSort, "x") bvl = tm.mkTerm(Kind.VARIABLE_LIST, x) app = tm.mkTerm(Kind.APPLY_UF, p, x) q = tm.mkTerm(Kind.FORALL, bvl, app) solver.assertFormula(q) five = tm.mkInteger(5) app2 = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.APPLY_UF, p, five)) solver.assertFormula(app2) with pytest.raises(RuntimeError): solver.getInstantiations() solver.checkSat() solver.getInstantiations() def test_get_statistics(tm, solver): # do some array reasoning to make sure we have a double statistics s1 = tm.getIntegerSort() s2 = tm.mkArraySort(s1, s1) t1 = tm.mkConst(s1, "i") t2 = tm.mkVar(s2, "a") t3 = tm.mkTerm(Kind.SELECT, t2, t1) solver.checkSat() stats = solver.getStatistics() assert not stats['global::totalTime']['internal'] assert not stats['global::totalTime']['default'] assert stats['global::totalTime']['value'][-2:] == 'ms' # ends with 'ms' assert stats['resource::resourceUnitsUsed']['internal'] assert not stats['resource::resourceUnitsUsed']['default'] assert stats.get(True)['resource::resourceUnitsUsed']['internal'] assert not stats.get(True)['resource::resourceUnitsUsed']['default'] assert '' not in stats assert len([s for s in stats]) > 0 for s in stats: str(s) if s[0] == 'theory::arrays::avgIndexListLength': assert s[1]['internal'] assert s[1]['default'] assert isnan(s[1]['value']) def test_set_info(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(tm, solver): bvSort = tm.mkBitVectorSort(32) uSort = tm.mkUninterpretedSort("u") funSort1 = tm.mkFunctionSort([bvSort, bvSort], bvSort) funSort2 = tm.mkFunctionSort(uSort, tm.getIntegerSort()) consListSpec = tm.mkDatatypeDecl("list") cons = tm.mkDatatypeConstructorDecl("cons") cons.addSelector("head", tm.getIntegerSort()) cons.addSelectorSelf("tail") consListSpec.addConstructor(cons) nil = tm.mkDatatypeConstructorDecl("nil") consListSpec.addConstructor(nil) consListSort = tm.mkDatatypeSort(consListSpec) x = tm.mkConst(bvSort, "x") solver.simplify(x) a = tm.mkConst(bvSort, "a") solver.simplify(a) b = tm.mkConst(bvSort, "b") solver.simplify(b) x_eq_x = tm.mkTerm(Kind.EQUAL, x, x) solver.simplify(x_eq_x) assert tm.mkTrue() != x_eq_x assert tm.mkTrue() == solver.simplify(x_eq_x) x_eq_b = tm.mkTerm(Kind.EQUAL, x, b) solver.simplify(x_eq_b) assert tm.mkTrue() != x_eq_b assert tm.mkTrue() != solver.simplify(x_eq_b) slv = Solver(tm) slv.simplify(x) i1 = tm.mkConst(tm.getIntegerSort(), "i1") solver.simplify(i1) i2 = tm.mkTerm(Kind.MULT, i1, tm.mkInteger("23")) solver.simplify(i2) assert i1 != i2 assert i1 != solver.simplify(i2) i3 = tm.mkTerm(Kind.ADD, i1, tm.mkInteger(0)) solver.simplify(i3) assert i1 != i3 assert i1 == solver.simplify(i3) consList = consListSort.getDatatype() dt1 = tm.mkTerm( Kind.APPLY_CONSTRUCTOR, consList.getConstructor("cons").getTerm(), tm.mkInteger(0), tm.mkTerm( Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm())) solver.simplify(dt1) dt2 = tm.mkTerm( Kind.APPLY_SELECTOR, consList["cons"].getSelector("head").getTerm(), dt1) solver.simplify(dt2) b1 = tm.mkVar(bvSort, "b1") solver.simplify(b1) b2 = tm.mkVar(bvSort, "b1") solver.simplify(b2) b3 = tm.mkVar(uSort, "b3") solver.simplify(b3) v1 = tm.mkConst(bvSort, "v1") solver.simplify(v1) v2 = tm.mkConst(tm.getIntegerSort(), "v2") solver.simplify(v2) f1 = tm.mkConst(funSort1, "f1") solver.simplify(f1) f2 = tm.mkConst(funSort2, "f2") solver.simplify(f2) solver.defineFunsRec([f1, f2], [[b1, b2], [b3]], [v1, v2]) solver.simplify(f1) solver.simplify(f2) ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): slv.simplify(x) def test_simplify_apply_subs(tm, solver): solver.setOption("incremental", "true") intSort = tm.getIntegerSort() x = tm.mkConst(intSort, "x") zero = tm.mkInteger(0) eq = tm.mkTerm(Kind.EQUAL, x, zero) solver.assertFormula(eq) solver.checkSat() assert solver.simplify(x, False) == x assert solver.simplify(x, True) == zero def test_assert_formula(tm, solver): solver.assertFormula(tm.mkTrue()) slv = Solver(tm) slv.assertFormula(tm.mkTrue()) ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): slv.assertFormula(tm.mkTrue()) def test_check_sat(solver): solver.setOption("incremental", "false") solver.checkSat() with pytest.raises(RuntimeError): solver.checkSat() def test_check_sat_assuming(tm, solver): solver.setOption("incremental", "false") solver.checkSatAssuming(tm.mkTrue()) with pytest.raises(RuntimeError): solver.checkSatAssuming(tm.mkTrue()) slv = Solver(tm) slv.checkSatAssuming(tm.mkTrue()) ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): slv.checkSatAssuming(tm.mkTrue()) def test_check_sat_assuming1(tm, solver): boolSort = tm.getBooleanSort() x = tm.mkConst(boolSort, "x") y = tm.mkConst(boolSort, "y") z = tm.mkTerm(Kind.AND, x, y) solver.setOption("incremental", "true") solver.checkSatAssuming(tm.mkTrue()) solver.checkSatAssuming(tm.mkTrue()) solver.checkSatAssuming(z) slv = Solver(tm) slv.checkSatAssuming(tm.mkTrue()) def test_check_sat_assuming2(tm, solver): solver.setOption("incremental", "true") uSort = tm.mkUninterpretedSort("u") intSort = tm.getIntegerSort() boolSort = solver.getBooleanSort() uToIntSort = tm.mkFunctionSort(uSort, intSort) intPredSort = tm.mkFunctionSort(intSort, boolSort) # Constants x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") # Functions f = tm.mkConst(uToIntSort, "f") p = tm.mkConst(intPredSort, "p") # Values zero = tm.mkInteger(0) one = tm.mkInteger(1) # Terms f_x = tm.mkTerm(Kind.APPLY_UF, f, x) f_y = tm.mkTerm(Kind.APPLY_UF, f, y) summ = tm.mkTerm(Kind.ADD, f_x, f_y) p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero) p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y) # Assertions assertions =\ tm.mkTerm(Kind.AND,\ tm.mkTerm(Kind.LEQ, zero, f_x), # 0 <= f(x) tm.mkTerm(Kind.LEQ, zero, f_y), # 0 <= f(y) tm.mkTerm(Kind.LEQ, summ, one), # f(x) + f(y) <= 1 p_0.notTerm(), # not p(0) p_f_y # p(f(y)) ) solver.checkSatAssuming(tm.mkTrue()) solver.assertFormula(assertions) solver.checkSatAssuming(tm.mkTerm(Kind.DISTINCT, x, y)) solver.checkSatAssuming( tm.mkFalse(), tm.mkTerm(Kind.DISTINCT, x, y)) slv = Solver(tm) slv.checkSatAssuming(tm.mkTrue()) def test_set_logic(tm, solver): solver.setLogic("AUFLIRA") with pytest.raises(RuntimeError): solver.setLogic("AF_BV") solver.assertFormula(tm.mkTrue()) with pytest.raises(RuntimeError): solver.setLogic("AUFLIRA") def test_is_logic_set(solver): assert solver.isLogicSet() == False solver.setLogic("QF_BV") assert solver.isLogicSet() == True def test_get_logic(solver): with pytest.raises(RuntimeError): solver.getLogic() solver.setLogic("QF_BV") assert solver.getLogic() == "QF_BV" def test_set_option(tm, solver): solver.setOption("bv-sat-solver", "minisat") with pytest.raises(RuntimeError): solver.setOption("bv-sat-solver", "1") solver.assertFormula(tm.mkTrue()) with pytest.raises(RuntimeError): solver.setOption("bv-sat-solver", "minisat") def test_reset_assertions(tm, solver): solver.setOption("incremental", "true") bvSort = tm.mkBitVectorSort(4) one = tm.mkBitVector(4, 1) x = tm.mkConst(bvSort, "x") ule = tm.mkTerm(Kind.BITVECTOR_ULE, x, one) srem = tm.mkTerm(Kind.BITVECTOR_SREM, one, x) solver.push(4) slt = tm.mkTerm(Kind.BITVECTOR_SLT, srem, one) solver.resetAssertions() solver.checkSatAssuming(slt, ule) def test_declare_sygus_var(tm, solver): solver.setOption("sygus", "true") boolSort = tm.getBooleanSort() intSort = tm.getIntegerSort() funSort = tm.mkFunctionSort([intSort], boolSort) solver.declareSygusVar("", boolSort) solver.declareSygusVar("", funSort) solver.declareSygusVar("b", boolSort) with pytest.raises(RuntimeError): solver.declareSygusVar("", cvc5.Sort()) with pytest.raises(RuntimeError): solver.declareSygusVar("a", cvc5.Sort()) with pytest.raises(RuntimeError): Solver(tm).declareSygusVar("", boolSort) ttm = TermManager() slv = Solver(ttm) slv.setOption("sygus", "true") with pytest.raises(RuntimeError): slv.declareSygusVar("", boolSort) def test_mk_sygus_grammar(tm, solver): boolTerm = tm.mkBoolean(True) boolVar = tm.mkVar(solver.getBooleanSort()) intVar = tm.mkVar(tm.getIntegerSort()) solver.mkGrammar([], [intVar]) solver.mkGrammar([boolVar], [intVar]) with pytest.raises(RuntimeError): solver.mkGrammar([], []) with pytest.raises(RuntimeError): solver.mkGrammar([], [boolTerm]) with pytest.raises(RuntimeError): solver.mkGrammar([boolTerm], [intVar]) slv = Solver(tm) boolVar2 = tm.mkVar(tm.getBooleanSort()) intVar2 = tm.mkVar(tm.getIntegerSort()) slv.mkGrammar([boolVar2], [intVar2]) slv.mkGrammar([boolVar], [intVar2]) slv.mkGrammar([boolVar2], [intVar]) ttm = TermManager() slv = Solver(ttm) slv.setOption("sygus", "true") boolVar2 = ttm.mkVar(ttm.getBooleanSort()) intVar2 = ttm.mkVar(ttm.getIntegerSort()) slv.mkGrammar([boolVar2], [intVar2]) with pytest.raises(RuntimeError): slv.mkGrammar([boolVar], [intVar2]) with pytest.raises(RuntimeError): slv.mkGrammar([boolVar2], [intVar]) def test_add_sygus_constraint(tm, solver): solver.setOption("sygus", "true") boolTerm = tm.mkBoolean(True) intTerm = tm.mkInteger(1) solver.addSygusConstraint(boolTerm) with pytest.raises(RuntimeError): solver.addSygusConstraint(intTerm) slv = Solver(tm) with pytest.raises(RuntimeError): slv.addSygusConstraint(boolTerm) ttm = TermManager() slv = Solver(ttm) slv.setOption("sygus", "true") with pytest.raises(RuntimeError): slv.addSygusConstraint(boolTerm) def test_get_sygus_constraints(tm, solver): solver.setOption("sygus", "true") true_term = tm.mkBoolean(True) false_term = tm.mkBoolean(False) solver.addSygusConstraint(true_term) solver.addSygusConstraint(false_term) constraints = [true_term, false_term] assert solver.getSygusConstraints() == constraints def test_add_sygus_assume(tm, solver): solver.setOption("sygus", "true") boolTerm = tm.mkBoolean(False) intTerm = tm.mkInteger(1) solver.addSygusAssume(boolTerm) with pytest.raises(RuntimeError): solver.addSygusAssume(intTerm) slv = Solver(tm) with pytest.raises(RuntimeError): slv.addSygusAssume(boolTerm) ttm = TermManager() slv = Solver(ttm) slv.setOption("sygus", "true") with pytest.raises(RuntimeError): slv.addSygusAssume(boolTerm) def test_get_sygus_assumptions(tm, solver): solver.setOption("sygus", "true") true_term = tm.mkBoolean(True) false_term = tm.mkBoolean(False) solver.addSygusAssume(true_term) solver.addSygusAssume(false_term) assumptions = [true_term, false_term] assert solver.getSygusAssumptions() == assumptions def test_add_sygus_inv_constraint(tm, solver): solver.setOption("sygus", "true") boolean = solver.getBooleanSort() real = solver.getRealSort() intTerm = tm.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(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 = Solver(tm) slv.setOption("sygus", "true") boolean2 = tm.getBooleanSort() real2 = tm.getRealSort() inv22 = solver.declareFun("inv", [real2], boolean2) pre22 = solver.declareFun("pre", [real2], boolean2) trans22 = solver.declareFun("trans", [real2, real2], boolean2) post22 = solver.declareFun("post", [real2], boolean2) slv.addSygusInvConstraint(inv22, pre22, trans22, post22) slv.addSygusInvConstraint(inv, pre22, trans22, post22) slv.addSygusInvConstraint(inv22, pre, trans22, post22) slv.addSygusInvConstraint(inv22, pre22, trans, post22) slv.addSygusInvConstraint(inv22, pre22, trans22, post) ttm = TermManager() slv = Solver(ttm) slv.setOption("sygus", "true") boolean2 = ttm.getBooleanSort() real2 = ttm.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_check_synth(solver): with pytest.raises(RuntimeError): solver.checkSynth() solver.setOption("sygus", "true") solver.checkSynth() def test_get_synth_solution(tm, solver): solver.setOption("sygus", "true") solver.setOption("incremental", "false") x = tm.mkBoolean(False) f = solver.synthFun("f", [], solver.getBooleanSort()) with pytest.raises(RuntimeError): solver.getSynthSolution(f) res = solver.checkSynth() assert res.hasSolution() solver.getSynthSolution(f) solver.getSynthSolution(f) with pytest.raises(RuntimeError): solver.getSynthSolution(x) slv = Solver(tm) with pytest.raises(RuntimeError): slv.getSynthSolution(f) def test_check_synth_next(solver): solver.setOption("sygus", "true") solver.setOption("incremental", "true") f = solver.synthFun("f", [], solver.getBooleanSort()) res = solver.checkSynth() assert res.hasSolution() solver.getSynthSolutions([f]) res = solver.checkSynthNext() assert res.hasSolution() solver.getSynthSolutions([f]) def test_check_synth_next2(solver): solver.setOption("sygus", "true") solver.setOption("incremental", "false") f = solver.synthFun("f", [], solver.getBooleanSort()) solver.checkSynth() with pytest.raises(RuntimeError): solver.checkSynthNext() def test_check_synth_next3(solver): solver.setOption("sygus", "true") solver.setOption("incremental", "true") f = solver.synthFun("f", [], solver.getBooleanSort()) with pytest.raises(RuntimeError): solver.checkSynthNext() def test_find_synth(tm, solver): solver.setOption("sygus", "true") boolSort = solver.getBooleanSort() start = tm.mkVar(boolSort) g = solver.mkGrammar([], [start]) truen = tm.mkBoolean(True) falsen = tm.mkBoolean(False) g.addRule(start, truen) g.addRule(start, falsen) f = solver.synthFun("f", [], solver.getBooleanSort(), g) # should enumerate based on the grammar of the function to synthesize above t = solver.findSynth(FindSynthTarget.ENUM) assert not t.isNull() and t.getSort().isBoolean() def test_find_synth2(tm, solver): solver.setOption("sygus", "true") solver.setOption("incremental", "true") boolSort = solver.getBooleanSort() start = tm.mkVar(boolSort) g = solver.mkGrammar([], [start]) truen = tm.mkBoolean(True) falsen = tm.mkBoolean(False) g.addRule(start, truen) g.addRule(start, falsen) # should enumerate true/false t = solver.findSynth(FindSynthTarget.ENUM, g) assert not t.isNull() and t.getSort().isBoolean() t = solver.findSynthNext() assert not t.isNull() and t.getSort().isBoolean() def test_get_abduct(tm, solver): solver.setLogic("QF_LIA") solver.setOption("produce-abducts", "true") solver.setOption("incremental", "false") intSort = tm.getIntegerSort() zero = tm.mkInteger(0) x = tm.mkConst(intSort, "x") y = tm.mkConst(intSort, "y") solver.assertFormula(tm.mkTerm(Kind.GT, x, zero)) conj = tm.mkTerm(Kind.GT, y, zero) output = solver.getAbduct(conj) assert not output.isNull() and output.getSort().isBoolean() boolean = solver.getBooleanSort() truen = tm.mkBoolean(True) start = tm.mkVar(boolean) g = solver.mkGrammar([], [start]) conj2 = tm.mkTerm(Kind.GT, x, zero) g.addRule(start, truen) output2 = solver.getAbduct(conj2, g) assert output2 == truen ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-abducts", "true") intSort2 = ttm.getIntegerSort() xx = ttm.mkConst(intSort2, "x") yy = ttm.mkConst(intSort2, "y") zzero = ttm.mkInteger(0) sstart = ttm.mkVar(ttm.getBooleanSort()) slv.assertFormula( ttm.mkTerm(Kind.GT, ttm.mkTerm(Kind.ADD, xx, yy), zzero)) gg = slv.mkGrammar([], [sstart]) gg.addRule(sstart, ttm.mkTrue()) cconj2 = ttm.mkTerm(Kind.EQUAL, zzero, zzero) slv.getAbduct(cconj2, gg) with pytest.raises(RuntimeError): slv.getAbduct(conj2) with pytest.raises(RuntimeError): slv.getAbduct(conj2, gg) with pytest.raises(RuntimeError): slv.getAbduct(cconj2, g) def test_get_abduct2(tm, solver): solver.setLogic("QF_LIA") solver.setOption("incremental", "false") intSort = tm.getIntegerSort() zero = tm.mkInteger(0) x = tm.mkConst(intSort, "x") y = tm.mkConst(intSort, "y") solver.assertFormula(tm.mkTerm(Kind.GT, x, zero)) conj = tm.mkTerm(Kind.GT, y, zero) with pytest.raises(RuntimeError): solver.getAbduct(conj) def test_get_abduct_next(tm, solver): solver.setLogic("QF_LIA") solver.setOption("produce-abducts", "true") solver.setOption("incremental", "true") intSort = tm.getIntegerSort() zero = tm.mkInteger(0) x = tm.mkConst(intSort, "x") y = tm.mkConst(intSort, "y") solver.assertFormula(tm.mkTerm(Kind.GT, x, zero)) conj = tm.mkTerm(Kind.GT, y, zero) output = solver.getAbduct(conj) output2 = solver.getAbductNext() assert output != output2 def test_get_interpolant(tm, solver): solver.setLogic("QF_LIA") solver.setOption("produce-interpolants", "true") solver.setOption("incremental", "false") intSort = tm.getIntegerSort() zero = tm.mkInteger(0) x = tm.mkConst(intSort, "x") y = tm.mkConst(intSort, "y") z = tm.mkConst(intSort, "z") solver.assertFormula(tm.mkTerm( Kind.GT, tm.mkTerm(Kind.ADD, x, y), zero)) solver.assertFormula(tm.mkTerm(Kind.LT, x, zero)) conj = tm.mkTerm( Kind.OR, tm.mkTerm(Kind.GT, tm.mkTerm(Kind.ADD, y, z), zero), tm.mkTerm(Kind.LT, z, zero)) output = solver.getInterpolant(conj) assert output.getSort().isBoolean() boolean = solver.getBooleanSort() truen = tm.mkBoolean(True) start = tm.mkVar(boolean) g = solver.mkGrammar([], [start]) conj2 = tm.mkTerm(Kind.EQUAL, zero, zero) g.addRule(start, truen) output2 = solver.getInterpolant(conj2, g) assert output2 == truen ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-interpolants", "true") intSort2 = ttm.getIntegerSort() xx = ttm.mkConst(intSort2, "x") yy = ttm.mkConst(intSort2, "y") zzero = ttm.mkInteger(0) sstart = ttm.mkVar(ttm.getBooleanSort()) slv.assertFormula( ttm.mkTerm(Kind.GT, ttm.mkTerm(Kind.ADD, xx, yy), zzero)) gg = slv.mkGrammar([], [sstart]) gg.addRule(sstart, ttm.mkTrue()) cconj2 = ttm.mkTerm(Kind.EQUAL, zzero, zzero) slv.getInterpolant(cconj2, gg) with pytest.raises(RuntimeError): slv.getInterpolant(conj2) with pytest.raises(RuntimeError): slv.getInterpolant(conj2, gg) with pytest.raises(RuntimeError): slv.getInterpolant(cconj2, g) def test_get_interpolant_next(tm, solver): solver.setLogic("QF_LIA") solver.setOption("produce-interpolants", "true") solver.setOption("incremental", "true") intSort = tm.getIntegerSort() zero = tm.mkInteger(0) x = tm.mkConst(intSort, "x") y = tm.mkConst(intSort, "y") z = tm.mkConst(intSort, "z") solver.assertFormula(tm.mkTerm( Kind.GT, tm.mkTerm(Kind.ADD, x, y), zero)) solver.assertFormula(tm.mkTerm(Kind.LT, x, zero)) conj = tm.mkTerm( Kind.OR, tm.mkTerm(Kind.GT, tm.mkTerm(Kind.ADD, y, z), zero), tm.mkTerm(Kind.LT, z, zero)) output = solver.getInterpolant(conj) output2 = solver.getInterpolantNext() assert output != output2 def test_declare_pool(tm, solver): intSort = tm.getIntegerSort() setSort = tm.mkSetSort(intSort) zero = tm.mkInteger(0) x = tm.mkConst(intSort, "x") y = tm.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 ttm = TermManager() slv = Solver(ttm) with pytest.raises(RuntimeError): slv.declarePool( "p", tm.getIntegerSort(), [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")]) with pytest.raises(RuntimeError): slv.declarePool( "p", tm.getIntegerSort(), [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")]) with pytest.raises(RuntimeError): slv.declarePool( "p", tm.getIntegerSort(), [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")]) with pytest.raises(RuntimeError): slv.declarePool( "p", tm.getIntegerSort(), [tm.mkInteger(0), tm.mkConst(intSort, "x"), tm.mkConst(intSort, "y")]) def test_get_model_domain_elements(tm, solver): solver.setOption("produce-models", "true") uSort = tm.mkUninterpretedSort("u") intSort = tm.getIntegerSort() x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") z = tm.mkConst(uSort, "z") f = tm.mkTerm(Kind.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) ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-models", "true") slv.checkSat() with pytest.raises(RuntimeError): slv.getModelDomainElements(tm.mkUninterpretedSort("u")) def test_get_model_domain_elements2(tm, solver): solver.setOption("produce-models", "true") solver.setOption("finite-model-find", "true") uSort = tm.mkUninterpretedSort("u") x = tm.mkVar(uSort, "x") y = tm.mkVar(uSort, "y") eq = tm.mkTerm(Kind.EQUAL, x, y) bvl = tm.mkTerm(Kind.VARIABLE_LIST, x, y) f = tm.mkTerm(Kind.FORALL, bvl, eq) solver.assertFormula(f) solver.checkSat() solver.getModelDomainElements(uSort) assert len(solver.getModelDomainElements(uSort)) == 1 def test_get_synth_solutions(tm, solver): solver.setOption("sygus", "true") solver.setOption("incremental", "false") x = tm.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([x]) slv = Solver(tm) with pytest.raises(RuntimeError): slv.getSynthSolutions([x]) def test_get_value_sep_heap1(tm, solver): solver.setLogic("QF_BV") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.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(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkFalse() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValueSepHeap() def test_get_value_sep_heap4(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.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(tm, solver): solver.setLogic("QF_BV") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.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(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.mkFalse() solver.assertFormula(t) solver.checkSat() with pytest.raises(RuntimeError): solver.getValueSepNil() def test_get_value_sep_nil4(tm, solver): solver.setLogic("ALL") solver.setOption("incremental", "false") solver.setOption("produce-models", "true") t = tm.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(tm, solver): solver.setOption("produce-models", "true") solver.setOption("model-cores", "simple") uSort = tm.mkUninterpretedSort("u") x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") z = tm.mkConst(uSort, "z") zero = tm.mkInteger(0) f = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.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) ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-models", "true") slv.checkSat() with pytest.raises(RuntimeError): slv.isModelCoreSymbol(tm.mkConst(uSort, "x")) def test_get_model(tm, solver): solver.setOption("produce-models", "true") uSort = tm.mkUninterpretedSort("u") x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") z = tm.mkConst(uSort, "z") f = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, x, y)) solver.assertFormula(f) solver.checkSat() sorts = [uSort] terms = [x, y] solver.getModel(sorts, terms) def test_get_model2(tm): solver.setOption("produce-models", "true") sorts = [] terms = [] with pytest.raises(RuntimeError): solver.getModel(sorts, terms) def test_get_model3(tm, solver): solver.setOption("produce-models", "true") sorts = [] terms = [] solver.checkSat() solver.getModel(sorts, terms) integer = tm.getIntegerSort() sorts.append(integer) with pytest.raises(RuntimeError): solver.getModel(sorts, terms) def test_issue5893(tm): bvsort4 = tm.mkBitVectorSort(4) bvsort8 = tm.mkBitVectorSort(8) arrsort = tm.mkArraySort(bvsort4, bvsort8) arr = tm.mkConst(arrsort, "arr") idx = tm.mkConst(bvsort4, "idx") ten = tm.mkBitVector(8, "10", 10) sel = tm.mkTerm(Kind.SELECT, arr, idx) distinct = tm.mkTerm(Kind.DISTINCT, sel, ten) distinct.getOp() def test_issue7000(tm, solver): s1 = tm.getIntegerSort() s2 = tm.mkFunctionSort(s1, s1) s3 = solver.getRealSort() t4 = tm.mkPi() t7 = tm.mkConst(s3, "_x5") t37 = tm.mkConst(s2, "_x32") t59 = tm.mkConst(s2, "_x51") t72 = tm.mkTerm(Kind.EQUAL, t37, t59) t74 = tm.mkTerm(Kind.GT, t4, t7) query = tm.mkTerm(Kind.AND, t72, t74, t72, t72) # throws logic exception since logic is not higher order by default with pytest.raises(RuntimeError): solver.checkSatAssuming(query.notTerm()) def test_mk_sygus_var(tm, solver): solver.setOption("sygus", "true") boolSort = solver.getBooleanSort() intSort = tm.getIntegerSort() funSort = tm.mkFunctionSort(intSort, boolSort) solver.declareSygusVar("", boolSort) solver.declareSygusVar("", funSort) solver.declareSygusVar("b", boolSort) slv = Solver(tm) with pytest.raises(RuntimeError): slv.declareSygusVar("", boolSort) def test_synth_fun(tm, solver): solver.setOption("sygus", "true") boolean = solver.getBooleanSort() integer = tm.getIntegerSort() x = tm.mkVar(boolean) start1 = tm.mkVar(boolean) start2 = tm.mkVar(integer) g1 = solver.mkGrammar(x, [start1]) g1.addRule(start1, tm.mkBoolean(False)) g2 = solver.mkGrammar(x, [start2]) g2.addRule(start2, tm.mkInteger(0)) solver.synthFun("", [], boolean) solver.synthFun("f1", [x], boolean) solver.synthFun("f2", [x], boolean, g1) with pytest.raises(RuntimeError): solver.synthFun("f6", [x], boolean, g2) slv = Solver(tm) slv.setOption("sygus", "true") x2 = tm.mkVar(tm.getBooleanSort()) slv.synthFun("f1", [x2], tm.getBooleanSort()) slv.synthFun("", [], tm.getBooleanSort()) slv.synthFun("f1", [x], tm.getBooleanSort()) ttm = TermManager() slv = Solver(ttm) slv.setOption("sygus", "true") slv.checkSat() x2 = ttm.mkVar(ttm.getBooleanSort()) with pytest.raises(RuntimeError): slv.synthFun("f1", [x2], tm.getBooleanSort()) with pytest.raises(RuntimeError): slv.synthFun("", [], tm.getBooleanSort()) with pytest.raises(RuntimeError): slv.synthFun("f1", [x], ttm.getBooleanSort()) def test_tuple_project(tm, solver): elements = [\ tm.mkBoolean(True), \ tm.mkInteger(3),\ tm.mkString("C"),\ tm.mkTerm(Kind.SET_SINGLETON, tm.mkString("Z"))] tuple = tm.mkTuple(elements) indices1 = [] indices2 = [0] indices3 = [0, 1] indices4 = [0, 0, 2, 2, 3, 3, 0] indices5 = [4] indices6 = [0, 4] tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices1), tuple) tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices2), tuple) tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices3), tuple) tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices4), tuple) with pytest.raises(RuntimeError): tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices5), tuple) with pytest.raises(RuntimeError): tm.mkTerm(tm.mkOp(Kind.TUPLE_PROJECT, *indices6), tuple) indices = [0, 3, 2, 0, 1, 2] op = tm.mkOp(Kind.TUPLE_PROJECT, *indices) projection = tm.mkTerm(op, tuple) datatype = tuple.getSort().getDatatype() constructor = datatype[0] for i in indices: selectorTerm = constructor[i].getTerm() selectedTerm = tm.mkTerm(Kind.APPLY_SELECTOR, 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) def test_get_data_type_arity(tm, solver): ctor1 = tm.mkDatatypeConstructorDecl("_x21") ctor2 = tm.mkDatatypeConstructorDecl("_x31") s3 = solver.declareDatatype("_x17", ctor1, ctor2) assert s3.getDatatypeArity() == 0 def test_get_unsat_core_lemmas1(tm, solver): solver.setOption("produce-unsat-cores", "true") solver.setOption("unsat-cores-mode", "sat-proof") # cannot ask before a check sat with pytest.raises(RuntimeError): solver.getUnsatCoreLemmas() solver.assertFormula(tm.mkFalse()) assert solver.checkSat().isUnsat() solver.getUnsatCoreLemmas() def test_get_unsat_core_lemmas2(tm, solver): solver.setOption("produce-unsat-cores", "true") solver.setOption("unsat-cores-mode", "sat-proof") uSort = tm.mkUninterpretedSort("u") intSort = tm.getIntegerSort() boolSort = solver.getBooleanSort() uToIntSort = tm.mkFunctionSort(uSort, intSort) intPredSort = tm.mkFunctionSort(intSort, boolSort) x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") f = tm.mkConst(uToIntSort, "f") p = tm.mkConst(intPredSort, "p") zero = tm.mkInteger(0) one = tm.mkInteger(1) f_x = tm.mkTerm(Kind.APPLY_UF, f, x) f_y = tm.mkTerm(Kind.APPLY_UF, f, y) summ = tm.mkTerm(Kind.ADD, f_x, f_y) p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero) p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y) solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_x)) solver.assertFormula(tm.mkTerm(Kind.GT, zero, f_y)) solver.assertFormula(tm.mkTerm(Kind.GT, summ, one)) solver.assertFormula(p_0) solver.assertFormula(p_f_y.notTerm()) assert solver.checkSat().isUnsat() solver.getUnsatCoreLemmas() def test_get_difficulty(solver): solver.setOption("produce-difficulty", "true") # cannot ask before a check sat with pytest.raises(RuntimeError): solver.getDifficulty() solver.checkSat() solver.getDifficulty() def test_get_difficulty2(solver): solver.checkSat() with pytest.raises(RuntimeError): # option is not set solver.getDifficulty() def test_get_difficulty3(tm, solver): solver.setOption("produce-difficulty", "true") intSort = tm.getIntegerSort() x = tm.mkConst(intSort, "x") zero = tm.mkInteger(0) ten = tm.mkInteger(10) f0 = tm.mkTerm(Kind.GEQ, x, ten) f1 = tm.mkTerm(Kind.GEQ, zero, x) solver.checkSat() dmap = solver.getDifficulty() # difficulty should map assertions to integer values for key, value in dmap.items(): assert key == f0 or key == f1 assert value.getKind() == Kind.CONST_INTEGER def test_get_model(tm, solver): solver.setOption("produce-models", "true") uSort = tm.mkUninterpretedSort("u") x = tm.mkConst(uSort, "x") y = tm.mkConst(uSort, "y") z = tm.mkConst(uSort, "z") f = tm.mkTerm(Kind.NOT, tm.mkTerm(Kind.EQUAL, x, y)); solver.assertFormula(f) solver.checkSat() sorts = [uSort] terms = [x, y] solver.getModel(sorts, terms) def test_get_model2(solver): solver.setOption("produce-models", "true") sorts = [] terms = [] with pytest.raises(RuntimeError): solver.getModel(sorts, terms) def test_get_model_3(tm, solver): solver.setOption("produce-models", "true") sorts = [] terms = [] solver.checkSat() solver.getModel(sorts, terms) integer = tm.getIntegerSort() sorts += [integer] with pytest.raises(RuntimeError): solver.getModel(sorts, terms) def test_get_option_names(solver): names = solver.getOptionNames() assert len(names) > 100 assert "verbose" in names assert "foobar" not in names def test_get_quantifier_elimination(tm, solver): x = tm.mkVar(solver.getBooleanSort(), "x") forall = tm.mkTerm( Kind.FORALL, tm.mkTerm(Kind.VARIABLE_LIST, x), tm.mkTerm(Kind.OR, x, tm.mkTerm(Kind.NOT, x))) with pytest.raises(RuntimeError): solver.getQuantifierElimination(tm.mkBoolean(False)) solver.getQuantifierElimination(forall) ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-models", "true") slv.checkSat() xx = tm.mkVar(tm.getBooleanSort(), "x") fforall = tm.mkTerm( Kind.FORALL, tm.mkTerm(Kind.VARIABLE_LIST, xx), tm.mkTerm(Kind.OR, xx, tm.mkTerm(Kind.NOT, xx))) with pytest.raises(RuntimeError): slv.getQuantifierElimination(fforall) def test_get_quantifier_elimination_disjunct(tm, solver): x = tm.mkVar(solver.getBooleanSort(), "x") forall = tm.mkTerm( Kind.FORALL, tm.mkTerm(Kind.VARIABLE_LIST, x), tm.mkTerm(Kind.OR, x, tm.mkTerm(Kind.NOT, x))) with pytest.raises(RuntimeError): solver.getQuantifierEliminationDisjunct(tm.mkBoolean(False)) solver.getQuantifierEliminationDisjunct(forall) ttm = TermManager() slv = Solver(ttm) slv.setOption("produce-models", "true") slv.checkSat() xx = tm.mkVar(tm.getBooleanSort(), "x") fforall = tm.mkTerm( Kind.FORALL, tm.mkTerm(Kind.VARIABLE_LIST, xx), tm.mkTerm(Kind.OR, xx, tm.mkTerm(Kind.NOT, xx))) with pytest.raises(RuntimeError): slv.getQuantifierEliminationDisjunct(fforall) def test_get_version(solver): print(solver.getVersion()) class PluginUnsat(Plugin): def __init__(self, tm): super().__init__(tm) self.tm = tm def check(self): lemmas = [self.tm.mkBoolean(False)] return lemmas def getName(self): return "PluginUnsat" def test_plugin_unsat(tm, solver): p = PluginUnsat(tm) solver.addPlugin(p) assert solver.checkSat().isUnsat() class PluginListen(Plugin): def __init__(self, tm): super().__init__(tm) self.has_seen_theory_lemma = False self.has_seen_sat_clause = False def notifySatClause(self, cl): super().notifySatClause(cl) self.has_seen_sat_clause = True def hasSeenSatClause(self): return self.has_seen_sat_clause def notifyTheoryLemma(self, lem): super().notifyTheoryLemma(lem) self.has_seen_theory_lemma = True def hasSeenTheoryLemma(self): return self.has_seen_theory_lemma def getName(self): return "PluginListen" def test_plugin_listen(tm, solver): # NOTE: this shouldn't be necessary but ensures notifySatClause is called here. solver.setOption("plugin-notify-sat-clause-in-solve", "false") pl = PluginListen(tm) solver.addPlugin(pl) stringSort = tm.getStringSort() x = tm.mkConst(stringSort, "x") y = tm.mkConst(stringSort, "y") ctn1 = tm.mkTerm(Kind.STRING_CONTAINS, x, y) ctn2 = tm.mkTerm(Kind.STRING_CONTAINS, y, x) solver.assertFormula(tm.mkTerm(Kind.OR, ctn1, ctn2)) lx = tm.mkTerm(Kind.STRING_LENGTH, x) ly = tm.mkTerm(Kind.STRING_LENGTH, y) lc = tm.mkTerm(Kind.GT, lx, ly) solver.assertFormula(lc) assert solver.checkSat().isSat() # above input formulas should induce a theory lemma and SAT clause learning assert pl.hasSeenTheoryLemma() assert pl.hasSeenSatClause()