From 49853e244323fa1964d69621506aa5daf8177a9c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 30 Jul 2019 13:52:28 -0500 Subject: [PATCH] Track solver execution mode (#3132) --- src/smt/smt_engine.cpp | 76 ++++++++++++++++++++++++++---------------- src/smt/smt_engine.h | 44 ++++++++++++++++++------ 2 files changed, 80 insertions(+), 40 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4a8803392..f75726be2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -869,13 +869,13 @@ SmtEngine::SmtEngine(ExprManager* em) d_isInternalSubsolver(false), d_pendingPops(0), d_fullyInited(false), - d_problemExtended(false), d_queryMade(false), d_needPostsolve(false), d_earlyTheoryPP(true), d_globalNegation(false), d_status(), d_expectedStatus(), + d_smtMode(SMT_MODE_START), d_replayStream(NULL), d_private(NULL), d_statisticsRegistry(NULL), @@ -2334,10 +2334,10 @@ void SmtEngine::setDefaults() { } } -void SmtEngine::setProblemExtended(bool value) +void SmtEngine::setProblemExtended() { - d_problemExtended = value; - if (value) { d_assumptions.clear(); } + d_smtMode = SMT_MODE_ASSERT; + d_assumptions.clear(); } void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) @@ -3071,8 +3071,7 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (d_status.isNull() || d_status.asSatisfiabilityResult() == Result::UNSAT - || d_problemExtended) + if (d_smtMode != SMT_MODE_SAT) { std::stringstream ss; ss << "Cannot " << c @@ -3666,7 +3665,7 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, bool didInternalPush = false; - setProblemExtended(true); + setProblemExtended(); if (isQuery) { @@ -3771,6 +3770,7 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, // Remember the status d_status = r; + // Check against expected status if (!d_expectedStatus.isUnknown() && !d_status.isUnknown() && d_status != d_expectedStatus) { @@ -3778,8 +3778,17 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, << d_status; } d_expectedStatus = Result(); - - setProblemExtended(false); + // Update the SMT mode + if (d_status.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + d_smtMode = SMT_MODE_UNSAT; + } + else + { + // Notice that unknown response moves to sat mode, since the same set + // of commands (get-model, get-value) are applicable to this case. + d_smtMode = SMT_MODE_SAT; + } Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; @@ -3831,9 +3840,7 @@ vector SmtEngine::getUnsatAssumptions(void) "Cannot get unsat assumptions when produce-unsat-assumptions option " "is off."); } - if (d_status.isNull() - || d_status.asSatisfiabilityResult() != Result::UNSAT - || d_problemExtended) + if (d_smtMode != SMT_MODE_UNSAT) { throw RecoverableModalException( "Cannot get unsat assumptions unless immediately preceded by " @@ -4175,9 +4182,8 @@ Expr SmtEngine::getValue(const Expr& ex) const "Cannot get value when produce-models options is off."; throw ModalException(msg); } - if(d_status.isNull() || - d_status.asSatisfiabilityResult() == Result::UNSAT || - d_problemExtended) { + if (d_smtMode != SMT_MODE_SAT) + { const char* msg = "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response."; throw RecoverableModalException(msg); @@ -4298,9 +4304,8 @@ vector> SmtEngine::getAssignment() "produce-assignments option is off."; throw ModalException(msg); } - if(d_status.isNull() || - d_status.asSatisfiabilityResult() == Result::UNSAT || - d_problemExtended) { + if (d_smtMode != SMT_MODE_SAT) + { const char* msg = "Cannot get the current assignment unless immediately " "preceded by SAT/INVALID or UNKNOWN response."; @@ -4552,8 +4557,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() throw ModalException( "Cannot get an unsat core when produce-unsat-cores option is off."); } - if (d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT - || d_problemExtended) + if (d_smtMode != SMT_MODE_UNSAT) { throw RecoverableModalException( "Cannot get an unsat core unless immediately preceded by UNSAT/VALID " @@ -4943,9 +4947,8 @@ const Proof& SmtEngine::getProof() if(!options::proof()) { throw ModalException("Cannot get a proof when produce-proofs option is off."); } - if(d_status.isNull() || - d_status.asSatisfiabilityResult() != Result::UNSAT || - d_problemExtended) { + if (d_smtMode != SMT_MODE_UNSAT) + { throw RecoverableModalException( "Cannot get a proof unless immediately preceded by UNSAT/VALID " "response."); @@ -5107,6 +5110,21 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) d_subsolver->setLogic(l); // assert the abduction query d_subsolver->assertFormula(aconj.toExpr()); + if (getAbductInternal(abd)) + { + // successfully generated an abduct, update to abduct state + d_smtMode = SMT_MODE_ABDUCT; + return true; + } + // failed, we revert to the assert state + d_smtMode = SMT_MODE_ASSERT; + return false; +} + +bool SmtEngine::getAbductInternal(Expr& abd) +{ + // should have initialized the subsolver by now + Assert(d_subsolver != nullptr); Trace("sygus-abduct") << " SmtEngine::getAbduct check sat..." << std::endl; Result r = d_subsolver->checkSat(); Trace("sygus-abduct") << " SmtEngine::getAbduct result: " << r << std::endl; @@ -5119,13 +5137,14 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) std::map::iterator its = sols.find(d_sssf); if (its != sols.end()) { - Node abdn = Node::fromExpr(its->second); Trace("sygus-abduct") - << "SmtEngine::getAbduct: solution is " << abdn << std::endl; + << "SmtEngine::getAbduct: solution is " << its->second << std::endl; + Node abdn = Node::fromExpr(its->second); if (abdn.getKind() == kind::LAMBDA) { abdn = abdn[1]; } + Assert(d_sssfVarlist.size() == d_sssfSyms.size()); // convert back to original // must replace formal arguments of abd with the free variables in the // input problem that they correspond to. @@ -5136,7 +5155,6 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) // convert to expression abd = abdn.toExpr(); - return true; } Trace("sygus-abduct") << "SmtEngine::getAbduct: could not find solution!" @@ -5232,8 +5250,8 @@ void SmtEngine::push() // The problem isn't really "extended" yet, but this disallows // get-model after a push, simplifying our lives somewhat and - // staying symmtric with pop. - setProblemExtended(true); + // staying symmetric with pop. + setProblemExtended(); d_userLevels.push_back(d_userContext->getLevel()); internalPush(); @@ -5261,7 +5279,7 @@ void SmtEngine::pop() { // but also it would be weird to have a legally-executed (get-model) // that only returns a subset of the assignment (because the rest // is no longer in scope!). - setProblemExtended(true); + setProblemExtended(); AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 316ca16d1..9f56a1cd3 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -253,13 +253,6 @@ class CVC4_PUBLIC SmtEngine { */ bool d_fullyInited; - /** - * Whether or not we have added any assertions/declarations/definitions, - * or done push/pop, since the last checkSat/query, and therefore we're - * not responsible for models or proofs. - */ - bool d_problemExtended; - /** * Whether or not a query() or checkSat() has already been made through * this SmtEngine. If true, and incrementalSolving is false, then @@ -295,6 +288,26 @@ class CVC4_PUBLIC SmtEngine { */ Result d_expectedStatus; + /** + * The current mode of the solver, see Figure 4.1 on page 52 of the + * SMT-LIB version 2.6 standard + * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf + */ + enum SmtMode + { + // the initial state of the solver + SMT_MODE_START, + // normal state of the solver, after assert/push/pop/declare/define + SMT_MODE_ASSERT, + // immediately after a check-sat returning "sat" or "unknown" + SMT_MODE_SAT, + // immediately after a check-sat returning "unsat" + SMT_MODE_UNSAT, + // immediately after a successful call to get-abduct + SMT_MODE_ABDUCT + }; + SmtMode d_smtMode; + /** * The input file name (if any) or the name set through setInfo (if any) */ @@ -370,11 +383,11 @@ class CVC4_PUBLIC SmtEngine { void setDefaults(); /** - * Sets d_problemExtended to the given value. - * If d_problemExtended is set to true, the list of assumptions from the - * previous call to checkSatisfiability is cleared. + * Sets that the problem has been extended. This sets the smt mode of the + * solver to SMT_MODE_ASSERT, and clears the list of assumptions from the + * previous call to checkSatisfiability. */ - void setProblemExtended(bool value); + void setProblemExtended(); /** * Create theory engine, prop engine, decision engine. Called by @@ -482,6 +495,15 @@ class CVC4_PUBLIC SmtEngine { void debugCheckFunctionBody(Expr formula, const std::vector& formals, Expr func); + /** get abduct internal + * + * Gets the next abduct from the internal subsolver d_subsolver. If + * successful, this method returns true and sets abd to that abduct. + * + * This method assumes d_subsolver has been initialized to do abduction + * problems. + */ + bool getAbductInternal(Expr& abd); /** * Helper method to obtain both the heap and nil from the solver. Returns a -- 2.30.2