From 9e481faf7dfce8f992ae6730ad49f6db335b6432 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Sat, 10 Oct 2020 08:25:24 -0500 Subject: [PATCH] Provide API version of some SMT Commands. (#5222) This PR provides an SMT version of the following SMT commands: get-instantiations block-model block-model-values get-qe get-qe-disjunct command.cpp now calls those functions instead of their SmtEngine counterparts. In addition, SEXPR is now an API kind. --- src/api/cvc4cpp.cpp | 74 ++++++++++++++++++-- src/api/cvc4cpp.h | 66 ++++++++++++++++++ src/api/cvc4cppkind.h | 13 +++- src/smt/command.cpp | 62 +++++++++-------- src/smt/command.h | 2 +- src/smt/smt_engine.cpp | 3 - test/unit/api/solver_black.h | 129 +++++++++++++++++++++++++++++++++++ 7 files changed, 311 insertions(+), 38 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 165854476..4dda6098e 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -79,6 +79,7 @@ const static std::unordered_map s_kinds{ {DISTINCT, CVC4::Kind::DISTINCT}, {CONSTANT, CVC4::Kind::VARIABLE}, {VARIABLE, CVC4::Kind::BOUND_VARIABLE}, + {SEXPR, CVC4::Kind::SEXPR}, {LAMBDA, CVC4::Kind::LAMBDA}, {WITNESS, CVC4::Kind::WITNESS}, /* Boolean ------------------------------------------------------------- */ @@ -2321,11 +2322,9 @@ Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const d_ctor->getConstructor()); (void)ret.getType(true); /* kick off type checking */ // apply type ascription to the operator - Term sctor = - api::Term(d_solver, - ret); + Term sctor = api::Term(d_solver, ret); return sctor; - + CVC4_API_SOLVER_TRY_CATCH_END; } @@ -5176,6 +5175,28 @@ std::vector Solver::getValue(const std::vector& terms) const CVC4_API_SOLVER_TRY_CATCH_END; } +Term Solver::getQuantifierElimination(api::Term q) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(q); + CVC4_API_SOLVER_CHECK_TERM(q); + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + return Term(this, + d_smtEngine->getQuantifierElimination(q.getNode(), true, true)); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +Term Solver::getQuantifierEliminationDisjunct(api::Term q) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_ARG_CHECK_NOT_NULL(q); + CVC4_API_SOLVER_CHECK_TERM(q); + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + return Term( + this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true)); + CVC4_API_SOLVER_TRY_CATCH_END; +} + Term Solver::getSeparationHeap() const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; @@ -5315,6 +5336,51 @@ void Solver::printModel(std::ostream& out) const CVC4_API_SOLVER_TRY_CATCH_END; } +void Solver::blockModel() const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + << "Cannot get value unless model generation is enabled " + "(try --produce-models)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) + << "Cannot get value when in unsat mode."; + d_smtEngine->blockModel(); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +void Solver::blockModelValues(const std::vector& terms) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + << "Cannot get value unless model generation is enabled " + "(try --produce-models)"; + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) + << "Cannot get value when in unsat mode."; + CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) + << "a non-empty set of terms"; + for (int i = 0; i < terms.size(); ++i) + { + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + !terms[i].isNull(), "term", terms[i], i) + << "a non-null term"; + CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED( + this == terms[i].d_solver, "term", terms[i], i) + << "a term associated to this solver object"; + } + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + d_smtEngine->blockModelValues(termVectorToExprs(terms)); + CVC4_API_SOLVER_TRY_CATCH_END; +} + +void Solver::printInstantiations(std::ostream& out) const +{ + CVC4_API_SOLVER_TRY_CATCH_BEGIN; + CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); + d_smtEngine->printInstantiations(out); + CVC4_API_SOLVER_TRY_CATCH_END; +} + /** * ( push ) */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 679f39750..5c6b01d59 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3094,6 +3094,48 @@ class CVC4_PUBLIC Solver */ std::vector getValue(const std::vector& terms) const; + /** + * Do quantifier elimination. + * SMT-LIB: ( get-qe ) + * Requires a logic that supports quantifier elimination. Currently, the only + * logics supported by quantifier elimination is LRA and LIA. + * @param q a quantified formula of the form: + * Q x1...xn. P( x1...xn, y1...yn ) + * where P( x1...xn, y1...yn ) is a quantifier-free formula + * @return a formula ret such that, given the current set of formulas A + * asserted to this solver: + * - ( A ^ q ) and ( A ^ ret ) are equivalent + * - ret is quantifier-free formula containing only free variables in + * y1...yn. + */ + Term getQuantifierElimination(api::Term q) const; + + /** + * Do partial quantifier elimination, which can be used for incrementally + * computing the result of a quantifier elimination. + * SMT-LIB: ( get-qe-disjunct ) + * Requires a logic that supports quantifier elimination. Currently, the only + * logics supported by quantifier elimination is LRA and LIA. + * @param q a quantified formula of the form: + * Q x1...xn. P( x1...xn, y1...yn ) + * where P( x1...xn, y1...yn ) is a quantifier-free formula + * @return a formula ret such that, given the current set of formulas A + * asserted to this solver: + * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is + * exists, + * - ret is quantifier-free formula containing only free variables in + * y1...yn, + * - If Q is exists, let A^Q_n be the formula + * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n + * where for each i=1,...n, formula ret^Q_i is the result of calling + * getQuantifierEliminationDisjunct for q with the set of assertions + * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be + * A ^ ret^Q_1 ^ ... ^ ret^Q_n + * where ret^Q_i is the same as above. In either case, we have + * that ret^Q_j will eventually be true or false, for some finite j. + */ + Term getQuantifierEliminationDisjunct(api::Term q) const; + /** * When using separation logic, obtain the term for the heap. * @return The term for the heap @@ -3168,6 +3210,30 @@ class CVC4_PUBLIC Solver */ void printModel(std::ostream& out) const; + /** + * Block the current model. Can be called only if immediately preceded by a + * SAT or INVALID query. + * SMT-LIB: ( block-model ) + * Requires enabling 'produce-models' option and setting 'block-models' option + * to a mode other than "none". + */ + void blockModel() const; + + /** + * Block the current model values of (at least) the values in terms. Can be + * called only if immediately preceded by a SAT or NOT_ENTAILED query. + * SMT-LIB: ( block-model-values ( + ) ) + * Requires enabling 'produce-models' option and setting 'block-models' option + * to a mode other than "none". + */ + void blockModelValues(const std::vector& terms) const; + + /** + * Print all instantiations made by the quantifiers module. + * @param out the output stream + */ + void printInstantiations(std::ostream& out) const; + /** * Push (a) level(s) to the assertion stack. * SMT-LIB: ( push ) diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 6f84a9959..913a4a993 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -120,9 +120,18 @@ enum CVC4_PUBLIC Kind : int32_t #if 0 /* Skolem variable (internal only) */ SKOLEM, - /* Symbolic expression (any arity) */ - SEXPR, #endif + /* + * Symbolic expression. + * Parameters: n > 0 + * -[1]..[n]: terms + * Create with: + * mkTerm(Kind kind, Term child) + * mkTerm(Kind kind, Term child1, Term child2) + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector& children) + */ + SEXPR, /** * Lambda expression. * Parameters: 2 diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5edbe51e0..73553a31c 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -282,7 +282,7 @@ void AssertCommand::invoke(api::Solver* solver) { try { - solver->getSmtEngine()->assertFormula(d_term.getExpr(), d_inUnsatCore); + solver->getSmtEngine()->assertFormula(d_term.getNode(), d_inUnsatCore); d_commandStatus = CommandSuccess::instance(); } catch (UnsafeInterruptException& e) @@ -1594,9 +1594,16 @@ ExpandDefinitionsCommand::ExpandDefinitionsCommand(api::Term term) api::Term ExpandDefinitionsCommand::getTerm() const { return d_term; } void ExpandDefinitionsCommand::invoke(api::Solver* solver) { - Node t = d_term.getNode(); - d_result = api::Term(solver, solver->getSmtEngine()->expandDefinitions(t)); - d_commandStatus = CommandSuccess::instance(); + try + { + d_result = api::Term( + solver, solver->getSmtEngine()->expandDefinitions(d_term.getNode())); + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } } api::Term ExpandDefinitionsCommand::getResult() const { return d_result; } @@ -1659,29 +1666,23 @@ void GetValueCommand::invoke(api::Solver* solver) { try { - NodeManager* nm = solver->getNodeManager(); - smt::SmtScope scope(solver->getSmtEngine()); - std::vector result = - api::termVectorToNodes(solver->getValue(d_terms)); + std::vector result = solver->getValue(d_terms); Assert(result.size() == d_terms.size()); for (int i = 0, size = d_terms.size(); i < size; i++) { - api::Term t = d_terms[i]; - Node tNode = t.getNode(); - Node request = options::expandDefinitions() - ? solver->getSmtEngine()->expandDefinitions(tNode) - : tNode; - Node value = result[i]; - if (value.getType().isInteger() && request.getType() == nm->realType()) + api::Term request = d_terms[i]; + api::Term value = result[i]; + if (value.getSort().isInteger() + && request.getSort() == solver->getRealSort()) { // Need to wrap in division-by-one so that output printers know this // is an integer-looking constant that really should be output as // a rational. Necessary for SMT-LIB standards compliance. - value = nm->mkNode(kind::DIVISION, value, nm->mkConst(Rational(1))); + value = solver->mkTerm(api::DIVISION, value, solver->mkReal(1)); } - result[i] = nm->mkNode(kind::SEXPR, request, value); + result[i] = solver->mkTerm(api::SEXPR, request, value); } - d_result = api::Term(solver, nm->mkNode(kind::SEXPR, result)); + d_result = solver->mkTerm(api::SEXPR, result); d_commandStatus = CommandSuccess::instance(); } catch (api::CVC4ApiRecoverableException& e) @@ -1873,10 +1874,10 @@ void BlockModelCommand::invoke(api::Solver* solver) { try { - solver->getSmtEngine()->blockModel(); + solver->blockModel(); d_commandStatus = CommandSuccess::instance(); } - catch (RecoverableModalException& e) + catch (api::CVC4ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1928,7 +1929,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver) { try { - solver->getSmtEngine()->blockModelValues(api::termVectorToExprs(d_terms)); + solver->blockModelValues(d_terms); d_commandStatus = CommandSuccess::instance(); } catch (RecoverableModalException& e) @@ -1997,12 +1998,12 @@ void GetProofCommand::toStream(std::ostream& out, /* class GetInstantiationsCommand */ /* -------------------------------------------------------------------------- */ -GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {} +GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {} void GetInstantiationsCommand::invoke(api::Solver* solver) { try { - d_smtEngine = solver->getSmtEngine(); + d_solver = solver; d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -2020,7 +2021,7 @@ void GetInstantiationsCommand::printResult(std::ostream& out, } else { - d_smtEngine->printInstantiations(out); + d_solver->printInstantiations(out); } } @@ -2028,7 +2029,7 @@ Command* GetInstantiationsCommand::clone() const { GetInstantiationsCommand* c = new GetInstantiationsCommand(); // c->d_result = d_result; - c->d_smtEngine = d_smtEngine; + c->d_solver = d_solver; return c; } @@ -2301,9 +2302,14 @@ void GetQuantifierEliminationCommand::invoke(api::Solver* solver) { try { - d_result = api::Term(solver, - solver->getSmtEngine()->getQuantifierElimination( - d_term.getNode(), d_doFull)); + if (d_doFull) + { + d_result = solver->getQuantifierElimination(d_term); + } + else + { + d_result = solver->getQuantifierEliminationDisjunct(d_term); + } d_commandStatus = CommandSuccess::instance(); } catch (exception& e) diff --git a/src/smt/command.h b/src/smt/command.h index 81a736407..b823b5730 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1070,7 +1070,7 @@ class CVC4_PUBLIC GetInstantiationsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; protected: - SmtEngine* d_smtEngine; + api::Solver* d_solver; }; /* class GetInstantiationsCommand */ class CVC4_PUBLIC GetSynthSolutionCommand : public Command diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 25643200f..ff45ce0ce 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1444,9 +1444,6 @@ Result SmtEngine::blockModelValues(const std::vector& exprs) finishInit(); - PrettyCheckArgument( - !exprs.empty(), - "block model values must be called on non-empty set of terms"); if (Dump.isOn("benchmark")) { getOutputManager().getPrinter().toStreamCmdBlockModelValues( diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 62531daf7..aa4289ef3 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -115,6 +115,8 @@ class SolverBlack : public CxxTest::TestSuite void testGetValue1(); void testGetValue2(); void testGetValue3(); + void testGetQuantifierElimination(); + void testGetQuantifierEliminationDisjunct(); void testGetSeparationHeapTerm1(); void testGetSeparationHeapTerm2(); void testGetSeparationHeapTerm3(); @@ -141,6 +143,16 @@ class SolverBlack : public CxxTest::TestSuite void testPrintModel2(); void testPrintModel3(); + void testBlockModel1(); + void testBlockModel2(); + void testBlockModel3(); + void testBlockModel4(); + void testBlockModelValues1(); + void testBlockModelValues2(); + void testBlockModelValues3(); + void testBlockModelValues4(); + void testBlockModelValues5(); + void testSimplify(); void testAssertFormula(); @@ -1613,6 +1625,36 @@ void SolverBlack::testGetValue3() TS_ASSERT_THROWS(slv.getValue(x), CVC4ApiException&); } +void SolverBlack::testGetQuantifierElimination() +{ + Term x = d_solver->mkVar(d_solver->getBooleanSort(), "x"); + Term forall = + d_solver->mkTerm(FORALL, + d_solver->mkTerm(BOUND_VAR_LIST, x), + d_solver->mkTerm(OR, x, d_solver->mkTerm(NOT, x))); + TS_ASSERT_THROWS(d_solver->getQuantifierElimination(Term()), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->getQuantifierElimination(Solver().mkBoolean(false)), + CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierElimination(forall)); +} + +void SolverBlack::testGetQuantifierEliminationDisjunct() +{ + Term x = d_solver->mkVar(d_solver->getBooleanSort(), "x"); + Term forall = + d_solver->mkTerm(FORALL, + d_solver->mkTerm(BOUND_VAR_LIST, x), + d_solver->mkTerm(OR, x, d_solver->mkTerm(NOT, x))); + TS_ASSERT_THROWS(d_solver->getQuantifierEliminationDisjunct(Term()), + CVC4ApiException&); + TS_ASSERT_THROWS( + d_solver->getQuantifierEliminationDisjunct(Solver().mkBoolean(false)), + CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->getQuantifierEliminationDisjunct(forall)); +} + namespace { /** * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks @@ -1793,6 +1835,93 @@ void SolverBlack::testPrintModel3() TS_ASSERT_THROWS_NOTHING(d_solver->printModel(std::cout)); } +void SolverBlack::testBlockModel1() +{ + d_solver->setOption("produce-models", "true"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&); +} + +void SolverBlack::testBlockModel2() +{ + d_solver->setOption("block-models", "literals"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&); +} + +void SolverBlack::testBlockModel3() +{ + d_solver->setOption("produce-models", "true"); + d_solver->setOption("block-models", "literals"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + TS_ASSERT_THROWS(d_solver->blockModel(), CVC4ApiException&); +} + +void SolverBlack::testBlockModel4() +{ + d_solver->setOption("produce-models", "true"); + d_solver->setOption("block-models", "literals"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + d_solver->checkSat(); + TS_ASSERT_THROWS_NOTHING(d_solver->blockModel()); +} + +void SolverBlack::testBlockModelValues1() +{ + d_solver->setOption("produce-models", "true"); + d_solver->setOption("block-models", "literals"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->blockModelValues({}), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->blockModelValues({Term()}), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->blockModelValues({Solver().mkBoolean(false)}), + CVC4ApiException&); +} + +void SolverBlack::testBlockModelValues2() +{ + d_solver->setOption("produce-models", "true"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&); +} + +void SolverBlack::testBlockModelValues3() +{ + d_solver->setOption("block-models", "literals"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + d_solver->checkSat(); + TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&); +} + +void SolverBlack::testBlockModelValues4() +{ + d_solver->setOption("produce-models", "true"); + d_solver->setOption("block-models", "literals"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + TS_ASSERT_THROWS(d_solver->blockModelValues({x}), CVC4ApiException&); +} + +void SolverBlack::testBlockModelValues5() +{ + d_solver->setOption("produce-models", "true"); + d_solver->setOption("block-models", "literals"); + Term x = d_solver->mkConst(d_solver->getBooleanSort(), "x"); + d_solver->assertFormula(x.eqTerm(x)); + d_solver->checkSat(); + TS_ASSERT_THROWS_NOTHING(d_solver->blockModelValues({x})); +} + void SolverBlack::testSetInfo() { TS_ASSERT_THROWS(d_solver->setInfo("cvc4-lagic", "QF_BV"), CVC4ApiException&); -- 2.30.2