diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 94 |
1 files changed, 67 insertions, 27 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ae00b4caf..d3489b301 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2144,6 +2144,12 @@ void SmtEngine::setDefaults() { } } +void SmtEngine::setProblemExtended(bool value) +{ + d_problemExtended = value; + if (value) { d_assumptions.clear(); } +} + void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) { SmtScope smts(this); @@ -4693,25 +4699,25 @@ void SmtEngine::ensureBoolean(const Expr& e) } } -Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) +Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { - return checkSatisfiability(ex, inUnsatCore, false); + return checkSatisfiability(assumption, inUnsatCore, false); } -Result SmtEngine::checkSat(const vector<Expr>& exprs, bool inUnsatCore) +Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) { - return checkSatisfiability(exprs, inUnsatCore, false); + return checkSatisfiability(assumptions, inUnsatCore, false); } -Result SmtEngine::query(const Expr& ex, bool inUnsatCore) +Result SmtEngine::query(const Expr& assumption, bool inUnsatCore) { - Assert(!ex.isNull()); - return checkSatisfiability(ex, inUnsatCore, true); + Assert(!assumption.isNull()); + return checkSatisfiability(assumption, inUnsatCore, true); } -Result SmtEngine::query(const vector<Expr>& exprs, bool inUnsatCore) +Result SmtEngine::query(const vector<Expr>& assumptions, bool inUnsatCore) { - return checkSatisfiability(exprs, inUnsatCore, true); + return checkSatisfiability(assumptions, inUnsatCore, true); } Result SmtEngine::checkSatisfiability(const Expr& expr, @@ -4724,7 +4730,7 @@ Result SmtEngine::checkSatisfiability(const Expr& expr, isQuery); } -Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs, +Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, bool inUnsatCore, bool isQuery) { @@ -4735,7 +4741,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs, doPendingPops(); Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" - << exprs << ")" << endl; + << assumptions << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { throw ModalException("Cannot make multiple queries unless " @@ -4755,29 +4761,31 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs, bool didInternalPush = false; - vector<Expr> t_exprs; + setProblemExtended(true); + if (isQuery) { - size_t size = exprs.size(); + size_t size = assumptions.size(); if (size > 1) { - /* Assume: not (BIGAND exprs) */ - t_exprs.push_back(d_exprManager->mkExpr(kind::AND, exprs).notExpr()); + /* Assume: not (BIGAND assumptions) */ + d_assumptions.push_back( + d_exprManager->mkExpr(kind::AND, assumptions).notExpr()); } else if (size == 1) { /* Assume: not expr */ - t_exprs.push_back(exprs[0].notExpr()); + d_assumptions.push_back(assumptions[0].notExpr()); } } else { - /* Assume: BIGAND exprs */ - t_exprs = exprs; + /* Assume: BIGAND assumptions */ + d_assumptions = assumptions; } Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - for (Expr e : t_exprs) + for (Expr e : d_assumptions) { // Substitute out any abstract values in ex. e = d_private->substituteAbstractValues(Node::fromExpr(e)).toExpr(); @@ -4788,7 +4796,6 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs, /* Add assumption */ internalPush(); didInternalPush = true; - d_problemExtended = true; if (d_assertionList != NULL) { d_assertionList->push_back(e); @@ -4832,13 +4839,14 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs, if (Dump.isOn("benchmark")) { // the expr already got dumped out if assertion-dumping is on - if (isQuery && exprs.size() == 1) + if (isQuery && assumptions.size() == 1) { - Dump("benchmark") << QueryCommand(exprs[0]); + Dump("benchmark") << QueryCommand(assumptions[0]); } else { - Dump("benchmark") << CheckSatAssumingCommand(t_exprs, inUnsatCore); + Dump("benchmark") << CheckSatAssumingCommand(d_assumptions, + inUnsatCore); } } @@ -4851,10 +4859,10 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs, // Remember the status d_status = r; - d_problemExtended = false; + setProblemExtended(false); Trace("smt") << "SmtEngine::" << (isQuery ? "query" : "checkSat") << "(" - << exprs << ") => " << r << endl; + << assumptions << ") => " << r << endl; // Check that SAT results generate a model correctly. if(options::checkModels()) { @@ -4893,6 +4901,38 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& exprs, } } +vector<Expr> SmtEngine::getUnsatAssumptions(void) +{ + Trace("smt") << "SMT getUnsatAssumptions()" << endl; + SmtScope smts(this); + if (!options::unsatAssumptions()) + { + throw ModalException( + "Cannot get unsat assumptions when produce-unsat-assumptions option " + "is off."); + } + if (d_status.isNull() + || d_status.asSatisfiabilityResult() != Result::UNSAT + || d_problemExtended) + { + throw RecoverableModalException( + "Cannot get unsat assumptions unless immediately preceded by " + "UNSAT/VALID response."); + } + finalOptionsAreSet(); + if (Dump.isOn("benchmark")) + { + Dump("benchmark") << GetUnsatCoreCommand(); + } + UnsatCore core = getUnsatCore(); + vector<Expr> res; + for (const Expr& e : d_assumptions) + { + if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); } + } + return res; +} + Result SmtEngine::checkSynth(const Expr& e) { SmtScope smts(this); @@ -5890,7 +5930,7 @@ 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. - d_problemExtended = true; + setProblemExtended(true); d_userLevels.push_back(d_userContext->getLevel()); internalPush(); @@ -5924,7 +5964,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!). - d_problemExtended = true; + setProblemExtended(true); AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); |