From 6b55bf59675fcdaab4c8dbf70a8a74ebb1f990e9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 2 Aug 2021 20:21:04 -0500 Subject: [PATCH] Remove "inUnsatCore" flag throughout (#6964) The internal solver no longer cares about what assertions are named / are in the unsat core. This simplifies the code so that the (now unused) `inUnsatCore` flag is removed from all interfaces. This eliminates another external use of `getSmtEngine`. --- src/parser/smt2/Smt2.g | 6 +++--- src/parser/tptp/Tptp.g | 11 +++++------ src/parser/tptp/tptp.cpp | 7 ++----- src/parser/tptp/tptp.h | 5 +---- src/smt/assertions.cpp | 13 +++++-------- src/smt/assertions.h | 9 ++------- src/smt/command.cpp | 19 +++++-------------- src/smt/command.h | 6 ++---- src/smt/quant_elim_solver.cpp | 3 +-- src/smt/smt_engine.cpp | 24 ++++++++++-------------- src/smt/smt_engine.h | 18 +++++++----------- src/smt/smt_solver.cpp | 3 +-- src/smt/smt_solver.h | 2 -- src/smt/sygus_solver.cpp | 2 +- 14 files changed, 45 insertions(+), 83 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 483da3ff0..f56fc3c90 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -359,9 +359,9 @@ command [std::unique_ptr* cmd] ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] - { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; - cmd->reset(new AssertCommand(expr, inUnsatCore)); - if(inUnsatCore) { + { cmd->reset(new AssertCommand(expr)); + if (PARSER_STATE->lastNamedTerm().first == expr) + { // set the expression name, if there was a named term std::pair namedTerm = PARSER_STATE->lastNamedTerm(); diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index c96fbf07d..feaf876f7 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -165,7 +165,7 @@ parseCommand returns [cvc5::Command* cmd = NULL] SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula - cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true); + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, true); } | FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); } @@ -177,7 +177,7 @@ parseCommand returns [cvc5::Command* cmd = NULL] SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula - cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, false); } | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd] @@ -191,7 +191,7 @@ parseCommand returns [cvc5::Command* cmd = NULL] SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula - cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, false); } ) RPAREN_TOK DOT_TOK | THF_TOK @@ -218,8 +218,7 @@ parseCommand returns [cvc5::Command* cmd = NULL] SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula - cmd = PARSER_STATE->makeAssertCommand( - fr, aexpr, /* cnf == */ false, true); + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, false); } ) RPAREN_TOK DOT_TOK | INCLUDE_TOK LPAREN_TOK unquotedFileName[name] @@ -249,7 +248,7 @@ parseCommand returns [cvc5::Command* cmd = NULL] cvc5::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants(); if( !aexpr.isNull() ) { - seq->addCommand(new AssertCommand(aexpr, false)); + seq->addCommand(new AssertCommand(aexpr)); } std::string filename = PARSER_STATE->getInput()->getInputStreamName(); diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 91fcc7a12..7c65f5c57 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -573,10 +573,7 @@ api::Term Tptp::getAssertionDistinctConstants() return d_nullExpr; } -Command* Tptp::makeAssertCommand(FormulaRole fr, - api::Term expr, - bool cnf, - bool inUnsatCore) +Command* Tptp::makeAssertCommand(FormulaRole fr, api::Term expr, bool cnf) { // For SZS ontology compliance. // if we're in cnf() though, conjectures don't result in "Theorem" or @@ -588,7 +585,7 @@ Command* Tptp::makeAssertCommand(FormulaRole fr, if( expr.isNull() ){ return new EmptyCommand("Untreated role for expression"); }else{ - return new AssertCommand(expr, inUnsatCore); + return new AssertCommand(expr); } } diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index 258394486..2167a6c38 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -134,10 +134,7 @@ class Tptp : public Parser { * getAssertionExpr above). This may set a flag in the parser to mark * that we have asserted a conjecture. */ - Command* makeAssertCommand(FormulaRole fr, - api::Term expr, - bool cnf, - bool inUnsatCore); + Command* makeAssertCommand(FormulaRole fr, api::Term expr, bool cnf); /** Ugly hack because I don't know how to return an expression from a token */ diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 504dce71e..b7688d833 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -70,7 +70,6 @@ void Assertions::clearCurrent() } void Assertions::initializeCheckSat(const std::vector& assumptions, - bool inUnsatCore, bool isEntailmentCheck) { NodeManager* nm = NodeManager::currentNM(); @@ -105,7 +104,7 @@ void Assertions::initializeCheckSat(const std::vector& assumptions, Node n = d_absValues.substituteAbstractValues(e); // Ensure expr is type-checked at this point. ensureBoolean(n); - addFormula(n, inUnsatCore, true, true, false, false); + addFormula(n, true, true, false, false); } if (d_globalDefineFunLemmas != nullptr) { @@ -114,16 +113,16 @@ void Assertions::initializeCheckSat(const std::vector& assumptions, // zero assertions) for (const Node& lemma : *d_globalDefineFunLemmas) { - addFormula(lemma, false, true, false, true, false); + addFormula(lemma, true, false, true, false); } } } -void Assertions::assertFormula(const Node& n, bool inUnsatCore) +void Assertions::assertFormula(const Node& n) { ensureBoolean(n); bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); - addFormula(n, inUnsatCore, true, false, false, maybeHasFv); + addFormula(n, true, false, false, maybeHasFv); } std::vector& Assertions::getAssumptions() { return d_assumptions; } @@ -141,7 +140,6 @@ context::CDList* Assertions::getAssertionList() } void Assertions::addFormula(TNode n, - bool inUnsatCore, bool inInput, bool isAssumption, bool isFunDef, @@ -158,7 +156,6 @@ void Assertions::addFormula(TNode n, return; } Trace("smt") << "SmtEnginePrivate::addFormula(" << n - << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << ", isAssumption = " << isAssumption << ", isFunDef = " << isFunDef << std::endl; @@ -210,7 +207,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global) { // we don't check for free variables here, since even if we are sygus, // we could contain functions-to-synthesize within definitions. - addFormula(n, false, true, false, true, false); + addFormula(n, true, false, true, false); } } diff --git a/src/smt/assertions.h b/src/smt/assertions.h index c922cbaea..de7ba72c9 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -65,24 +65,20 @@ class Assertions * upcoming check-sat call. * * @param assumptions The assumptions of the upcoming check-sat call. - * @param inUnsatCore Whether assumptions are in the unsat core. * @param isEntailmentCheck Whether we are checking entailment of assumptions * in the upcoming check-sat call. */ void initializeCheckSat(const std::vector& assumptions, - bool inUnsatCore, bool isEntailmentCheck); /** * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for * literals and conjunction of literals. Returns false if - * immediately determined to be inconsistent. This version - * takes a Boolean flag to determine whether to include this asserted - * formula in an unsat core (if one is later requested). + * immediately determined to be inconsistent. * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - void assertFormula(const Node& n, bool inUnsatCore = true); + void assertFormula(const Node& n); /** * Assert that n corresponds to an assertion from a define-fun or * define-fun-rec command. @@ -145,7 +141,6 @@ class Assertions * (this is used to distinguish assertions and assumptions) */ void addFormula(TNode n, - bool inUnsatCore, bool inInput, bool isAssumption, bool isFunDef, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 5f0da7a0c..36bc17096 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -343,17 +343,14 @@ void EchoCommand::toStream(std::ostream& out, /* class AssertCommand */ /* -------------------------------------------------------------------------- */ -AssertCommand::AssertCommand(const api::Term& t, bool inUnsatCore) - : d_term(t), d_inUnsatCore(inUnsatCore) -{ -} +AssertCommand::AssertCommand(const api::Term& t) : d_term(t) {} api::Term AssertCommand::getTerm() const { return d_term; } void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->getSmtEngine()->assertFormula(termToNode(d_term), d_inUnsatCore); + solver->assertFormula(d_term); d_commandStatus = CommandSuccess::instance(); } catch (UnsafeInterruptException& e) @@ -366,10 +363,7 @@ void AssertCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -Command* AssertCommand::clone() const -{ - return new AssertCommand(d_term, d_inUnsatCore); -} +Command* AssertCommand::clone() const { return new AssertCommand(d_term); } std::string AssertCommand::getCommandName() const { return "assert"; } @@ -581,10 +575,7 @@ void CheckSatAssumingCommand::toStream(std::ostream& out, /* class QueryCommand */ /* -------------------------------------------------------------------------- */ -QueryCommand::QueryCommand(const api::Term& t, bool inUnsatCore) - : d_term(t), d_inUnsatCore(inUnsatCore) -{ -} +QueryCommand::QueryCommand(const api::Term& t) : d_term(t) {} api::Term QueryCommand::getTerm() const { return d_term; } void QueryCommand::invoke(api::Solver* solver, SymbolManager* sm) @@ -615,7 +606,7 @@ void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const Command* QueryCommand::clone() const { - QueryCommand* c = new QueryCommand(d_term, d_inUnsatCore); + QueryCommand* c = new QueryCommand(d_term); c->d_result = d_result; return c; } diff --git a/src/smt/command.h b/src/smt/command.h index 2d32062e2..590fcace3 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -348,10 +348,9 @@ class CVC5_EXPORT AssertCommand : public Command { protected: api::Term d_term; - bool d_inUnsatCore; public: - AssertCommand(const api::Term& t, bool inUnsatCore = true); + AssertCommand(const api::Term& t); api::Term getTerm() const; @@ -706,10 +705,9 @@ class CVC5_EXPORT QueryCommand : public Command protected: api::Term d_term; api::Result d_result; - bool d_inUnsatCore; public: - QueryCommand(const api::Term& t, bool inUnsatCore = true); + QueryCommand(const api::Term& t); api::Term getTerm() const; api::Result getResult() const; diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index e66717f5b..185a60e46 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -75,8 +75,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as, Assert(ne.getNumChildren() == 3); // We consider this to be an entailment check, which also avoids incorrect // status reporting (see SmtEngineState::d_expectedStatus). - Result r = - d_smtSolver.checkSatisfiability(as, std::vector{ne}, false, true); + Result r = d_smtSolver.checkSatisfiability(as, std::vector{ne}, true); Trace("smt-qe") << "Query returned " << r << std::endl; if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b9ed95339..774d8b192 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -831,7 +831,7 @@ Result SmtEngine::checkSat() return checkSat(nullNode); } -Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore) +Result SmtEngine::checkSat(const Node& assumption) { if (Dump.isOn("benchmark")) { @@ -843,11 +843,10 @@ Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore) { assump.push_back(assumption); } - return checkSatInternal(assump, inUnsatCore, false); + return checkSatInternal(assump, false); } -Result SmtEngine::checkSat(const std::vector& assumptions, - bool inUnsatCore) +Result SmtEngine::checkSat(const std::vector& assumptions) { if (Dump.isOn("benchmark")) { @@ -861,10 +860,10 @@ Result SmtEngine::checkSat(const std::vector& assumptions, assumptions); } } - return checkSatInternal(assumptions, inUnsatCore, false); + return checkSatInternal(assumptions, false); } -Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore) +Result SmtEngine::checkEntailed(const Node& node) { if (Dump.isOn("benchmark")) { @@ -872,19 +871,16 @@ Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore) } return checkSatInternal( node.isNull() ? std::vector() : std::vector{node}, - inUnsatCore, true) .asEntailmentResult(); } -Result SmtEngine::checkEntailed(const std::vector& nodes, - bool inUnsatCore) +Result SmtEngine::checkEntailed(const std::vector& nodes) { - return checkSatInternal(nodes, inUnsatCore, true).asEntailmentResult(); + return checkSatInternal(nodes, true).asEntailmentResult(); } Result SmtEngine::checkSatInternal(const std::vector& assumptions, - bool inUnsatCore, bool isEntailmentCheck) { try @@ -897,7 +893,7 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, << assumptions << ")" << endl; // check the satisfiability with the solver object Result r = d_smtSolver->checkSatisfiability( - *d_asserts.get(), assumptions, inUnsatCore, isEntailmentCheck); + *d_asserts.get(), assumptions, isEntailmentCheck); Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; @@ -995,7 +991,7 @@ std::vector SmtEngine::getUnsatAssumptions(void) return res; } -Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) +Result SmtEngine::assertFormula(const Node& formula) { SmtScope smts(this); finishInit(); @@ -1011,7 +1007,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) // Substitute out any abstract values in ex Node n = d_absValues->substituteAbstractValues(formula); - d_asserts->assertFormula(n, inUnsatCore); + d_asserts->assertFormula(n); return quickCheck().asEntailmentResult(); }/* SmtEngine::assertFormula() */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 357f60b85..68b1caad0 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -359,13 +359,12 @@ class CVC5_EXPORT SmtEngine * Add a formula to the current context: preprocess, do per-theory * setup, use processAssertionList(), asserting to T-solver for * literals and conjunction of literals. Returns false if - * immediately determined to be inconsistent. This version - * takes a Boolean flag to determine whether to include this asserted - * formula in an unsat core (if one is later requested). + * immediately determined to be inconsistent. Note this formula will + * be included in the unsat core when applicable. * * @throw TypeCheckingException, LogicException, UnsafeInterruptException */ - Result assertFormula(const Node& formula, bool inUnsatCore = true); + Result assertFormula(const Node& formula); /** * Reduce an unsatisfiable core to make it minimal. @@ -380,9 +379,8 @@ class CVC5_EXPORT SmtEngine * * @throw Exception */ - Result checkEntailed(const Node& assumption, bool inUnsatCore = true); - Result checkEntailed(const std::vector& assumptions, - bool inUnsatCore = true); + Result checkEntailed(const Node& assumption); + Result checkEntailed(const std::vector& assumptions); /** * Assert a formula (if provided) to the current context and call @@ -391,9 +389,8 @@ class CVC5_EXPORT SmtEngine * @throw Exception */ Result checkSat(); - Result checkSat(const Node& assumption, bool inUnsatCore = true); - Result checkSat(const std::vector& assumptions, - bool inUnsatCore = true); + Result checkSat(const Node& assumption); + Result checkSat(const std::vector& assumptions); /** * Returns a set of so-called "failed" assumptions. @@ -1008,7 +1005,6 @@ class CVC5_EXPORT SmtEngine * Check satisfiability (used to check satisfiability and entailment). */ Result checkSatInternal(const std::vector& assumptions, - bool inUnsatCore, bool isEntailmentCheck); /** diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index f5783ab6b..6d3326603 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -133,7 +133,6 @@ void SmtSolver::shutdown() Result SmtSolver::checkSatisfiability(Assertions& as, const std::vector& assumptions, - bool inUnsatCore, bool isEntailmentCheck) { // update the state to indicate we are about to run a check-sat @@ -141,7 +140,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, d_state.notifyCheckSat(hasAssumptions); // then, initialize the assertions - as.initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck); + as.initializeCheckSat(assumptions, isEntailmentCheck); // make the check Assert(d_smt.isFullyInited()); diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 01e52fbfa..ea89f6d57 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -103,13 +103,11 @@ class SmtSolver * during this call. * @param assumptions The assumptions for this check-sat call, which are * temporary assertions. - * @param inUnsatCore Whether assumptions are in the unsat core. * @param isEntailmentCheck Whether this is an entailment check (assumptions * are negated in this case). */ Result checkSatisfiability(Assertions& as, const std::vector& assumptions, - bool inUnsatCore, bool isEntailmentCheck); /** * Process the assertions that have been asserted in as. This moves the set of diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 98278ef9e..d5cfe274e 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -221,7 +221,7 @@ Result SygusSolver::checkSynth(Assertions& as) query.push_back(body); } - Result r = d_smtSolver.checkSatisfiability(as, query, false, false); + Result r = d_smtSolver.checkSatisfiability(as, query, false); // Check that synthesis solutions satisfy the conjecture if (options::checkSynthSol() -- 2.30.2