/****************************************************************************** * Top contributors (to current version): * Aina Niemetz, Andrew Reynolds, Gereon Kremer * * 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. * **************************************************************************** * * Black box testing of the Solver class of the C++ API. */ #include #include #include #include #include "base/output.h" #include "test_api.h" namespace cvc5::internal { namespace test { class TestApiBlackSolver : public TestApi { }; TEST_F(TestApiBlackSolver, pow2Large1) { // Based on https://github.com/cvc5/cvc5-projects/issues/371 Sort s4 = d_tm.mkArraySort(d_string, d_int); Sort s7 = d_tm.mkArraySort(d_int, d_string); Term t10 = d_tm.mkInteger("68038927088685865242724985643"); Term t74 = d_tm.mkInteger("8416288636405"); std::vector ctors; ctors.push_back(d_tm.mkDatatypeConstructorDecl("_x109")); ctors.back().addSelector("_x108", s7); ctors.push_back(d_tm.mkDatatypeConstructorDecl("_x113")); ctors.back().addSelector("_x110", s4); ctors.back().addSelector("_x111", d_int); ctors.back().addSelector("_x112", s7); Sort s11 = d_solver->declareDatatype("_x107", ctors); Term t82 = d_tm.mkConst(s11, "_x114"); Term t180 = d_tm.mkTerm(Kind::POW2, {t10}); Term t258 = d_tm.mkTerm(Kind::GEQ, {t74, t180}); d_solver->assertFormula(t258); ASSERT_THROW(d_solver->simplify(t82, true), CVC5ApiException); } TEST_F(TestApiBlackSolver, pow2Large2) { // Based on https://github.com/cvc5/cvc5-projects/issues/333 Term t1 = d_tm.mkBitVector(63, ~(((uint64_t)1) << 62)); Term t2 = d_tm.mkTerm(Kind::BITVECTOR_UBV_TO_INT, {t1}); Term t3 = d_tm.mkTerm(Kind::POW2, {t2}); Term t4 = d_tm.mkTerm(Kind::DISTINCT, {t3, t2}); ASSERT_THROW(d_solver->checkSatAssuming({t4}), CVC5ApiException); } TEST_F(TestApiBlackSolver, pow2Large3) { // Based on https://github.com/cvc5/cvc5-projects/issues/339 Term t203 = d_tm.mkInteger("6135470354240554220207"); Term t262 = d_tm.mkTerm(Kind::POW2, {t203}); Term t536 = d_tm.mkTerm(d_tm.mkOp(Kind::INT_TO_BITVECTOR, {49}), {t262}); // should not throw an exception, will not simplify. ASSERT_NO_THROW(d_solver->simplify(t536)); } TEST_F(TestApiBlackSolver, recoverableException) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x).notTerm()); ASSERT_THROW(d_solver->getValue(x), CVC5ApiRecoverableException); try { d_solver->getValue(x); } catch (const CVC5ApiRecoverableException& e) { ASSERT_NO_THROW(e.what()); ASSERT_NO_THROW(e.getMessage()); } } TEST_F(TestApiBlackSolver, simplify) { ASSERT_THROW(d_solver->simplify(Term()), CVC5ApiException); Sort bvSort = d_tm.mkBitVectorSort(32); Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int); DatatypeDecl consListSpec = d_tm.mkDatatypeDecl("list"); DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", d_int); cons.addSelectorSelf("tail"); consListSpec.addConstructor(cons); DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil"); consListSpec.addConstructor(nil); Sort consListSort = d_tm.mkDatatypeSort(consListSpec); Term x = d_tm.mkConst(bvSort, "x"); ASSERT_NO_THROW(d_solver->simplify(x)); Term a = d_tm.mkConst(bvSort, "a"); ASSERT_NO_THROW(d_solver->simplify(a)); Term b = d_tm.mkConst(bvSort, "b"); ASSERT_NO_THROW(d_solver->simplify(b)); Term x_eq_x = d_tm.mkTerm(Kind::EQUAL, {x, x}); ASSERT_NO_THROW(d_solver->simplify(x_eq_x)); ASSERT_NE(d_tm.mkTrue(), x_eq_x); ASSERT_EQ(d_tm.mkTrue(), d_solver->simplify(x_eq_x)); Term x_eq_b = d_tm.mkTerm(Kind::EQUAL, {x, b}); ASSERT_NO_THROW(d_solver->simplify(x_eq_b)); ASSERT_NE(d_tm.mkTrue(), x_eq_b); ASSERT_NE(d_tm.mkTrue(), d_solver->simplify(x_eq_b)); Term i1 = d_tm.mkConst(d_int, "i1"); ASSERT_NO_THROW(d_solver->simplify(i1)); Term i2 = d_tm.mkTerm(Kind::MULT, {i1, d_tm.mkInteger("23")}); ASSERT_NO_THROW(d_solver->simplify(i2)); ASSERT_NE(i1, i2); ASSERT_NE(i1, d_solver->simplify(i2)); Term i3 = d_tm.mkTerm(Kind::ADD, {i1, d_tm.mkInteger(0)}); ASSERT_NO_THROW(d_solver->simplify(i3)); ASSERT_NE(i1, i3); ASSERT_EQ(i1, d_solver->simplify(i3)); Datatype consList = consListSort.getDatatype(); Term dt1 = d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {consList.getConstructor("cons").getTerm(), d_tm.mkInteger(0), d_tm.mkTerm(Kind::APPLY_CONSTRUCTOR, {consList.getConstructor("nil").getTerm()})}); ASSERT_NO_THROW(d_solver->simplify(dt1)); Term dt2 = d_tm.mkTerm(Kind::APPLY_SELECTOR, {consList["cons"].getSelector("head").getTerm(), dt1}); ASSERT_NO_THROW(d_solver->simplify(dt2)); Term b1 = d_tm.mkVar(bvSort, "b1"); ASSERT_NO_THROW(d_solver->simplify(b1)); Term b2 = d_tm.mkVar(bvSort, "b1"); ASSERT_NO_THROW(d_solver->simplify(b2)); Term b3 = d_tm.mkVar(d_uninterpreted, "b3"); ASSERT_NO_THROW(d_solver->simplify(b3)); Term v1 = d_tm.mkConst(bvSort, "v1"); ASSERT_NO_THROW(d_solver->simplify(v1)); Term v2 = d_tm.mkConst(d_int, "v2"); ASSERT_NO_THROW(d_solver->simplify(v2)); Term f1 = d_tm.mkConst(funSort1, "f1"); ASSERT_NO_THROW(d_solver->simplify(f1)); Term f2 = d_tm.mkConst(funSort2, "f2"); ASSERT_NO_THROW(d_solver->simplify(f2)); d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b3}}, {v1, v2}); ASSERT_NO_THROW(d_solver->simplify(f1)); ASSERT_NO_THROW(d_solver->simplify(f2)); TermManager tm; Solver slv(tm); ASSERT_THROW(slv.simplify(x), CVC5ApiException); } TEST_F(TestApiBlackSolver, simplifyApplySubs) { d_solver->setOption("incremental", "true"); Term x = d_tm.mkConst(d_int, "x"); Term zero = d_tm.mkInteger(0); Term eq = d_tm.mkTerm(Kind::EQUAL, {x, zero}); d_solver->assertFormula(eq); ASSERT_NO_THROW(d_solver->checkSat()); ASSERT_EQ(d_solver->simplify(x, false), x); ASSERT_EQ(d_solver->simplify(x, true), zero); } TEST_F(TestApiBlackSolver, assertFormula) { ASSERT_NO_THROW(d_solver->assertFormula(d_tm.mkTrue())); ASSERT_THROW(d_solver->assertFormula(Term()), CVC5ApiException); TermManager tm; Solver slv(tm); ASSERT_THROW(slv.assertFormula(d_tm.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSat) { d_solver->setOption("incremental", "false"); ASSERT_NO_THROW(d_solver->checkSat()); ASSERT_THROW(d_solver->checkSat(), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSatAssuming) { d_solver->setOption("incremental", "false"); ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue())); ASSERT_THROW(d_solver->checkSatAssuming(d_tm.mkTrue()), CVC5ApiException); TermManager tm; Solver slv(tm); ASSERT_THROW(slv.checkSatAssuming(d_tm.mkTrue()), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSatAssuming1) { Term x = d_tm.mkConst(d_bool, "x"); Term y = d_tm.mkConst(d_bool, "y"); Term z = d_tm.mkTerm(Kind::AND, {x, y}); d_solver->setOption("incremental", "true"); ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue())); ASSERT_THROW(d_solver->checkSatAssuming(Term()), CVC5ApiException); ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue())); ASSERT_NO_THROW(d_solver->checkSatAssuming(z)); } TEST_F(TestApiBlackSolver, checkSatAssuming2) { d_solver->setOption("incremental", "true"); Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool); Term n = Term(); // Constants Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); // Functions Term f = d_tm.mkConst(uToIntSort, "f"); Term p = d_tm.mkConst(intPredSort, "p"); // Values Term zero = d_tm.mkInteger(0); Term one = d_tm.mkInteger(1); // Terms Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x}); Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y}); Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y}); Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero}); Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y}); // Assertions Term assertions = d_tm.mkTerm(Kind::AND, { d_tm.mkTerm(Kind::LEQ, {zero, f_x}), // 0 <= f(x) d_tm.mkTerm(Kind::LEQ, {zero, f_y}), // 0 <= f(y) d_tm.mkTerm(Kind::LEQ, {sum, one}), // f(x) + f(y) <= 1 p_0.notTerm(), // not p(0) p_f_y // p(f(y)) }); ASSERT_NO_THROW(d_solver->checkSatAssuming(d_tm.mkTrue())); d_solver->assertFormula(assertions); ASSERT_NO_THROW( d_solver->checkSatAssuming(d_tm.mkTerm(Kind::DISTINCT, {x, y}))); ASSERT_NO_THROW(d_solver->checkSatAssuming( {d_tm.mkFalse(), d_tm.mkTerm(Kind::DISTINCT, {x, y})})); ASSERT_THROW(d_solver->checkSatAssuming(n), CVC5ApiException); ASSERT_THROW( d_solver->checkSatAssuming({n, d_tm.mkTerm(Kind::DISTINCT, {x, y})}), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareFunFresh) { Term t1 = d_solver->declareFun(std::string("b"), {}, d_bool, true); Term t2 = d_solver->declareFun(std::string("b"), {}, d_bool, false); Term t3 = d_solver->declareFun(std::string("b"), {}, d_bool, false); ASSERT_FALSE(t1 == t2); ASSERT_FALSE(t1 == t3); ASSERT_TRUE(t2 == t3); Term t4 = d_solver->declareFun(std::string("c"), {}, d_bool, false); ASSERT_FALSE(t2 == t4); Term t5 = d_solver->declareFun(std::string("b"), {}, d_int, false); ASSERT_FALSE(t2 == t5); TermManager tm; Solver slv(tm); ASSERT_THROW(slv.declareFun(std::string("b"), {}, d_int, false), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareDatatype) { DatatypeConstructorDecl lin = d_tm.mkDatatypeConstructorDecl("lin"); std::vector ctors0 = {lin}; ASSERT_NO_THROW(d_solver->declareDatatype(std::string(""), ctors0)); DatatypeConstructorDecl nil = d_tm.mkDatatypeConstructorDecl("nil"); std::vector ctors1 = {nil}; ASSERT_NO_THROW(d_solver->declareDatatype(std::string("a"), ctors1)); DatatypeConstructorDecl cons = d_tm.mkDatatypeConstructorDecl("cons"); DatatypeConstructorDecl nil2 = d_tm.mkDatatypeConstructorDecl("nil"); std::vector ctors2 = {cons, nil2}; ASSERT_NO_THROW(d_solver->declareDatatype(std::string("b"), ctors2)); DatatypeConstructorDecl cons2 = d_tm.mkDatatypeConstructorDecl("cons"); DatatypeConstructorDecl nil3 = d_tm.mkDatatypeConstructorDecl("nil"); std::vector ctors3 = {cons2, nil3}; ASSERT_NO_THROW(d_solver->declareDatatype(std::string(""), ctors3)); // must have at least one constructor std::vector ctors4; ASSERT_THROW(d_solver->declareDatatype(std::string("c"), ctors4), CVC5ApiException); // constructors may not be reused DatatypeConstructorDecl ctor1 = d_tm.mkDatatypeConstructorDecl("_x21"); DatatypeConstructorDecl ctor2 = d_tm.mkDatatypeConstructorDecl("_x31"); d_solver->declareDatatype(std::string("_x17"), {ctor1, ctor2}); ASSERT_THROW(d_solver->declareDatatype(std::string("_x86"), {ctor1, ctor2}), CVC5ApiException); TermManager tm; Solver slv(tm); DatatypeConstructorDecl nnil = d_tm.mkDatatypeConstructorDecl("nil"); ASSERT_THROW(slv.declareDatatype(std::string("a"), {nnil}), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareFun) { Sort bvSort = d_tm.mkBitVectorSort(32); Sort funSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int); ASSERT_NO_THROW(d_solver->declareFun("f1", {}, bvSort)); ASSERT_NO_THROW(d_solver->declareFun("f3", {bvSort, d_int}, bvSort)); ASSERT_THROW(d_solver->declareFun("f2", {}, funSort), CVC5ApiException); // functions as arguments is allowed ASSERT_NO_THROW(d_solver->declareFun("f4", {bvSort, funSort}, bvSort)); ASSERT_THROW(d_solver->declareFun("f5", {bvSort, bvSort}, funSort), CVC5ApiException); TermManager tm; Solver slv(tm); ASSERT_THROW(slv.declareFun("f1", {}, bvSort), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareSort) { ASSERT_NO_THROW(d_solver->declareSort("s", 0)); ASSERT_NO_THROW(d_solver->declareSort("s", 2)); ASSERT_NO_THROW(d_solver->declareSort("", 2)); } TEST_F(TestApiBlackSolver, declareSortFresh) { Sort t1 = d_solver->declareSort(std::string("b"), 0, true); Sort t2 = d_solver->declareSort(std::string("b"), 0, false); Sort t3 = d_solver->declareSort(std::string("b"), 0, false); ASSERT_FALSE(t1 == t2); ASSERT_FALSE(t1 == t3); ASSERT_TRUE(t2 == t3); Sort t4 = d_solver->declareSort(std::string("c"), 0, false); ASSERT_FALSE(t2 == t4); Sort t5 = d_solver->declareSort(std::string("b"), 1, false); ASSERT_FALSE(t2 == t5); } TEST_F(TestApiBlackSolver, defineFun) { Sort bvSort = d_tm.mkBitVectorSort(32); Sort funSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Term b1 = d_tm.mkVar(bvSort, "b1"); Term b2 = d_tm.mkVar(d_int, "b2"); Term b3 = d_tm.mkVar(funSort, "b3"); Term v1 = d_tm.mkConst(bvSort, "v1"); Term v2 = d_tm.mkConst(funSort, "v2"); ASSERT_NO_THROW(d_solver->defineFun("f", {}, bvSort, v1)); ASSERT_NO_THROW(d_solver->defineFun("ff", {b1, b2}, bvSort, v1)); ASSERT_THROW(d_solver->defineFun("ff", {v1, b2}, bvSort, v1), CVC5ApiException); ASSERT_THROW(d_solver->defineFun("fff", {b1}, bvSort, v2), CVC5ApiException); ASSERT_THROW(d_solver->defineFun("ffff", {b1}, funSort, v2), CVC5ApiException); // b3 has function sort, which is allowed as an argument ASSERT_NO_THROW(d_solver->defineFun("fffff", {b1, b3}, bvSort, v1)); TermManager tm; Solver slv(tm); Sort bvSort2 = tm.mkBitVectorSort(32); Term v12 = tm.mkConst(bvSort2, "v1"); Term b12 = tm.mkVar(bvSort2, "b1"); Term b22 = tm.mkVar(tm.getIntegerSort(), "b2"); ASSERT_THROW(slv.defineFun("f", {}, bvSort, v12), CVC5ApiException); ASSERT_THROW(slv.defineFun("f", {}, bvSort2, v1), CVC5ApiException); ASSERT_THROW(slv.defineFun("ff", {b1, b22}, bvSort2, v12), CVC5ApiException); ASSERT_THROW(slv.defineFun("ff", {b12, b2}, bvSort2, v12), CVC5ApiException); ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort, v12), CVC5ApiException); ASSERT_THROW(slv.defineFun("ff", {b12, b22}, bvSort2, v1), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunGlobal) { Term bTrue = d_tm.mkBoolean(true); // (define-fun f () Bool true) Term f = d_solver->defineFun("f", {}, d_bool, bTrue, true); Term b = d_tm.mkVar(d_bool, "b"); // (define-fun g (b Bool) Bool b) Term g = d_solver->defineFun("g", {b}, d_bool, b, true); // (assert (or (not f) (not (g true)))) d_solver->assertFormula(d_tm.mkTerm( Kind::OR, {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver->checkSat().isUnsat()); d_solver->resetAssertions(); // (assert (or (not f) (not (g true)))) d_solver->assertFormula(d_tm.mkTerm( Kind::OR, {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver->checkSat().isUnsat()); TermManager tm; Solver slv(tm); ASSERT_THROW(slv.defineFun("f", {}, d_bool, bTrue, true), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunRec) { Sort bvSort = d_tm.mkBitVectorSort(32); Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Term b1 = d_tm.mkVar(bvSort, "b1"); Term b11 = d_tm.mkVar(bvSort, "b1"); Term b2 = d_tm.mkVar(d_int, "b2"); Term b3 = d_tm.mkVar(funSort2, "b3"); Term v1 = d_tm.mkConst(bvSort, "v1"); Term v2 = d_tm.mkConst(d_int, "v2"); Term v3 = d_tm.mkConst(funSort2, "v3"); Term f1 = d_tm.mkConst(funSort1, "f1"); Term f2 = d_tm.mkConst(funSort2, "f2"); Term f3 = d_tm.mkConst(bvSort, "f3"); ASSERT_NO_THROW(d_solver->defineFunRec("f", {}, bvSort, v1)); ASSERT_NO_THROW(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1)); ASSERT_NO_THROW(d_solver->defineFunRec(f1, {b1, b11}, v1)); ASSERT_THROW(d_solver->defineFunRec("fff", {b1}, bvSort, v3), CVC5ApiException); ASSERT_THROW(d_solver->defineFunRec("ff", {b1, v2}, bvSort, v1), CVC5ApiException); ASSERT_THROW(d_solver->defineFunRec("ffff", {b1}, funSort2, v3), CVC5ApiException); // b3 has function sort, which is allowed as an argument ASSERT_NO_THROW(d_solver->defineFunRec("fffff", {b1, b3}, bvSort, v1)); ASSERT_THROW(d_solver->defineFunRec(f1, {b1}, v1), CVC5ApiException); ASSERT_THROW(d_solver->defineFunRec(f1, {b1, b11}, v2), CVC5ApiException); ASSERT_THROW(d_solver->defineFunRec(f1, {b1, b11}, v3), CVC5ApiException); ASSERT_THROW(d_solver->defineFunRec(f2, {b1}, v2), CVC5ApiException); ASSERT_THROW(d_solver->defineFunRec(f3, {b1}, v1), CVC5ApiException); TermManager tm; Solver slv(tm); Sort bvSort2 = tm.mkBitVectorSort(32); Term v12 = tm.mkConst(bvSort2, "v1"); Term b12 = tm.mkVar(bvSort2, "b1"); Term b22 = tm.mkVar(tm.getIntegerSort(), "b2"); ASSERT_NO_THROW(slv.defineFunRec("f", {}, bvSort2, v12)); ASSERT_NO_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v12)); ASSERT_THROW(slv.defineFunRec("f", {}, bvSort, v12), CVC5ApiException); ASSERT_THROW(slv.defineFunRec("f", {}, bvSort2, v1), CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b1, b22}, bvSort2, v12), CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b12, b2}, bvSort2, v12), CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort, v12), CVC5ApiException); ASSERT_THROW(slv.defineFunRec("ff", {b12, b22}, bvSort2, v1), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunRecWrongLogic) { d_solver->setLogic("QF_BV"); Sort bvSort = d_tm.mkBitVectorSort(32); Sort funSort = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort); Term b = d_tm.mkVar(bvSort, "b"); Term v = d_tm.mkConst(bvSort, "v"); Term f = d_tm.mkConst(funSort, "f"); ASSERT_THROW(d_solver->defineFunRec("f", {}, bvSort, v), CVC5ApiException); ASSERT_THROW(d_solver->defineFunRec(f, {b, b}, v), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunRecGlobal) { d_solver->push(); Term bTrue = d_tm.mkBoolean(true); // (define-fun f () Bool true) Term f = d_solver->defineFunRec("f", {}, d_bool, bTrue, true); Term b = d_tm.mkVar(d_bool, "b"); // (define-fun g (b Bool) Bool b) Term g = d_solver->defineFunRec( d_tm.mkConst(d_tm.mkFunctionSort({d_bool}, d_bool), "g"), {b}, b, true); // (assert (or (not f) (not (g true)))) d_solver->assertFormula(d_tm.mkTerm( Kind::OR, {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver->checkSat().isUnsat()); d_solver->pop(); // (assert (or (not f) (not (g true)))) d_solver->assertFormula(d_tm.mkTerm( Kind::OR, {f.notTerm(), d_tm.mkTerm(Kind::APPLY_UF, {g, bTrue}).notTerm()})); ASSERT_TRUE(d_solver->checkSat().isUnsat()); TermManager tm; Solver slv(tm); Term bb = tm.mkVar(tm.getBooleanSort(), "b"); ASSERT_THROW( slv.defineFunRec(d_tm.mkConst(d_tm.mkFunctionSort({d_bool}, d_bool), "g"), {bb}, bb, true), CVC5ApiException); ASSERT_THROW( slv.defineFunRec( tm.mkConst(tm.mkFunctionSort({d_bool}, d_bool), "g"), {b}, b, true), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunsRec) { Sort bvSort = d_tm.mkBitVectorSort(32); Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Term b1 = d_tm.mkVar(bvSort, "b1"); Term b11 = d_tm.mkVar(bvSort, "b1"); Term b2 = d_tm.mkVar(d_int, "b2"); Term b4 = d_tm.mkVar(d_uninterpreted, "b4"); Term v1 = d_tm.mkConst(bvSort, "v1"); Term v2 = d_tm.mkConst(d_int, "v2"); Term v4 = d_tm.mkConst(d_uninterpreted, "v4"); Term f1 = d_tm.mkConst(funSort1, "f1"); Term f2 = d_tm.mkConst(funSort2, "f2"); Term f3 = d_tm.mkConst(bvSort, "f3"); ASSERT_NO_THROW( d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2})); ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{v1, b11}, {b4}}, {v1, v2}), CVC5ApiException); ASSERT_THROW(d_solver->defineFunsRec({f1, f3}, {{b1, b11}, {b4}}, {v1, v2}), CVC5ApiException); ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b1}, {b4}}, {v1, v2}), CVC5ApiException); ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b1, b2}, {b4}}, {v1, v2}), CVC5ApiException); ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v4}), CVC5ApiException); TermManager tm; Solver slv(tm); Sort uSort2 = tm.mkUninterpretedSort("u"); Sort bvSort2 = tm.mkBitVectorSort(32); Sort funSort12 = tm.mkFunctionSort({bvSort2, bvSort2}, bvSort2); Sort funSort22 = tm.mkFunctionSort({uSort2}, tm.getIntegerSort()); Term b12 = tm.mkVar(bvSort2, "b1"); Term b112 = tm.mkVar(bvSort2, "b1"); Term b42 = tm.mkVar(uSort2, "b4"); Term v12 = tm.mkConst(bvSort2, "v1"); Term v22 = tm.mkConst(tm.getIntegerSort(), "v2"); Term f12 = tm.mkConst(funSort12, "f1"); Term f22 = tm.mkConst(funSort22, "f2"); ASSERT_NO_THROW( slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v22})); ASSERT_THROW(slv.defineFunsRec({f1, f22}, {{b12, b112}, {b42}}, {v12, v22}), CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f2}, {{b12, b112}, {b42}}, {v12, v22}), CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b1, b112}, {b42}}, {v12, v22}), CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b11}, {b42}}, {v12, v22}), CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b4}}, {v12, v22}), CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v1, v22}), CVC5ApiException); ASSERT_THROW(slv.defineFunsRec({f12, f22}, {{b12, b112}, {b42}}, {v12, v2}), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunsRecWrongLogic) { d_solver->setLogic("QF_BV"); Sort bvSort = d_tm.mkBitVectorSort(32); Sort funSort1 = d_tm.mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Term b = d_tm.mkVar(bvSort, "b"); Term u = d_tm.mkVar(d_uninterpreted, "u"); Term v1 = d_tm.mkConst(bvSort, "v1"); Term v2 = d_tm.mkConst(d_int, "v2"); Term f1 = d_tm.mkConst(funSort1, "f1"); Term f2 = d_tm.mkConst(funSort2, "f2"); ASSERT_THROW(d_solver->defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}), CVC5ApiException); } TEST_F(TestApiBlackSolver, defineFunsRecGlobal) { Sort fSort = d_tm.mkFunctionSort({d_bool}, d_bool); d_solver->push(); Term bTrue = d_tm.mkBoolean(true); Term b = d_tm.mkVar(d_bool, "b"); Term gSym = d_tm.mkConst(fSort, "g"); // (define-funs-rec ((g ((b Bool)) Bool)) (b)) d_solver->defineFunsRec({gSym}, {{b}}, {b}, true); // (assert (not (g true))) d_solver->assertFormula(d_tm.mkTerm(Kind::APPLY_UF, {gSym, bTrue}).notTerm()); ASSERT_TRUE(d_solver->checkSat().isUnsat()); d_solver->pop(); // (assert (not (g true))) d_solver->assertFormula(d_tm.mkTerm(Kind::APPLY_UF, {gSym, bTrue}).notTerm()); ASSERT_TRUE(d_solver->checkSat().isUnsat()); } TEST_F(TestApiBlackSolver, getAssertions) { Term a = d_tm.mkConst(d_bool, "a"); Term b = d_tm.mkConst(d_bool, "b"); d_solver->assertFormula(a); d_solver->assertFormula(b); std::vector asserts{a, b}; ASSERT_EQ(d_solver->getAssertions(), asserts); } TEST_F(TestApiBlackSolver, getInfo) { ASSERT_NO_THROW(d_solver->getInfo("name")); ASSERT_THROW(d_solver->getInfo("asdf"), CVC5ApiException); } TEST_F(TestApiBlackSolver, getOption) { ASSERT_NO_THROW(d_solver->getOption("incremental")); ASSERT_THROW(d_solver->getOption("asdf"), CVC5ApiException); } TEST_F(TestApiBlackSolver, getOptionNames) { std::vector names = d_solver->getOptionNames(); ASSERT_TRUE(names.size() > 100); ASSERT_NE(std::find(names.begin(), names.end(), "verbose"), names.end()); ASSERT_EQ(std::find(names.begin(), names.end(), "foobar"), names.end()); } TEST_F(TestApiBlackSolver, getOptionInfo) { d_solver->setOption("verbosity", "2"); { ASSERT_THROW(d_solver->getOptionInfo("asdf-invalid"), CVC5ApiException); } { cvc5::OptionInfo info = d_solver->getOptionInfo("verbose"); ASSERT_EQ("verbose", info.name); ASSERT_EQ(std::vector{}, info.aliases); ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON); ASSERT_FALSE(info.setByUser); ASSERT_TRUE(std::holds_alternative(info.valueInfo)); std::stringstream ss; ss << info; ASSERT_EQ(ss.str(), "OptionInfo{ verbose | void }"); } { // bool type with default cvc5::OptionInfo info = d_solver->getOptionInfo("print-success"); ASSERT_EQ("print-success", info.name); ASSERT_EQ(std::vector{}, info.aliases); ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON); ASSERT_FALSE(info.setByUser); ASSERT_TRUE( std::holds_alternative>(info.valueInfo)); auto valInfo = std::get>(info.valueInfo); ASSERT_EQ(false, valInfo.defaultValue); ASSERT_EQ(false, valInfo.currentValue); ASSERT_EQ(info.boolValue(), false); std::stringstream ss; ss << info; ASSERT_EQ(ss.str(), "OptionInfo{ print-success | bool | false | default false }"); } { // int64 type with default cvc5::OptionInfo info = d_solver->getOptionInfo("verbosity"); ASSERT_EQ("verbosity", info.name); ASSERT_EQ(std::vector{}, info.aliases); ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON); ASSERT_TRUE(info.setByUser); ASSERT_TRUE(std::holds_alternative>( info.valueInfo)); auto numInfo = std::get>(info.valueInfo); ASSERT_EQ(0, numInfo.defaultValue); ASSERT_EQ(2, numInfo.currentValue); ASSERT_FALSE(numInfo.minimum || numInfo.maximum); ASSERT_EQ(info.intValue(), 2); std::stringstream ss; ss << info; ASSERT_EQ( ss.str(), "OptionInfo{ verbosity | set by user | int64_t | 2 | default 0 }"); } { // uint64 type with default cvc5::OptionInfo info = d_solver->getOptionInfo("rlimit"); ASSERT_EQ("rlimit", info.name); ASSERT_EQ(std::vector{}, info.aliases); ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON); ASSERT_FALSE(info.setByUser); ASSERT_TRUE(std::holds_alternative>( info.valueInfo)); auto numInfo = std::get>(info.valueInfo); ASSERT_EQ(0, numInfo.defaultValue); ASSERT_EQ(0, numInfo.currentValue); ASSERT_FALSE(numInfo.minimum || numInfo.maximum); ASSERT_EQ(info.uintValue(), 0); std::stringstream ss; ss << info; ASSERT_EQ(ss.str(), "OptionInfo{ rlimit | uint64_t | 0 | default 0 }"); } // string type { auto info = d_solver->getOptionInfo("random-freq"); ASSERT_EQ(info.name, "random-freq"); ASSERT_EQ(info.aliases, std::vector{"random-frequency"}); ASSERT_EQ(info.category, cvc5::modes::OptionCategory::EXPERT); ASSERT_FALSE(info.setByUser); ASSERT_TRUE(std::holds_alternative>( info.valueInfo)); auto ni = std::get>(info.valueInfo); ASSERT_EQ(ni.currentValue, 0.0); ASSERT_EQ(ni.defaultValue, 0.0); ASSERT_TRUE(ni.minimum && ni.maximum); ASSERT_EQ(*ni.minimum, 0.0); ASSERT_EQ(*ni.maximum, 1.0); ASSERT_EQ(info.doubleValue(), 0.0); std::stringstream ss; ss << info; ASSERT_EQ(ss.str(), "OptionInfo{ random-freq, random-frequency | double | 0 | " "default 0 | 0 <= x <= 1 }"); } { // string type with default cvc5::OptionInfo info = d_solver->getOptionInfo("force-logic"); ASSERT_EQ("force-logic", info.name); ASSERT_EQ(std::vector{}, info.aliases); ASSERT_EQ(info.category, cvc5::modes::OptionCategory::COMMON); ASSERT_FALSE(info.setByUser); ASSERT_TRUE(std::holds_alternative>( info.valueInfo)); auto valInfo = std::get>(info.valueInfo); ASSERT_EQ("", valInfo.defaultValue); ASSERT_EQ("", valInfo.currentValue); ASSERT_EQ(info.stringValue(), ""); std::stringstream ss; ss << info; ASSERT_EQ(ss.str(), "OptionInfo{ force-logic | string | \"\" | default \"\" }"); } { // mode option cvc5::OptionInfo info = d_solver->getOptionInfo("simplification"); ASSERT_EQ("simplification", info.name); ASSERT_EQ(std::vector{"simplification-mode"}, info.aliases); ASSERT_EQ(info.category, cvc5::modes::OptionCategory::REGULAR); ASSERT_FALSE(info.setByUser); ASSERT_TRUE(std::holds_alternative(info.valueInfo)); auto modeInfo = std::get(info.valueInfo); ASSERT_EQ("batch", modeInfo.defaultValue); ASSERT_EQ("batch", modeInfo.currentValue); ASSERT_EQ(2, modeInfo.modes.size()); ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "batch") != modeInfo.modes.end()); ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none") != modeInfo.modes.end()); std::stringstream ss; ss << info; ASSERT_EQ(ss.str(), "OptionInfo{ simplification, simplification-mode | mode | batch " "| default batch | modes: batch, none }"); } } TEST_F(TestApiBlackSolver, getUnsatAssumptions1) { d_solver->setOption("incremental", "false"); d_solver->checkSatAssuming(d_tm.mkFalse()); ASSERT_THROW(d_solver->getUnsatAssumptions(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatAssumptions2) { d_solver->setOption("incremental", "true"); d_solver->setOption("produce-unsat-assumptions", "false"); d_solver->checkSatAssuming(d_tm.mkFalse()); ASSERT_THROW(d_solver->getUnsatAssumptions(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatAssumptions3) { d_solver->setOption("incremental", "true"); d_solver->setOption("produce-unsat-assumptions", "true"); d_solver->checkSatAssuming(d_tm.mkFalse()); ASSERT_NO_THROW(d_solver->getUnsatAssumptions()); d_solver->checkSatAssuming(d_tm.mkTrue()); ASSERT_THROW(d_solver->getUnsatAssumptions(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatCore1) { d_solver->setOption("incremental", "false"); d_solver->assertFormula(d_tm.mkFalse()); d_solver->checkSat(); ASSERT_THROW(d_solver->getUnsatCore(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatCore2) { d_solver->setOption("incremental", "false"); d_solver->setOption("produce-unsat-cores", "false"); d_solver->assertFormula(d_tm.mkFalse()); d_solver->checkSat(); ASSERT_THROW(d_solver->getUnsatCore(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getUnsatCoreAndProof) { d_solver->setOption("incremental", "true"); d_solver->setOption("produce-unsat-cores", "true"); d_solver->setOption("produce-proofs", "true"); Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool); std::vector uc; Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term f = d_tm.mkConst(uToIntSort, "f"); Term p = d_tm.mkConst(intPredSort, "p"); Term zero = d_tm.mkInteger(0); Term one = d_tm.mkInteger(1); Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x}); Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y}); Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y}); Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero}); Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y}); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_x})); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_y})); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {sum, one})); d_solver->assertFormula(p_0); d_solver->assertFormula(p_f_y.notTerm()); ASSERT_TRUE(d_solver->checkSat().isUnsat()); ASSERT_NO_THROW(uc = d_solver->getUnsatCore()); ASSERT_FALSE(uc.empty()); ASSERT_NO_THROW(d_solver->getProof()); ASSERT_NO_THROW(d_solver->getProof(modes::ProofComponent::SAT)); d_solver->resetAssertions(); for (const auto& t : uc) { d_solver->assertFormula(t); } cvc5::Result res = d_solver->checkSat(); ASSERT_TRUE(res.isUnsat()); ASSERT_NO_THROW(d_solver->getProof()); } TEST_F(TestApiBlackSolver, getUnsatCoreLemmas1) { d_solver->setOption("produce-unsat-cores", "true"); d_solver->setOption("unsat-cores-mode", "sat-proof"); // cannot ask before a check sat ASSERT_THROW(d_solver->getUnsatCoreLemmas(), CVC5ApiException); d_solver->assertFormula(d_tm.mkFalse()); ASSERT_TRUE(d_solver->checkSat().isUnsat()); ASSERT_NO_THROW(d_solver->getUnsatCoreLemmas()); } TEST_F(TestApiBlackSolver, getUnsatCoreLemmas2) { d_solver->setOption("incremental", "true"); d_solver->setOption("produce-unsat-cores", "true"); d_solver->setOption("produce-proofs", "true"); Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool); Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term f = d_tm.mkConst(uToIntSort, "f"); Term p = d_tm.mkConst(intPredSort, "p"); Term zero = d_tm.mkInteger(0); Term one = d_tm.mkInteger(1); Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x}); Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y}); Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y}); Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero}); Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y}); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_x})); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_y})); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {sum, one})); d_solver->assertFormula(p_0); d_solver->assertFormula(p_f_y.notTerm()); ASSERT_TRUE(d_solver->checkSat().isUnsat()); ASSERT_NO_THROW(d_solver->getUnsatCoreLemmas()); } TEST_F(TestApiBlackSolver, getAbduct) { d_solver->setLogic("QF_LIA"); d_solver->setOption("produce-abducts", "true"); d_solver->setOption("incremental", "false"); Term zero = d_tm.mkInteger(0); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); // Assumptions for abduction: x > 0 d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {x, zero})); // Conjecture for abduction: y > 0 Term conj = d_tm.mkTerm(Kind::GT, {y, zero}); // Call the abduction api, while the resulting abduct is the output Term output = d_solver->getAbduct(conj); // We expect the resulting output to be a boolean formula ASSERT_TRUE(!output.isNull() && output.getSort().isBoolean()); // try with a grammar, a simple grammar admitting true Term truen = d_tm.mkBoolean(true); Term start = d_tm.mkVar(d_bool); Grammar g = d_solver->mkGrammar({}, {start}); Term conj2 = d_tm.mkTerm(Kind::GT, {x, zero}); ASSERT_THROW(d_solver->getAbduct(conj2, g), CVC5ApiException); ASSERT_NO_THROW(g.addRule(start, truen)); // Call the abduction api, while the resulting abduct is the output Term output2 = d_solver->getAbduct(conj2, g); // abduct must be true ASSERT_EQ(output2, truen); TermManager tm; Solver slv(tm); slv.setOption("produce-abducts", "true"); Sort intSort2 = tm.getIntegerSort(); Term xx = tm.mkConst(intSort2, "x"); Term yy = tm.mkConst(intSort2, "y"); Term zzero = tm.mkInteger(0); Term sstart = tm.mkVar(tm.getBooleanSort()); slv.assertFormula( tm.mkTerm(Kind::GT, {tm.mkTerm(Kind::ADD, {xx, yy}), zzero})); Grammar gg = slv.mkGrammar({}, {sstart}); gg.addRule(sstart, tm.mkTrue()); Term cconj2 = tm.mkTerm(Kind::EQUAL, {zzero, zzero}); ASSERT_NO_THROW(slv.getAbduct(cconj2, gg)); ASSERT_THROW(slv.getAbduct(conj2), CVC5ApiException); ASSERT_THROW(slv.getAbduct(conj2, gg), CVC5ApiException); ASSERT_THROW(slv.getAbduct(cconj2, g), CVC5ApiException); } TEST_F(TestApiBlackSolver, getAbduct2) { d_solver->setLogic("QF_LIA"); d_solver->setOption("incremental", "false"); Term zero = d_tm.mkInteger(0); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); // Assumptions for abduction: x > 0 d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {x, zero})); // Conjecture for abduction: y > 0 Term conj = d_tm.mkTerm(Kind::GT, {y, zero}); // Fails due to option not set ASSERT_THROW(d_solver->getAbduct(conj), CVC5ApiException); } TEST_F(TestApiBlackSolver, getAbductNext) { d_solver->setLogic("QF_LIA"); d_solver->setOption("produce-abducts", "true"); d_solver->setOption("incremental", "true"); Term zero = d_tm.mkInteger(0); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); // Assumptions for abduction: x > 0 d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {x, zero})); // Conjecture for abduction: y > 0 Term conj = d_tm.mkTerm(Kind::GT, {y, zero}); // Call the abduction api, while the resulting abduct is the output Term output = d_solver->getAbduct(conj); Term output2 = d_solver->getAbductNext(); // should produce a different output ASSERT_TRUE(output != output2); } TEST_F(TestApiBlackSolver, getInterpolant) { d_solver->setLogic("QF_LIA"); d_solver->setOption("produce-interpolants", "true"); d_solver->setOption("incremental", "false"); Term zero = d_tm.mkInteger(0); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); Term z = d_tm.mkConst(d_int, "z"); // Assumptions for interpolation: x + y > 0 /\ x < 0 d_solver->assertFormula( d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {x, y}), zero})); d_solver->assertFormula(d_tm.mkTerm(Kind::LT, {x, zero})); // Conjecture for interpolation: y + z > 0 \/ z < 0 Term conj = d_tm.mkTerm( Kind::OR, {d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {y, z}), zero}), d_tm.mkTerm(Kind::LT, {z, zero})}); // Call the interpolation api, while the resulting interpolant is the output Term output = d_solver->getInterpolant(conj); // We expect the resulting output to be a boolean formula ASSERT_TRUE(output.getSort().isBoolean()); // try with a grammar, a simple grammar admitting true Term truen = d_tm.mkBoolean(true); Term start = d_tm.mkVar(d_bool); Grammar g = d_solver->mkGrammar({}, {start}); Term conj2 = d_tm.mkTerm(Kind::EQUAL, {zero, zero}); ASSERT_THROW(d_solver->getInterpolant(conj2, g), CVC5ApiException); ASSERT_NO_THROW(g.addRule(start, truen)); // Call the interpolation api, while the resulting interpolant is the output Term output2 = d_solver->getInterpolant(conj2, g); // interpolant must be true ASSERT_EQ(output2, truen); TermManager tm; Solver slv(tm); slv.setOption("produce-interpolants", "true"); Term zzero = tm.mkInteger(0); Term sstart = tm.mkVar(tm.getBooleanSort()); Grammar gg = slv.mkGrammar({}, {sstart}); gg.addRule(sstart, tm.mkTrue()); Term cconj2 = tm.mkTerm(Kind::EQUAL, {zzero, zzero}); ASSERT_NO_THROW(slv.getInterpolant(cconj2, gg)); ASSERT_THROW(slv.getInterpolant(conj2), CVC5ApiException); ASSERT_THROW(slv.getInterpolant(conj2, gg), CVC5ApiException); ASSERT_THROW(slv.getInterpolant(cconj2, g), CVC5ApiException); } TEST_F(TestApiBlackSolver, getInterpolantNext) { d_solver->setLogic("QF_LIA"); d_solver->setOption("produce-interpolants", "true"); d_solver->setOption("incremental", "true"); Term zero = d_tm.mkInteger(0); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); Term z = d_tm.mkConst(d_int, "z"); // Assumptions for interpolation: x + y > 0 /\ x < 0 d_solver->assertFormula( d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {x, y}), zero})); d_solver->assertFormula(d_tm.mkTerm(Kind::LT, {x, zero})); // Conjecture for interpolation: y + z > 0 \/ z < 0 Term conj = d_tm.mkTerm( Kind::OR, {d_tm.mkTerm(Kind::GT, {d_tm.mkTerm(Kind::ADD, {y, z}), zero}), d_tm.mkTerm(Kind::LT, {z, zero})}); Term output = d_solver->getInterpolant(conj); Term output2 = d_solver->getInterpolantNext(); // We expect the next output to be distinct ASSERT_TRUE(output != output2); } TEST_F(TestApiBlackSolver, declarePool) { Sort setSort = d_tm.mkSetSort(d_int); Term zero = d_tm.mkInteger(0); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); // declare a pool with initial value { 0, x, y } Term p = d_solver->declarePool("p", d_int, {zero, x, y}); // pool should have the same sort ASSERT_TRUE(p.getSort() == setSort); // cannot pass null sort Sort nullSort; ASSERT_THROW(d_solver->declarePool("i", nullSort, {}), CVC5ApiException); TermManager tm; Solver slv(tm); Sort tm_int = tm.getIntegerSort(); Term tm_zero = tm.mkInteger(0); Term tm_x = tm.mkConst(tm_int, "x"); Term tm_y = tm.mkConst(tm_int, "y"); ASSERT_THROW(slv.declarePool("p", d_int, {tm_zero, tm_x, tm_y}), CVC5ApiException); ASSERT_THROW(slv.declarePool("p", tm_int, {zero, tm_x, tm_y}), CVC5ApiException); ASSERT_THROW(slv.declarePool("p", tm_int, {tm_zero, x, tm_y}), CVC5ApiException); ASSERT_THROW(slv.declarePool("p", tm_int, {tm_zero, tm_x, y}), CVC5ApiException); } TEST_F(TestApiBlackSolver, getDriverOptions) { auto dopts = d_solver->getDriverOptions(); ASSERT_EQ(dopts.err().rdbuf(), std::cerr.rdbuf()); ASSERT_EQ(dopts.in().rdbuf(), std::cin.rdbuf()); ASSERT_EQ(dopts.out().rdbuf(), std::cout.rdbuf()); } TEST_F(TestApiBlackSolver, getStatistics) { ASSERT_NO_THROW(cvc5::Stat()); // do some array reasoning to make sure we have statistics { Sort s2 = d_tm.mkArraySort(d_int, d_int); Term t1 = d_tm.mkConst(d_int, "i"); Term t2 = d_tm.mkConst(s2, "a"); Term t3 = d_tm.mkTerm(Kind::SELECT, {t2, t1}); d_solver->assertFormula(t3.eqTerm(t1)); d_solver->checkSat(); } cvc5::Statistics stats = d_solver->getStatistics(); std::stringstream ss; ss << stats; { auto s = stats.get("global::totalTime"); ASSERT_FALSE(s.isInternal()); ASSERT_FALSE(s.isDefault()); ASSERT_TRUE(s.isString()); std::string time = s.getString(); ASSERT_TRUE(time.rfind("ms") == time.size() - 2); // ends with "ms" ASSERT_FALSE(s.isDouble()); ss << s << s.toString(); s = stats.get("resource::resourceUnitsUsed"); ASSERT_TRUE(s.isInternal()); ASSERT_FALSE(s.isDefault()); ASSERT_TRUE(s.isInt()); ASSERT_TRUE(s.getInt() >= 0); ss << s << s.toString(); } bool hasstats = false; for (const auto& s : stats) { hasstats = true; ASSERT_FALSE(s.first.empty()); } ASSERT_TRUE(hasstats); hasstats = false; for (auto it = stats.begin(true, true); it != stats.end(); ++it) { hasstats = true; { auto tmp1 = it, tmp2 = it; ++tmp1; tmp2++; ASSERT_EQ(tmp1, tmp2); --tmp1; tmp2--; ASSERT_EQ(tmp1, tmp2); ASSERT_EQ(tmp1, it); ASSERT_EQ(it, tmp2); } const auto& s = *it; // check some basic utility methods ASSERT_TRUE(!(it == stats.end())); ASSERT_EQ(s.first, it->first); if (s.first == "theory::arrays::avgIndexListLength") { ASSERT_TRUE(s.second.isInternal()); ASSERT_TRUE(s.second.isDouble()); ASSERT_TRUE(std::isnan(s.second.getDouble())); } } ASSERT_TRUE(hasstats); } TEST_F(TestApiBlackSolver, printStatisticsSafe) { // do some array reasoning to make sure we have statistics { Sort s2 = d_tm.mkArraySort(d_int, d_int); Term t1 = d_tm.mkConst(d_int, "i"); Term t2 = d_tm.mkConst(s2, "a"); Term t3 = d_tm.mkTerm(Kind::SELECT, {t2, t1}); d_solver->assertFormula(t3.eqTerm(t1)); d_solver->checkSat(); } testing::internal::CaptureStdout(); d_solver->printStatisticsSafe(STDOUT_FILENO); testing::internal::GetCapturedStdout(); } TEST_F(TestApiBlackSolver, getProofAndProofToString) { d_solver->setOption("produce-proofs", "true"); Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool); std::vector proofs; Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term f = d_tm.mkConst(uToIntSort, "f"); Term p = d_tm.mkConst(intPredSort, "p"); Term zero = d_tm.mkInteger(0); Term one = d_tm.mkInteger(1); Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x}); Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y}); Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y}); Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero}); Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y}); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_x})); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {zero, f_y})); d_solver->assertFormula(d_tm.mkTerm(Kind::GT, {sum, one})); d_solver->assertFormula(p_0); d_solver->assertFormula(p_f_y.notTerm()); ASSERT_TRUE(d_solver->checkSat().isUnsat()); std::string printedProof; ASSERT_NO_THROW(proofs = d_solver->getProof()); ASSERT_FALSE(proofs.empty()); ASSERT_NO_THROW(printedProof = d_solver->proofToString(proofs[0])); ASSERT_FALSE(printedProof.empty()); ASSERT_NO_THROW(printedProof = d_solver->proofToString( proofs[0], modes::ProofFormat::ALETHE)); ASSERT_FALSE(printedProof.empty()); ASSERT_NO_THROW(proofs = d_solver->getProof(modes::ProofComponent::SAT)); ASSERT_NO_THROW(printedProof = d_solver->proofToString( proofs[0], modes::ProofFormat::NONE)); ASSERT_FALSE(printedProof.empty()); } TEST_F(TestApiBlackSolver, proofToStringAssertionNames) { d_solver->setOption("produce-proofs", "true"); std::vector proofs; Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term x_eq_y = d_tm.mkTerm(Kind::EQUAL, {x, y}); Term not_x_eq_y = d_tm.mkTerm(Kind::NOT, {x_eq_y}); std::map assertionNames; assertionNames.emplace(x_eq_y, "as1"); assertionNames.emplace(not_x_eq_y, "as2"); d_solver->assertFormula(x_eq_y); d_solver->assertFormula(not_x_eq_y); ASSERT_TRUE(d_solver->checkSat().isUnsat()); std::string printedProof; ASSERT_NO_THROW(proofs = d_solver->getProof()); ASSERT_FALSE(proofs.empty()); ASSERT_NO_THROW(printedProof = d_solver->proofToString( proofs[0], modes::ProofFormat::ALETHE, assertionNames)); ASSERT_FALSE(printedProof.empty()); ASSERT_LT(printedProof.find("as1"), std::string::npos); ASSERT_LT(printedProof.find("as2"), std::string::npos); } TEST_F(TestApiBlackSolver, getDifficulty) { d_solver->setOption("produce-difficulty", "true"); // cannot ask before a check sat ASSERT_THROW(d_solver->getDifficulty(), CVC5ApiException); d_solver->checkSat(); ASSERT_NO_THROW(d_solver->getDifficulty()); } TEST_F(TestApiBlackSolver, getDifficulty2) { d_solver->checkSat(); // option is not set ASSERT_THROW(d_solver->getDifficulty(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getDifficulty3) { d_solver->setOption("produce-difficulty", "true"); Term x = d_tm.mkConst(d_int, "x"); Term zero = d_tm.mkInteger(0); Term ten = d_tm.mkInteger(10); Term f0 = d_tm.mkTerm(Kind::GEQ, {x, ten}); Term f1 = d_tm.mkTerm(Kind::GEQ, {zero, x}); d_solver->assertFormula(f0); d_solver->assertFormula(f1); d_solver->checkSat(); std::map dmap; ASSERT_NO_THROW(dmap = d_solver->getDifficulty()); // difficulty should map assertions to integer values for (const std::pair& t : dmap) { ASSERT_TRUE(t.first == f0 || t.first == f1); ASSERT_TRUE(t.second.getKind() == Kind::CONST_INTEGER); } } TEST_F(TestApiBlackSolver, getLearnedLiterals) { d_solver->setOption("produce-learned-literals", "true"); // cannot ask before a check sat ASSERT_THROW(d_solver->getLearnedLiterals(), CVC5ApiException); d_solver->checkSat(); ASSERT_NO_THROW(d_solver->getLearnedLiterals()); ASSERT_NO_THROW( d_solver->getLearnedLiterals(modes::LearnedLitType::PREPROCESS)); } TEST_F(TestApiBlackSolver, getLearnedLiterals2) { d_solver->setOption("produce-learned-literals", "true"); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); Term zero = d_tm.mkInteger(0); Term ten = d_tm.mkInteger(10); Term f0 = d_tm.mkTerm(Kind::GEQ, {x, ten}); Term f1 = d_tm.mkTerm( Kind::OR, {d_tm.mkTerm(Kind::GEQ, {zero, x}), d_tm.mkTerm(Kind::GEQ, {y, zero})}); d_solver->assertFormula(f0); d_solver->assertFormula(f1); d_solver->checkSat(); ASSERT_NO_THROW(d_solver->getLearnedLiterals()); } TEST_F(TestApiBlackSolver, getTimeoutCore) { d_solver->setOption("timeout-core-timeout", "100"); d_solver->setOption("produce-unsat-cores", "true"); Term x = d_tm.mkConst(d_int, "x"); Term tt = d_tm.mkBoolean(true); Term hard = d_tm.mkTerm(Kind::EQUAL, {d_tm.mkTerm(Kind::MULT, {x, x}), d_tm.mkInteger("501240912901901249014210220059591")}); d_solver->assertFormula(tt); d_solver->assertFormula(hard); std::pair> res = d_solver->getTimeoutCore(); ASSERT_TRUE(res.first.isUnknown()); ASSERT_TRUE(res.second.size() == 1); ASSERT_EQ(res.second[0], hard); } TEST_F(TestApiBlackSolver, getTimeoutCoreUnsat) { d_solver->setOption("produce-unsat-cores", "true"); Term ff = d_tm.mkBoolean(false); Term tt = d_tm.mkBoolean(true); d_solver->assertFormula(tt); d_solver->assertFormula(ff); d_solver->assertFormula(tt); std::pair> res = d_solver->getTimeoutCore(); ASSERT_TRUE(res.first.isUnsat()); ASSERT_TRUE(res.second.size() == 1); ASSERT_EQ(res.second[0], ff); } TEST_F(TestApiBlackSolver, getTimeoutCoreAssuming) { d_solver->setOption("produce-unsat-cores", "true"); Term ff = d_tm.mkBoolean(false); Term tt = d_tm.mkBoolean(true); d_solver->assertFormula(tt); std::pair> res = d_solver->getTimeoutCoreAssuming({ff, tt}); ASSERT_TRUE(res.first.isUnsat()); ASSERT_TRUE(res.second.size() == 1); ASSERT_EQ(res.second[0], ff); } TEST_F(TestApiBlackSolver, getTimeoutCoreAssumingEmpty) { d_solver->setOption("produce-unsat-cores", "true"); ASSERT_THROW(d_solver->getTimeoutCoreAssuming({}), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValue1) { d_solver->setOption("produce-models", "false"); Term t = d_tm.mkTrue(); d_solver->assertFormula(t); d_solver->checkSat(); ASSERT_THROW(d_solver->getValue(t), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValue2) { d_solver->setOption("produce-models", "true"); Term t = d_tm.mkFalse(); d_solver->assertFormula(t); d_solver->checkSat(); ASSERT_THROW(d_solver->getValue(t), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValue3) { d_solver->setOption("produce-models", "true"); Sort uToIntSort = d_tm.mkFunctionSort({d_uninterpreted}, d_int); Sort intPredSort = d_tm.mkFunctionSort({d_int}, d_bool); std::vector unsat_core; Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term z = d_tm.mkConst(d_uninterpreted, "z"); Term f = d_tm.mkConst(uToIntSort, "f"); Term p = d_tm.mkConst(intPredSort, "p"); Term zero = d_tm.mkInteger(0); Term one = d_tm.mkInteger(1); Term f_x = d_tm.mkTerm(Kind::APPLY_UF, {f, x}); Term f_y = d_tm.mkTerm(Kind::APPLY_UF, {f, y}); Term sum = d_tm.mkTerm(Kind::ADD, {f_x, f_y}); Term p_0 = d_tm.mkTerm(Kind::APPLY_UF, {p, zero}); Term p_f_y = d_tm.mkTerm(Kind::APPLY_UF, {p, f_y}); d_solver->assertFormula(d_tm.mkTerm(Kind::LEQ, {zero, f_x})); d_solver->assertFormula(d_tm.mkTerm(Kind::LEQ, {zero, f_y})); d_solver->assertFormula(d_tm.mkTerm(Kind::LEQ, {sum, one})); d_solver->assertFormula(p_0.notTerm()); d_solver->assertFormula(p_f_y); ASSERT_TRUE(d_solver->checkSat().isSat()); ASSERT_NO_THROW(d_solver->getValue(x)); ASSERT_NO_THROW(d_solver->getValue(y)); ASSERT_NO_THROW(d_solver->getValue(z)); ASSERT_NO_THROW(d_solver->getValue(sum)); ASSERT_NO_THROW(d_solver->getValue(p_f_y)); std::vector a; ASSERT_NO_THROW(a.emplace_back(d_solver->getValue(x))); ASSERT_NO_THROW(a.emplace_back(d_solver->getValue(y))); ASSERT_NO_THROW(a.emplace_back(d_solver->getValue(z))); std::vector b; ASSERT_NO_THROW(b = d_solver->getValue({x, y, z})); ASSERT_EQ(a, b); ASSERT_THROW(Solver(d_tm).getValue(x), CVC5ApiException); { Solver slv(d_tm); slv.setOption("produce-models", "true"); ASSERT_THROW(slv.getValue(x), CVC5ApiException); } { Solver slv(d_tm); slv.setOption("produce-models", "true"); slv.checkSat(); ASSERT_NO_THROW(slv.getValue(x)); } TermManager tm; Solver slv(tm); slv.setOption("produce-models", "true"); slv.checkSat(); ASSERT_THROW(slv.getValue(d_tm.mkConst(d_bool, "x")), CVC5ApiException); } TEST_F(TestApiBlackSolver, getModelDomainElements) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term z = d_tm.mkConst(d_uninterpreted, "z"); Term f = d_tm.mkTerm(Kind::DISTINCT, {x, y, z}); d_solver->assertFormula(f); d_solver->checkSat(); auto elems = d_solver->getModelDomainElements(d_uninterpreted); ASSERT_TRUE(elems.size() >= 3); ASSERT_THROW(d_solver->getModelDomainElements(d_int), CVC5ApiException); TermManager tm; Solver slv(tm); slv.setOption("produce-models", "true"); slv.checkSat(); ASSERT_THROW(slv.getModelDomainElements(d_uninterpreted), CVC5ApiException); } TEST_F(TestApiBlackSolver, getModelDomainElements2) { d_solver->setOption("produce-models", "true"); d_solver->setOption("finite-model-find", "true"); Term x = d_tm.mkVar(d_uninterpreted, "x"); Term y = d_tm.mkVar(d_uninterpreted, "y"); Term eq = d_tm.mkTerm(Kind::EQUAL, {x, y}); Term bvl = d_tm.mkTerm(Kind::VARIABLE_LIST, {x, y}); Term f = d_tm.mkTerm(Kind::FORALL, {bvl, eq}); d_solver->assertFormula(f); d_solver->checkSat(); auto elems = d_solver->getModelDomainElements(d_uninterpreted); // a model for the above must interpret u as size 1 ASSERT_TRUE(elems.size() == 1); } TEST_F(TestApiBlackSolver, isModelCoreSymbol) { d_solver->setOption("produce-models", "true"); d_solver->setOption("model-cores", "simple"); Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term z = d_tm.mkConst(d_uninterpreted, "z"); Term zero = d_tm.mkInteger(0); Term f = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::EQUAL, {x, y})}); d_solver->assertFormula(f); d_solver->checkSat(); ASSERT_TRUE(d_solver->isModelCoreSymbol(x)); ASSERT_TRUE(d_solver->isModelCoreSymbol(y)); ASSERT_FALSE(d_solver->isModelCoreSymbol(z)); ASSERT_THROW(d_solver->isModelCoreSymbol(zero), CVC5ApiException); TermManager tm; Solver slv(tm); slv.setOption("produce-models", "true"); slv.checkSat(); ASSERT_THROW(slv.isModelCoreSymbol(d_tm.mkConst(d_uninterpreted, "x")), CVC5ApiException); } TEST_F(TestApiBlackSolver, getModel) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_uninterpreted, "x"); Term y = d_tm.mkConst(d_uninterpreted, "y"); Term z = d_tm.mkConst(d_uninterpreted, "z"); Term f = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::EQUAL, {x, y})}); d_solver->assertFormula(f); d_solver->checkSat(); std::vector sorts{d_uninterpreted}; std::vector terms{x, y}; ASSERT_NO_THROW(d_solver->getModel(sorts, terms)); Term null; terms.push_back(null); ASSERT_THROW(d_solver->getModel(sorts, terms), CVC5ApiException); } TEST_F(TestApiBlackSolver, getModel2) { d_solver->setOption("produce-models", "true"); std::vector sorts; std::vector terms; ASSERT_THROW(d_solver->getModel(sorts, terms), CVC5ApiException); } TEST_F(TestApiBlackSolver, getModel3) { d_solver->setOption("produce-models", "true"); std::vector sorts; std::vector terms; d_solver->checkSat(); ASSERT_NO_THROW(d_solver->getModel(sorts, terms)); sorts.push_back(d_int); ASSERT_THROW(d_solver->getModel(sorts, terms), CVC5ApiException); } TEST_F(TestApiBlackSolver, getQuantifierElimination) { Term x = d_tm.mkVar(d_bool, "x"); Term forall = d_tm.mkTerm(Kind::FORALL, {d_tm.mkTerm(Kind::VARIABLE_LIST, {x}), d_tm.mkTerm(Kind::OR, {x, d_tm.mkTerm(Kind::NOT, {x})})}); ASSERT_THROW(d_solver->getQuantifierElimination(Term()), CVC5ApiException); ASSERT_THROW(d_solver->getQuantifierElimination(d_tm.mkBoolean(false)), CVC5ApiException); ASSERT_NO_THROW(d_solver->getQuantifierElimination(forall)); TermManager tm; Solver slv(tm); slv.checkSat(); ASSERT_THROW(slv.getQuantifierElimination(forall), CVC5ApiException); } TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct) { Term x = d_tm.mkVar(d_bool, "x"); Term forall = d_tm.mkTerm(Kind::FORALL, {d_tm.mkTerm(Kind::VARIABLE_LIST, {x}), d_tm.mkTerm(Kind::OR, {x, d_tm.mkTerm(Kind::NOT, {x})})}); ASSERT_THROW(d_solver->getQuantifierEliminationDisjunct(Term()), CVC5ApiException); ASSERT_THROW( d_solver->getQuantifierEliminationDisjunct(d_tm.mkBoolean(false)), CVC5ApiException); ASSERT_NO_THROW(d_solver->getQuantifierEliminationDisjunct(forall)); TermManager tm; Solver slv(tm); slv.checkSat(); ASSERT_THROW(slv.getQuantifierEliminationDisjunct(forall), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareSepHeap) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); ASSERT_NO_THROW(d_solver->declareSepHeap(d_int, d_int)); // cannot declare separation logic heap more than once ASSERT_THROW(d_solver->declareSepHeap(d_int, d_int), CVC5ApiException); TermManager tm; { Solver slv(tm); // no logic set yet ASSERT_THROW(slv.declareSepHeap(tm.getIntegerSort(), tm.getIntegerSort()), CVC5ApiException); } { Solver slv(tm); slv.setLogic("ALL"); ASSERT_THROW(slv.declareSepHeap(d_int, tm.getRealSort()), CVC5ApiException); } { Solver slv(tm); slv.setLogic("ALL"); ASSERT_THROW(slv.declareSepHeap(tm.getBooleanSort(), d_int), CVC5ApiException); } } namespace { /** * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks * some simple separation logic constraints. */ void checkSimpleSeparationConstraints(Solver* solver) { TermManager& tm = solver->getTermManager(); Sort integer = tm.getIntegerSort(); // declare the separation heap solver->declareSepHeap(integer, integer); Term x = tm.mkConst(integer, "x"); Term p = tm.mkConst(integer, "p"); Term heap = tm.mkTerm(cvc5::Kind::SEP_PTO, {p, x}); solver->assertFormula(heap); Term nil = tm.mkSepNil(integer); solver->assertFormula(nil.eqTerm(tm.mkInteger(5))); solver->checkSat(); } } // namespace TEST_F(TestApiBlackSolver, getValueSepHeap1) { d_solver->setLogic("QF_BV"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); Term t = d_tm.mkTrue(); d_solver->assertFormula(t); ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepHeap2) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "false"); checkSimpleSeparationConstraints(d_solver.get()); ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepHeap3) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); Term t = d_tm.mkFalse(); d_solver->assertFormula(t); d_solver->checkSat(); ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepHeap4) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); Term t = d_tm.mkTrue(); d_solver->assertFormula(t); d_solver->checkSat(); ASSERT_THROW(d_solver->getValueSepHeap(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepHeap5) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); checkSimpleSeparationConstraints(d_solver.get()); ASSERT_NO_THROW(d_solver->getValueSepHeap()); } TEST_F(TestApiBlackSolver, getValueSepNil1) { d_solver->setLogic("QF_BV"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); Term t = d_tm.mkTrue(); d_solver->assertFormula(t); ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepNil2) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "false"); checkSimpleSeparationConstraints(d_solver.get()); ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepNil3) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); Term t = d_tm.mkFalse(); d_solver->assertFormula(t); d_solver->checkSat(); ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepNil4) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); Term t = d_tm.mkTrue(); d_solver->assertFormula(t); d_solver->checkSat(); ASSERT_THROW(d_solver->getValueSepNil(), CVC5ApiException); } TEST_F(TestApiBlackSolver, getValueSepNil5) { d_solver->setLogic("ALL"); d_solver->setOption("incremental", "false"); d_solver->setOption("produce-models", "true"); checkSimpleSeparationConstraints(d_solver.get()); ASSERT_NO_THROW(d_solver->getValueSepNil()); } TEST_F(TestApiBlackSolver, push1) { d_solver->setOption("incremental", "true"); ASSERT_NO_THROW(d_solver->push(1)); ASSERT_THROW(d_solver->setOption("incremental", "false"), CVC5ApiException); ASSERT_THROW(d_solver->setOption("incremental", "true"), CVC5ApiException); } TEST_F(TestApiBlackSolver, push2) { d_solver->setOption("incremental", "false"); ASSERT_THROW(d_solver->push(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, pop1) { d_solver->setOption("incremental", "false"); ASSERT_THROW(d_solver->pop(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, pop2) { d_solver->setOption("incremental", "true"); ASSERT_THROW(d_solver->pop(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, pop3) { d_solver->setOption("incremental", "true"); ASSERT_NO_THROW(d_solver->push(1)); ASSERT_NO_THROW(d_solver->pop(1)); ASSERT_THROW(d_solver->pop(1), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel1) { Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); d_solver->checkSat(); ASSERT_THROW(d_solver->blockModel(modes::BlockModelsMode::LITERALS), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel2) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); ASSERT_THROW(d_solver->blockModel(modes::BlockModelsMode::LITERALS), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModel3) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); d_solver->checkSat(); ASSERT_NO_THROW(d_solver->blockModel(modes::BlockModelsMode::LITERALS)); } TEST_F(TestApiBlackSolver, blockModelValues1) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); d_solver->checkSat(); ASSERT_THROW(d_solver->blockModelValues({}), CVC5ApiException); ASSERT_THROW(d_solver->blockModelValues({Term()}), CVC5ApiException); ASSERT_NO_THROW(d_solver->blockModelValues({d_tm.mkBoolean(false)})); TermManager tm; Solver slv(tm); slv.setOption("produce-models", "true"); slv.checkSat(); ASSERT_THROW(slv.blockModelValues({d_tm.mkFalse()}), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModelValues2) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); d_solver->checkSat(); ASSERT_NO_THROW(d_solver->blockModelValues({x})); } TEST_F(TestApiBlackSolver, blockModelValues3) { Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); d_solver->checkSat(); ASSERT_THROW(d_solver->blockModelValues({x}), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModelValues4) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); ASSERT_THROW(d_solver->blockModelValues({x}), CVC5ApiException); } TEST_F(TestApiBlackSolver, blockModelValues5) { d_solver->setOption("produce-models", "true"); Term x = d_tm.mkConst(d_bool, "x"); d_solver->assertFormula(x.eqTerm(x)); d_solver->checkSat(); ASSERT_NO_THROW(d_solver->blockModelValues({x})); } TEST_F(TestApiBlackSolver, getInstantiations) { Term p = d_solver->declareFun("p", {d_int}, d_bool); Term x = d_tm.mkVar(d_int, "x"); Term bvl = d_tm.mkTerm(Kind::VARIABLE_LIST, {x}); Term app = d_tm.mkTerm(Kind::APPLY_UF, {p, x}); Term q = d_tm.mkTerm(Kind::FORALL, {bvl, app}); d_solver->assertFormula(q); Term five = d_tm.mkInteger(5); Term app2 = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::APPLY_UF, {p, five})}); d_solver->assertFormula(app2); ASSERT_THROW(d_solver->getInstantiations(), CVC5ApiException); d_solver->checkSat(); ASSERT_NO_THROW(d_solver->getInstantiations()); } TEST_F(TestApiBlackSolver, setInfo) { ASSERT_THROW(d_solver->setInfo("cvc5-lagic", "QF_BV"), CVC5ApiException); ASSERT_THROW(d_solver->setInfo("cvc2-logic", "QF_BV"), CVC5ApiException); ASSERT_THROW(d_solver->setInfo("cvc5-logic", "asdf"), CVC5ApiException); ASSERT_NO_THROW(d_solver->setInfo("source", "asdf")); ASSERT_NO_THROW(d_solver->setInfo("category", "asdf")); ASSERT_NO_THROW(d_solver->setInfo("difficulty", "asdf")); ASSERT_NO_THROW(d_solver->setInfo("filename", "asdf")); ASSERT_NO_THROW(d_solver->setInfo("license", "asdf")); ASSERT_NO_THROW(d_solver->setInfo("name", "asdf")); ASSERT_NO_THROW(d_solver->setInfo("notes", "asdf")); ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2")); ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2.0")); ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2.5")); ASSERT_NO_THROW(d_solver->setInfo("smt-lib-version", "2.6")); ASSERT_THROW(d_solver->setInfo("smt-lib-version", ".0"), CVC5ApiException); ASSERT_NO_THROW(d_solver->setInfo("status", "sat")); ASSERT_NO_THROW(d_solver->setInfo("status", "unsat")); ASSERT_NO_THROW(d_solver->setInfo("status", "unknown")); ASSERT_THROW(d_solver->setInfo("status", "asdf"), CVC5ApiException); } TEST_F(TestApiBlackSolver, setLogic) { ASSERT_NO_THROW(d_solver->setLogic("AUFLIRA")); ASSERT_THROW(d_solver->setLogic("AF_BV"), CVC5ApiException); d_solver->assertFormula(d_tm.mkTrue()); ASSERT_THROW(d_solver->setLogic("AUFLIRA"), CVC5ApiException); } TEST_F(TestApiBlackSolver, isLogicSet) { ASSERT_FALSE(d_solver->isLogicSet()); ASSERT_NO_THROW(d_solver->setLogic("QF_BV")); ASSERT_TRUE(d_solver->isLogicSet()); } TEST_F(TestApiBlackSolver, getLogic) { ASSERT_THROW(d_solver->getLogic(), CVC5ApiException); ASSERT_NO_THROW(d_solver->setLogic("QF_BV")); ASSERT_EQ(d_solver->getLogic(), "QF_BV"); } TEST_F(TestApiBlackSolver, setOption) { ASSERT_NO_THROW(d_solver->setOption("bv-sat-solver", "minisat")); ASSERT_THROW(d_solver->setOption("bv-sat-solver", "1"), CVC5ApiException); d_solver->assertFormula(d_tm.mkTrue()); ASSERT_THROW(d_solver->setOption("bv-sat-solver", "minisat"), CVC5ApiException); } TEST_F(TestApiBlackSolver, resetAssertions) { d_solver->setOption("incremental", "true"); Sort bvSort = d_tm.mkBitVectorSort(4); Term one = d_tm.mkBitVector(4, 1); Term x = d_tm.mkConst(bvSort, "x"); Term ule = d_tm.mkTerm(Kind::BITVECTOR_ULE, {x, one}); Term srem = d_tm.mkTerm(Kind::BITVECTOR_SREM, {one, x}); d_solver->push(4); Term slt = d_tm.mkTerm(Kind::BITVECTOR_SLT, {srem, one}); d_solver->resetAssertions(); d_solver->checkSatAssuming({slt, ule}); } TEST_F(TestApiBlackSolver, declareSygusVar) { d_solver->setOption("sygus", "true"); Sort funSort = d_tm.mkFunctionSort({d_int}, d_bool); ASSERT_NO_THROW(d_solver->declareSygusVar("", d_bool)); ASSERT_NO_THROW(d_solver->declareSygusVar("", funSort)); ASSERT_NO_THROW(d_solver->declareSygusVar(std::string("b"), d_bool)); ASSERT_THROW(d_solver->declareSygusVar("", Sort()), CVC5ApiException); ASSERT_THROW(d_solver->declareSygusVar("a", Sort()), CVC5ApiException); ASSERT_THROW(Solver(d_tm).declareSygusVar("", d_bool), CVC5ApiException); TermManager tm; Solver slv(tm); slv.setOption("sygus", "true"); ASSERT_THROW(slv.declareSygusVar("", d_bool), CVC5ApiException); } TEST_F(TestApiBlackSolver, mkGrammar) { Term nullTerm; Term boolTerm = d_tm.mkBoolean(true); Term boolVar = d_tm.mkVar(d_bool); Term intVar = d_tm.mkVar(d_int); ASSERT_NO_THROW(d_solver->mkGrammar({}, {intVar})); ASSERT_NO_THROW(d_solver->mkGrammar({boolVar}, {intVar})); ASSERT_THROW(d_solver->mkGrammar({}, {}), CVC5ApiException); ASSERT_THROW(d_solver->mkGrammar({}, {nullTerm}), CVC5ApiException); ASSERT_THROW(d_solver->mkGrammar({}, {boolTerm}), CVC5ApiException); ASSERT_THROW(d_solver->mkGrammar({boolTerm}, {intVar}), CVC5ApiException); TermManager tm; Solver slv(tm); Term boolVar2 = tm.mkVar(tm.getBooleanSort()); Term intVar2 = tm.mkVar(tm.getIntegerSort()); ASSERT_NO_THROW(slv.mkGrammar({boolVar2}, {intVar2})); ASSERT_THROW(slv.mkGrammar({boolVar}, {intVar2}), CVC5ApiException); ASSERT_THROW(slv.mkGrammar({boolVar2}, {intVar}), CVC5ApiException); } TEST_F(TestApiBlackSolver, synthFun) { d_solver->setOption("sygus", "true"); Sort null; Term nullTerm; Term x = d_tm.mkVar(d_bool); Term start1 = d_tm.mkVar(d_bool); Term start2 = d_tm.mkVar(d_int); Grammar g1 = d_solver->mkGrammar({x}, {start1}); ASSERT_NO_THROW(d_solver->synthFun("", {}, d_bool)); ASSERT_NO_THROW(d_solver->synthFun("f1", {x}, d_bool)); ASSERT_THROW(d_solver->synthFun("f2", {x}, d_bool, g1), CVC5ApiException); g1.addRule(start1, d_tm.mkBoolean(false)); Grammar g2 = d_solver->mkGrammar({x}, {start2}); g2.addRule(start2, d_tm.mkInteger(0)); ASSERT_NO_THROW(d_solver->synthFun("", {}, d_bool)); ASSERT_NO_THROW(d_solver->synthFun("f1", {x}, d_bool)); ASSERT_NO_THROW(d_solver->synthFun("f2", {x}, d_bool, g1)); ASSERT_THROW(d_solver->synthFun("f3", {nullTerm}, d_bool), CVC5ApiException); ASSERT_THROW(d_solver->synthFun("f4", {}, null), CVC5ApiException); ASSERT_THROW(d_solver->synthFun("f6", {x}, d_bool, g2), CVC5ApiException); TermManager tm; Solver slv(tm); slv.setOption("sygus", "true"); Term x2 = tm.mkVar(tm.getBooleanSort()); ASSERT_THROW(slv.synthFun("f1", {x2}, d_bool), CVC5ApiException); ASSERT_THROW(slv.synthFun("", {}, d_bool), CVC5ApiException); ASSERT_THROW(slv.synthFun("f1", {x}, tm.getBooleanSort()), CVC5ApiException); } TEST_F(TestApiBlackSolver, addSygusConstraint) { d_solver->setOption("sygus", "true"); Term nullTerm; Term boolTerm = d_tm.mkBoolean(true); Term intTerm = d_tm.mkInteger(1); ASSERT_NO_THROW(d_solver->addSygusConstraint(boolTerm)); ASSERT_THROW(d_solver->addSygusConstraint(nullTerm), CVC5ApiException); ASSERT_THROW(d_solver->addSygusConstraint(intTerm), CVC5ApiException); TermManager tm; Solver slv(tm); slv.setOption("sygus", "true"); ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSygusConstraints) { d_solver->setOption("sygus", "true"); Term trueTerm = d_tm.mkBoolean(true); Term falseTerm = d_tm.mkBoolean(false); d_solver->addSygusConstraint(trueTerm); d_solver->addSygusConstraint(falseTerm); std::vector constraints{trueTerm, falseTerm}; ASSERT_EQ(d_solver->getSygusConstraints(), constraints); } TEST_F(TestApiBlackSolver, addSygusAssume) { d_solver->setOption("sygus", "true"); Term nullTerm; Term boolTerm = d_tm.mkBoolean(false); Term intTerm = d_tm.mkInteger(1); ASSERT_NO_THROW(d_solver->addSygusAssume(boolTerm)); ASSERT_THROW(d_solver->addSygusAssume(nullTerm), CVC5ApiException); ASSERT_THROW(d_solver->addSygusAssume(intTerm), CVC5ApiException); TermManager tm; Solver slv(tm); slv.setOption("sygus", "true"); ASSERT_THROW(slv.addSygusAssume(boolTerm), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSygusAssumptions) { d_solver->setOption("sygus", "true"); Term trueTerm = d_tm.mkBoolean(true); Term falseTerm = d_tm.mkBoolean(false); d_solver->addSygusAssume(trueTerm); d_solver->addSygusAssume(falseTerm); std::vector assumptions{trueTerm, falseTerm}; ASSERT_EQ(d_solver->getSygusAssumptions(), assumptions); } TEST_F(TestApiBlackSolver, addSygusInvConstraint) { d_solver->setOption("sygus", "true"); Term nullTerm; Term intTerm = d_tm.mkInteger(1); Term inv = d_solver->declareFun("inv", {d_real}, d_bool); Term pre = d_solver->declareFun("pre", {d_real}, d_bool); Term trans = d_solver->declareFun("trans", {d_real, d_real}, d_bool); Term post = d_solver->declareFun("post", {d_real}, d_bool); Term inv1 = d_solver->declareFun("inv1", {d_real}, d_real); Term trans1 = d_solver->declareFun("trans1", {d_bool, d_real}, d_bool); Term trans2 = d_solver->declareFun("trans2", {d_real, d_bool}, d_bool); Term trans3 = d_solver->declareFun("trans3", {d_real, d_real}, d_real); ASSERT_NO_THROW(d_solver->addSygusInvConstraint(inv, pre, trans, post)); ASSERT_THROW(d_solver->addSygusInvConstraint(nullTerm, pre, trans, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, nullTerm, trans, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, nullTerm, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans, nullTerm), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(intTerm, pre, trans, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv1, pre, trans, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, trans, trans, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, intTerm, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, pre, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans1, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans2, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans3, post), CVC5ApiException); ASSERT_THROW(d_solver->addSygusInvConstraint(inv, pre, trans, trans), CVC5ApiException); TermManager tm; Solver slv(tm); slv.setOption("sygus", "true"); Sort boolean2 = tm.getBooleanSort(); Sort real2 = tm.getRealSort(); Term inv22 = slv.declareFun("inv", {real2}, boolean2); Term pre22 = slv.declareFun("pre", {real2}, boolean2); Term trans22 = slv.declareFun("trans", {real2, real2}, boolean2); Term post22 = slv.declareFun("post", {real2}, boolean2); ASSERT_NO_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post22)); ASSERT_THROW(slv.addSygusInvConstraint(inv, pre22, trans22, post22), CVC5ApiException); ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre, trans22, post22), CVC5ApiException); ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans, post22), CVC5ApiException); ASSERT_THROW(slv.addSygusInvConstraint(inv22, pre22, trans22, post), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSynth) { // requires option to be set ASSERT_THROW(d_solver->checkSynth(), CVC5ApiException); d_solver->setOption("sygus", "true"); ASSERT_NO_THROW(d_solver->checkSynth()); } TEST_F(TestApiBlackSolver, getSynthSolution) { d_solver->setOption("sygus", "true"); d_solver->setOption("incremental", "false"); Term nullTerm; Term x = d_tm.mkBoolean(false); Term f = d_solver->synthFun("f", {}, d_bool); ASSERT_THROW(d_solver->getSynthSolution(f), CVC5ApiException); cvc5::SynthResult sr = d_solver->checkSynth(); ASSERT_TRUE(sr.hasSolution()); ASSERT_NO_THROW(d_solver->getSynthSolution(f)); ASSERT_NO_THROW(d_solver->getSynthSolution(f)); ASSERT_THROW(d_solver->getSynthSolution(nullTerm), CVC5ApiException); ASSERT_THROW(d_solver->getSynthSolution(x), CVC5ApiException); ASSERT_THROW(Solver(d_tm).getSynthSolution(f), CVC5ApiException); } TEST_F(TestApiBlackSolver, getSynthSolutions) { d_solver->setOption("sygus", "true"); d_solver->setOption("incremental", "false"); Term nullTerm; Term x = d_tm.mkBoolean(false); Term f = d_solver->synthFun("f", {}, d_bool); ASSERT_THROW(d_solver->getSynthSolutions({}), CVC5ApiException); ASSERT_THROW(d_solver->getSynthSolutions({f}), CVC5ApiException); d_solver->checkSynth(); ASSERT_NO_THROW(d_solver->getSynthSolutions({f})); ASSERT_NO_THROW(d_solver->getSynthSolutions({f, f})); ASSERT_THROW(d_solver->getSynthSolutions({}), CVC5ApiException); ASSERT_THROW(d_solver->getSynthSolutions({nullTerm}), CVC5ApiException); ASSERT_THROW(d_solver->getSynthSolutions({x}), CVC5ApiException); ASSERT_THROW(Solver(d_tm).getSynthSolutions({x}), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSynthNext) { d_solver->setOption("sygus", "true"); d_solver->setOption("incremental", "true"); Term f = d_solver->synthFun("f", {}, d_bool); cvc5::SynthResult sr = d_solver->checkSynth(); ASSERT_TRUE(sr.hasSolution()); ASSERT_NO_THROW(d_solver->getSynthSolutions({f})); sr = d_solver->checkSynthNext(); ASSERT_TRUE(sr.hasSolution()); ASSERT_NO_THROW(d_solver->getSynthSolutions({f})); } TEST_F(TestApiBlackSolver, checkSynthNext2) { d_solver->setOption("sygus", "true"); d_solver->setOption("incremental", "false"); (void)d_solver->synthFun("f", {}, d_bool); d_solver->checkSynth(); ASSERT_THROW(d_solver->checkSynthNext(), CVC5ApiException); } TEST_F(TestApiBlackSolver, checkSynthNext3) { d_solver->setOption("sygus", "true"); d_solver->setOption("incremental", "true"); (void)d_solver->synthFun("f", {}, d_bool); ASSERT_THROW(d_solver->checkSynthNext(), CVC5ApiException); } TEST_F(TestApiBlackSolver, findSynth) { d_solver->setOption("sygus", "true"); Term start = d_tm.mkVar(d_bool); Grammar g = d_solver->mkGrammar({}, {start}); ASSERT_THROW(d_solver->synthFun("f", {}, d_bool, g), CVC5ApiException); Term truen = d_tm.mkBoolean(true); Term falsen = d_tm.mkBoolean(false); g.addRule(start, truen); g.addRule(start, falsen); (void)d_solver->synthFun("f", {}, d_bool, g); // should enumerate based on the grammar of the function to synthesize above cvc5::Term t = d_solver->findSynth(modes::FindSynthTarget::ENUM); ASSERT_TRUE(!t.isNull() && t.getSort().isBoolean()); } TEST_F(TestApiBlackSolver, findSynth2) { d_solver->setOption("sygus", "true"); d_solver->setOption("incremental", "true"); Term start = d_tm.mkVar(d_bool); Grammar g = d_solver->mkGrammar({}, {start}); Term truen = d_tm.mkBoolean(true); Term falsen = d_tm.mkBoolean(false); g.addRule(start, truen); g.addRule(start, falsen); // should enumerate true/false cvc5::Term t = d_solver->findSynth(modes::FindSynthTarget::ENUM, g); ASSERT_TRUE(!t.isNull() && t.getSort().isBoolean()); t = d_solver->findSynthNext(); ASSERT_TRUE(!t.isNull() && t.getSort().isBoolean()); } TEST_F(TestApiBlackSolver, tupleProject) { std::vector elements = { d_tm.mkBoolean(true), d_tm.mkInteger(3), d_tm.mkString("C"), d_tm.mkTerm(Kind::SET_SINGLETON, {d_tm.mkString("Z")})}; Term tuple = d_tm.mkTuple(elements); std::vector indices1 = {}; std::vector indices2 = {0}; std::vector indices3 = {0, 1}; std::vector indices4 = {0, 0, 2, 2, 3, 3, 0}; std::vector indices5 = {4}; std::vector indices6 = {0, 4}; ASSERT_NO_THROW( d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices1), {tuple})); ASSERT_NO_THROW( d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices2), {tuple})); ASSERT_NO_THROW( d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices3), {tuple})); ASSERT_NO_THROW( d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices4), {tuple})); ASSERT_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices5), {tuple}), CVC5ApiException); ASSERT_THROW(d_tm.mkTerm(d_tm.mkOp(Kind::TUPLE_PROJECT, indices6), {tuple}), CVC5ApiException); std::vector indices = {0, 3, 2, 0, 1, 2}; Op op = d_tm.mkOp(Kind::TUPLE_PROJECT, indices); Term projection = d_tm.mkTerm(op, {tuple}); Datatype datatype = tuple.getSort().getDatatype(); DatatypeConstructor constructor = datatype[0]; for (size_t i = 0; i < indices.size(); i++) { Term selectorTerm = constructor[indices[i]].getTerm(); Term selectedTerm = d_tm.mkTerm(Kind::APPLY_SELECTOR, {selectorTerm, tuple}); Term simplifiedTerm = d_solver->simplify(selectedTerm); ASSERT_EQ(elements[indices[i]], simplifiedTerm); } ASSERT_EQ( "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton " "\"Z\")))", projection.toString()); } TEST_F(TestApiBlackSolver, output) { ASSERT_THROW(d_solver->isOutputOn("foo-invalid"), CVC5ApiException); ASSERT_THROW(d_solver->getOutput("foo-invalid"), CVC5ApiException); ASSERT_FALSE(d_solver->isOutputOn("inst")); ASSERT_EQ(null_os.rdbuf(), d_solver->getOutput("inst").rdbuf()); d_solver->setOption("output", "inst"); ASSERT_TRUE(d_solver->isOutputOn("inst")); ASSERT_NE(null_os.rdbuf(), d_solver->getOutput("inst").rdbuf()); } TEST_F(TestApiBlackSolver, getDatatypeArity) { DatatypeConstructorDecl ctor1 = d_tm.mkDatatypeConstructorDecl("_x21"); DatatypeConstructorDecl ctor2 = d_tm.mkDatatypeConstructorDecl("_x31"); Sort s3 = d_solver->declareDatatype(std::string("_x17"), {ctor1, ctor2}); ASSERT_EQ(s3.getDatatypeArity(), 0); } TEST_F(TestApiBlackSolver, declareOracleFunError) { // cannot declare without option ASSERT_THROW(d_solver->declareOracleFun( "f", {d_int}, d_int, [&](const std::vector& input) { return d_tm.mkInteger(0); }); , CVC5ApiException); d_solver->setOption("oracles", "true"); Sort nullSort; // bad sort ASSERT_THROW(d_solver->declareOracleFun( "f", {nullSort}, d_int, [&](const std::vector& input) { return d_tm.mkInteger(0); }); , CVC5ApiException); } TEST_F(TestApiBlackSolver, declareOracleFunUnsat) { d_solver->setOption("oracles", "true"); // f is the function implementing (lambda ((x Int)) (+ x 1)) Term f = d_solver->declareOracleFun( "f", {d_int}, d_int, [&](const std::vector& input) { if (input[0].isUInt32Value()) { return d_tm.mkInteger(input[0].getUInt32Value() + 1); } return d_tm.mkInteger(0); }); Term three = d_tm.mkInteger(3); Term five = d_tm.mkInteger(5); Term eq = d_tm.mkTerm(Kind::EQUAL, {d_tm.mkTerm(Kind::APPLY_UF, {f, three}), five}); d_solver->assertFormula(eq); // (f 3) = 5 ASSERT_TRUE(d_solver->checkSat().isUnsat()); TermManager tm; Solver slv(tm); slv.setOption("oracles", "true"); Sort iiSort = tm.getIntegerSort(); ASSERT_THROW(slv.declareOracleFun("f", {iiSort}, d_int, [&](const std::vector& input) { if (input[0].isUInt32Value()) { return tm.mkInteger( input[0].getUInt32Value() + 1); } return tm.mkInteger(0); }), CVC5ApiException); ASSERT_THROW(slv.declareOracleFun("f", {d_int}, iiSort, [&](const std::vector& input) { if (input[0].isUInt32Value()) { return tm.mkInteger( input[0].getUInt32Value() + 1); } return tm.mkInteger(0); }), CVC5ApiException); // this cannot be caught during declaration, is caught during check-sat Term f2 = slv.declareOracleFun( "f2", {iiSort}, iiSort, [&](const std::vector& input) { if (input[0].isUInt32Value()) { return d_tm.mkInteger(input[0].getUInt32Value() + 1); } return d_tm.mkInteger(0); }); Term eq2 = tm.mkTerm( Kind::EQUAL, {tm.mkTerm(Kind::APPLY_UF, {f2, tm.mkInteger(3)}), tm.mkInteger(5)}); slv.assertFormula(eq2); ASSERT_THROW(slv.checkSat(), CVC5ApiException); } TEST_F(TestApiBlackSolver, declareOracleFunSat) { d_solver->setOption("oracles", "true"); d_solver->setOption("produce-models", "true"); // f is the function implementing (lambda ((x Int)) (% x 10)) Term f = d_solver->declareOracleFun( "f", {d_int}, d_int, [&](const std::vector& input) { if (input[0].isUInt32Value()) { return d_tm.mkInteger(input[0].getUInt32Value() % 10); } return d_tm.mkInteger(0); }); Term seven = d_tm.mkInteger(7); Term x = d_tm.mkConst(d_int, "x"); Term lb = d_tm.mkTerm(Kind::GEQ, {x, d_tm.mkInteger(0)}); d_solver->assertFormula(lb); Term ub = d_tm.mkTerm(Kind::LEQ, {x, d_tm.mkInteger(100)}); d_solver->assertFormula(ub); Term eq = d_tm.mkTerm(Kind::EQUAL, {d_tm.mkTerm(Kind::APPLY_UF, {f, x}), seven}); d_solver->assertFormula(eq); // x >= 0 ^ x <= 100 ^ (f x) = 7 ASSERT_TRUE(d_solver->checkSat().isSat()); Term xval = d_solver->getValue(x); ASSERT_TRUE(xval.isUInt32Value()); ASSERT_TRUE(xval.getUInt32Value() % 10 == 7); } TEST_F(TestApiBlackSolver, declareOracleFunSat2) { d_solver->setOption("oracles", "true"); d_solver->setOption("produce-models", "true"); // f is the function implementing (lambda ((x Int) (y Int)) (= x y)) Term eq = d_solver->declareOracleFun( "eq", {d_int, d_int}, d_bool, [&](const std::vector& input) { return d_tm.mkBoolean(input[0] == input[1]); }); Term x = d_tm.mkConst(d_int, "x"); Term y = d_tm.mkConst(d_int, "y"); Term neq = d_tm.mkTerm(Kind::NOT, {d_tm.mkTerm(Kind::APPLY_UF, {eq, x, y})}); d_solver->assertFormula(neq); // (not (eq x y)) ASSERT_TRUE(d_solver->checkSat().isSat()); Term xval = d_solver->getValue(x); Term yval = d_solver->getValue(y); ASSERT_TRUE(xval != yval); } class PluginUnsat : public Plugin { public: PluginUnsat(TermManager& tm) : Plugin(tm), d_tm(tm) {} virtual ~PluginUnsat() {} std::vector check() override { std::vector lemmas; // add the "false" lemma. Term flem = d_tm.mkBoolean(false); lemmas.push_back(flem); return lemmas; } std::string getName() override { return "PluginUnsat"; } private: /** Reference to the term manager */ TermManager& d_tm; }; TEST_F(TestApiBlackSolver, pluginUnsat) { PluginUnsat pu(d_tm); d_solver->addPlugin(pu); ASSERT_TRUE(pu.getName() == "PluginUnsat"); // should be unsat since the plugin above asserts "false" as a lemma ASSERT_TRUE(d_solver->checkSat().isUnsat()); } class PluginListen : public Plugin { public: PluginListen(TermManager& tm) : Plugin(tm), d_hasSeenTheoryLemma(false), d_hasSeenSatClause(false) { } virtual ~PluginListen() {} void notifySatClause(const Term& cl) override { Plugin::notifySatClause(cl); // Cover default implementation d_hasSeenSatClause = true; } bool hasSeenSatClause() const { return d_hasSeenSatClause; } void notifyTheoryLemma(const Term& lem) override { Plugin::notifyTheoryLemma(lem); // Cover default implementation d_hasSeenTheoryLemma = true; } bool hasSeenTheoryLemma() const { return d_hasSeenTheoryLemma; } std::string getName() override { return "PluginListen"; } private: /** have we seen a theory lemma? */ bool d_hasSeenTheoryLemma; /** have we seen a SAT clause? */ bool d_hasSeenSatClause; }; TEST_F(TestApiBlackSolver, pluginListen) { // NOTE: this shouldn't be necessary but ensures notifySatClause is called here. d_solver->setOption("plugin-notify-sat-clause-in-solve", "false"); PluginListen pl(d_tm); d_solver->addPlugin(pl); Term x = d_tm.mkConst(d_string, "x"); Term y = d_tm.mkConst(d_string, "y"); Term ctn1 = d_tm.mkTerm(Kind::STRING_CONTAINS, {x, y}); Term ctn2 = d_tm.mkTerm(Kind::STRING_CONTAINS, {y, x}); d_solver->assertFormula(d_tm.mkTerm(Kind::OR, {ctn1, ctn2})); Term lx = d_tm.mkTerm(Kind::STRING_LENGTH, {x}); Term ly = d_tm.mkTerm(Kind::STRING_LENGTH, {y}); Term lc = d_tm.mkTerm(Kind::GT, {lx, ly}); d_solver->assertFormula(lc); ASSERT_TRUE(d_solver->checkSat().isSat()); // above input formulas should induce a theory lemma and SAT clause learning ASSERT_TRUE(pl.hasSeenTheoryLemma()); ASSERT_TRUE(pl.hasSeenSatClause()); } TEST_F(TestApiBlackSolver, pluginListenCadical) { cvc5::Solver solver(d_tm); solver.setOption("sat-solver", "cadical"); solver.setOption("plugin-notify-sat-clause-in-solve", "true"); PluginListen pl(d_tm); solver.addPlugin(pl); Sort bv1 = d_tm.mkBitVectorSort(8); Sort bv16 = d_tm.mkBitVectorSort(8); Term x = d_tm.mkConst(d_bool, "x"); Term z16 = d_tm.mkBitVector(16, 0); Term o16 = d_tm.mkBitVector(16, 1); Term z1 = d_tm.mkBitVector(1, 0); Term o1 = d_tm.mkBitVector(1, 1); Term ite1 = d_tm.mkTerm(Kind::ITE, {x, z16, o16}); Term add = d_tm.mkTerm(Kind::BITVECTOR_ADD, {o16, ite1}); Term eq1 = d_tm.mkTerm(Kind::EQUAL, {z16, add}); Term ite2 = d_tm.mkTerm(Kind::ITE, {eq1, o1, z1}); Term eq2 = d_tm.mkTerm(Kind::EQUAL, {z1, d_tm.mkTerm(Kind::BITVECTOR_NOT, {ite2})}); solver.assertFormula(eq2); ASSERT_TRUE(solver.checkSat().isUnsat()); // above input formulas should induce a theory lemma and SAT clause learning ASSERT_TRUE(pl.hasSeenTheoryLemma()); ASSERT_TRUE(pl.hasSeenSatClause()); } TEST_F(TestApiBlackSolver, verticalBars) { Term a = d_solver->declareFun("|a |", {}, d_real); ASSERT_EQ("|a |", a.toString()); } TEST_F(TestApiBlackSolver, getVersion) { std::cout << d_solver->getVersion() << std::endl; } TEST_F(TestApiBlackSolver, multipleSolvers) { Term function1, function2, value1, value2, definedFunction; Term zero; { Solver s1(d_tm); s1.setLogic("ALL"); s1.setOption("produce-models", "true"); function1 = s1.declareFun("f1", {}, d_int); Term x = d_tm.mkVar(d_int, "x"); zero = d_tm.mkInteger(0); definedFunction = s1.defineFun("f", {x}, d_int, zero); s1.assertFormula(function1.eqTerm(zero)); s1.checkSat(); value1 = s1.getValue(function1); } ASSERT_EQ(zero, value1); { Solver s2(d_tm); s2.setLogic("ALL"); s2.setOption("produce-models", "true"); function2 = s2.declareFun("function2", {}, d_int); s2.assertFormula(function2.eqTerm(value1)); s2.checkSat(); value2 = s2.getValue(function2); } ASSERT_EQ(value1, value2); { Solver s3(d_tm); s3.setLogic("ALL"); s3.setOption("produce-models", "true"); function2 = s3.declareFun("function3", {}, d_int); Term apply = d_tm.mkTerm(Kind::APPLY_UF, {definedFunction, zero}); s3.assertFormula(function2.eqTerm(apply)); s3.checkSat(); Term value3 = s3.getValue(function2); ASSERT_EQ(value1, value3); } } #ifdef CVC5_USE_COCOA TEST_F(TestApiBlackSolver, basicFiniteField) { d_solver->setOption("produce-models", "true"); Sort F = d_tm.mkFiniteFieldSort("5"); Term a = d_tm.mkConst(F, "a"); Term b = d_tm.mkConst(F, "b"); ASSERT_EQ("5", F.getFiniteFieldSize()); Term inv = d_tm.mkTerm(Kind::EQUAL, {d_tm.mkTerm(Kind::FINITE_FIELD_MULT, {a, b}), d_tm.mkFiniteFieldElem("1", F)}); Term aIsTwo = d_tm.mkTerm(Kind::EQUAL, {a, d_tm.mkFiniteFieldElem("2", F)}); d_solver->assertFormula(inv); d_solver->assertFormula(aIsTwo); ASSERT_TRUE(d_solver->checkSat().isSat()); ASSERT_EQ(d_solver->getValue(a).getFiniteFieldValue(), "2"); ASSERT_EQ(d_solver->getValue(b).getFiniteFieldValue(), "-2"); Term bIsTwo = d_tm.mkTerm(Kind::EQUAL, {b, d_tm.mkFiniteFieldElem("2", F)}); d_solver->assertFormula(bIsTwo); ASSERT_FALSE(d_solver->checkSat().isSat()); } TEST_F(TestApiBlackSolver, basicFiniteFieldBase) { d_solver->setOption("produce-models", "true"); Sort F = d_tm.mkFiniteFieldSort("101", 2); Term a = d_tm.mkConst(F, "a"); Term b = d_tm.mkConst(F, "b"); ASSERT_EQ("5", F.getFiniteFieldSize()); Term inv = d_tm.mkTerm(Kind::EQUAL, {d_tm.mkTerm(Kind::FINITE_FIELD_MULT, {a, b}), d_tm.mkFiniteFieldElem("1", F, 3)}); Term aIsTwo = d_tm.mkTerm(Kind::EQUAL, {a, d_tm.mkFiniteFieldElem("10", F, 2)}); d_solver->assertFormula(inv); d_solver->assertFormula(aIsTwo); ASSERT_TRUE(d_solver->checkSat().isSat()); ASSERT_EQ(d_solver->getValue(a).getFiniteFieldValue(), "2"); ASSERT_EQ(d_solver->getValue(b).getFiniteFieldValue(), "-2"); Term bIsTwo = d_tm.mkTerm(Kind::EQUAL, {b, d_tm.mkFiniteFieldElem("2", F)}); d_solver->assertFormula(bIsTwo); ASSERT_FALSE(d_solver->checkSat().isSat()); } #endif // CVC5_USE_COCOA } // namespace test } // namespace cvc5::internal