diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 328 |
1 files changed, 85 insertions, 243 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e5b95d656..43aa3b0c8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -82,6 +82,7 @@ #include "prop/prop_engine.h" #include "smt/abduction_solver.h" #include "smt/abstract_values.h" +#include "smt/assertions.h" #include "smt/expr_names.h" #include "smt/command.h" #include "smt/defined_function.h" @@ -162,9 +163,6 @@ class SmtEnginePrivate /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; - /** Assertions in the preprocessing pipeline */ - AssertionPipeline d_assertions; - /** Whether any assertions have been processed */ CDO<bool> d_assertionsProcessed; @@ -178,7 +176,6 @@ class SmtEnginePrivate ProcessAssertions d_processor; public: - IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); } /** Instance of the ITE remover */ RemoveTermFormulas d_iteRemover; @@ -208,7 +205,6 @@ class SmtEnginePrivate SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), d_propagator(true, true), - d_assertions(), d_assertionsProcessed(smt.getUserContext(), false), d_processor(smt, *smt.getResourceManager()), d_iteRemover(smt.getUserContext()), @@ -241,12 +237,11 @@ class SmtEnginePrivate /** * Process the assertions that have been asserted. */ - void processAssertions(); + void processAssertions(Assertions& as); /** Process a user push. */ void notifyPush() { - } /** @@ -256,32 +251,8 @@ class SmtEnginePrivate * last map of expression names from notifyPush. */ void notifyPop() { - d_assertions.clear(); d_propagator.getLearnedLiterals().clear(); - getIteSkolemMap().clear(); } - - /** - * Adds a formula to the current context. Action here depends on - * the SimplificationMode (in the current Options scope); the - * formula might be pushed out to the propositional layer - * immediately, or it might be simplified and kept, or it might not - * even be simplified. - * The arguments isInput and isAssumption are used for bookkeeping for proofs. - * The argument maybeHasFv should be set to true if the assertion may have - * free variables. By construction, assertions from the smt2 parser are - * guaranteed not to have free variables. However, other cases such as - * assertions from the SyGuS parser may have free variables (say if the - * input contains an assert or define-fun-rec command). - * - * @param isAssumption If true, the formula is considered to be an assumption - * (this is used to distinguish assertions and assumptions) - */ - void addFormula(TNode n, - bool inUnsatCore, - bool inInput = true, - bool isAssumption = false, - bool maybeHasFv = false); /** * Simplify node "in" by expanding definitions and applying any * substitutions learned from preprocessing. @@ -291,8 +262,6 @@ class SmtEnginePrivate // Expand definitions. NodeToNodeHashMap cache; Node n = d_processor.expandDefinitions(in, cache).toExpr(); - // Make sure we've done all preprocessing, etc. - Assert(d_assertions.size() == 0); return applySubstitutions(n).toExpr(); } };/* class SmtEnginePrivate */ @@ -306,6 +275,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), d_absValues(new AbstractValues(d_nodeManager)), + d_asserts(new Assertions(d_userContext.get(), *d_absValues.get())), d_exprNames(new ExprNames(d_userContext.get())), d_dumpm(new DumpManager(d_userContext.get())), d_routListener(new ResourceOutListener(*this)), @@ -316,7 +286,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), d_abductSolver(nullptr), - d_assertionList(nullptr), d_assignments(nullptr), d_defineCommands(), d_logic(), @@ -326,7 +295,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_fullyInited(false), d_queryMade(false), d_needPostsolve(false), - d_globalNegation(false), d_status(), d_expectedStatus(), d_smtMode(SMT_MODE_START), @@ -434,18 +402,8 @@ void SmtEngine::finishInit() d_userContext->push(); d_context->push(); - Trace("smt-debug") << "Set up assertion list..." << std::endl; - // [MGD 10/20/2011] keep around in incremental mode, due to a - // cleanup ordering issue and Nodes/TNodes. If SAT is popped - // first, some user-context-dependent TNodes might still exist - // with rc == 0. - if(options::produceAssertions() || - options::incrementalSolving()) { - // In the case of incremental solving, we appear to need these to - // ensure the relevant Nodes remain live. - d_assertionList = new (true) AssertionList(getUserContext()); - d_globalDefineFunRecLemmas.reset(new std::vector<Node>()); - } + Trace("smt-debug") << "Set up assertions..." << std::endl; + d_asserts->finishInit(); // dump out a set-logic command only when raw-benchmark is disabled to avoid // dumping the command twice. @@ -534,12 +492,6 @@ SmtEngine::~SmtEngine() d_assignments->deleteSelf(); } - d_globalDefineFunRecLemmas.reset(); - - if(d_assertionList != NULL) { - d_assertionList->deleteSelf(); - } - d_definedFunctions->deleteSelf(); //destroy all passes before destroying things that they refer to @@ -557,6 +509,7 @@ SmtEngine::~SmtEngine() #endif d_absValues.reset(nullptr); + d_asserts.reset(nullptr); d_exprNames.reset(nullptr); d_dumpm.reset(nullptr); @@ -647,12 +600,6 @@ void SmtEngine::setLogicInternal() d_userLogic.lock(); } -void SmtEngine::setProblemExtended() -{ - d_smtMode = SMT_MODE_ASSERT; - d_assumptions.clear(); -} - void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) { SmtScope smts(this); @@ -983,7 +930,6 @@ void SmtEngine::defineFunctionsRec( } ExprManager* em = getExprManager(); - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); for (unsigned i = 0, size = funcs.size(); i < size; i++) { // we assert a quantified formula @@ -1018,22 +964,9 @@ void SmtEngine::defineFunctionsRec( // assert the quantified formula // notice we don't call assertFormula directly, since this would // duplicate the output on raw-benchmark. - Node n = d_absValues->substituteAbstractValues(Node::fromExpr(lem)); - if (d_assertionList != nullptr) - { - d_assertionList->push_back(n); - } - if (global && d_globalDefineFunRecLemmas != nullptr) - { - // Global definitions are asserted at check-sat-time because we have to - // make sure that they are always present - Assert(!language::isInputLangSygus(options::inputLanguage())); - d_globalDefineFunRecLemmas->emplace_back(n); - } - else - { - d_private->addFormula(n, false, true, false, maybeHasFv); - } + Node lemn = Node::fromExpr(lem); + // add define recursive definition to the assertions + d_asserts->addDefineFunRecDefinition(lemn, global); } } @@ -1084,7 +1017,7 @@ Result SmtEngine::check() { // Make sure the prop layer has all of the assertions Trace("smt") << "SmtEngine::check(): processing assertions" << endl; - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); @@ -1147,13 +1080,17 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const return m; } -void SmtEnginePrivate::processAssertions() { +void SmtEnginePrivate::processAssertions(Assertions& as) +{ TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); spendResource(ResourceManager::Resource::PreprocessStep); Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); - if (d_assertions.size() == 0) { + AssertionPipeline& ap = as.getAssertionPipeline(); + + if (ap.size() == 0) + { // nothing to do return; } @@ -1161,24 +1098,24 @@ void SmtEnginePrivate::processAssertions() { // TODO(b/1255): Substitutions in incremental mode should be managed with a // proper data structure. - d_assertions.enableStoreSubstsInAsserts(); + ap.enableStoreSubstsInAsserts(); } else { - d_assertions.disableStoreSubstsInAsserts(); + ap.disableStoreSubstsInAsserts(); } // process the assertions - bool noConflict = d_processor.apply(d_assertions); + bool noConflict = d_processor.apply(as); //notify theory engine new preprocessed assertions - d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() ); + d_smt.d_theoryEngine->notifyPreprocessedAssertions(ap.ref()); // Push the formula to decision engine if (noConflict) { Chat() << "pushing to decision engine..." << endl; - d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions); + d_smt.d_propEngine->addAssertionsToDecisionEngine(ap); } // end: INVARIANT to maintain: no reordering of assertions or @@ -1187,91 +1124,30 @@ void SmtEnginePrivate::processAssertions() { // if incremental, compute which variables are assigned if (options::incrementalSolving()) { - d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref()); + d_preprocessingPassContext->recordSymbolsInAssertions(ap.ref()); } // Push the formula to SAT { Chat() << "converting to CNF..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - Chat() << "+ " << d_assertions[i] << std::endl; - d_smt.d_propEngine->assertFormula(d_assertions[i]); - } - } - - d_assertionsProcessed = true; - - d_assertions.clear(); - getIteSkolemMap().clear(); -} - -void SmtEnginePrivate::addFormula( - TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv) -{ - if (n == d_true) { - // nothing to do - return; - } - - Trace("smt") << "SmtEnginePrivate::addFormula(" << n - << "), inUnsatCore = " << inUnsatCore - << ", inInput = " << inInput - << ", isAssumption = " << isAssumption << endl; - - // Ensure that it does not contain free variables - if (maybeHasFv) - { - if (expr::hasFreeVar(n)) + for (const Node& assertion : ap.ref()) { - std::stringstream se; - se << "Cannot process assertion with free variable."; - if (language::isInputLangSygus(options::inputLanguage())) - { - // Common misuse of SyGuS is to use top-level assert instead of - // constraint when defining the synthesis conjecture. - se << " Perhaps you meant `constraint` instead of `assert`?"; - } - throw ModalException(se.str().c_str()); + Chat() << "+ " << assertion << std::endl; + d_smt.d_propEngine->assertFormula(assertion); } } - // Give it to proof manager - PROOF( - if( inInput ){ - // n is an input assertion - if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) { - - ProofManager::currentPM()->addCoreAssertion(n.toExpr()); - } - }else{ - // n is the result of an unknown preprocessing step, add it to dependency map to null - ProofManager::currentPM()->addDependence(n, Node::null()); - } - ); - - // Add the normalized formula to the queue - d_assertions.push_back(n, isAssumption); - //d_assertions.push_back(Rewriter::rewrite(n)); -} + d_assertionsProcessed = true; -void SmtEngine::ensureBoolean(const Node& n) -{ - TypeNode type = n.getType(options::typeChecking()); - TypeNode boolType = NodeManager::currentNM()->booleanType(); - if(type != boolType) { - stringstream ss; - ss << "Expected " << boolType << "\n" - << "The assertion : " << n << "\n" - << "Its type : " << type; - throw TypeCheckingException(n.toExpr(), ss.str()); - } + // clear the current assertions + as.clearCurrent(); } Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore) { Dump("benchmark") << CheckSatCommand(assumption); - return checkSatisfiability(assumption, inUnsatCore, false); + return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false); } Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) @@ -1284,36 +1160,46 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore) { Dump("benchmark") << CheckSatAssumingCommand(assumptions); } - - return checkSatisfiability(assumptions, inUnsatCore, false); + std::vector<Node> assumps; + for (const Expr& e : assumptions) + { + assumps.push_back(Node::fromExpr(e)); + } + return checkSatisfiability(assumps, inUnsatCore, false); } -Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore) +Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore) { - Dump("benchmark") << QueryCommand(expr, inUnsatCore); - return checkSatisfiability( - expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, - inUnsatCore, - true) + Dump("benchmark") << QueryCommand(node, inUnsatCore); + return checkSatisfiability(node.isNull() + ? std::vector<Node>() + : std::vector<Node>{Node::fromExpr(node)}, + inUnsatCore, + true) .asEntailmentResult(); } -Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore) +Result SmtEngine::checkEntailed(const vector<Expr>& nodes, bool inUnsatCore) { - return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult(); + std::vector<Node> ns; + for (const Expr& e : nodes) + { + ns.push_back(Node::fromExpr(e)); + } + return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult(); } -Result SmtEngine::checkSatisfiability(const Expr& expr, +Result SmtEngine::checkSatisfiability(const Node& node, bool inUnsatCore, bool isEntailmentCheck) { return checkSatisfiability( - expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr}, + node.isNull() ? std::vector<Node>() : std::vector<Node>{node}, inUnsatCore, isEntailmentCheck); } -Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, +Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions, bool inUnsatCore, bool isEntailmentCheck) { @@ -1333,70 +1219,23 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, "(try --incremental)"); } - // Note that a query has been made + // Note that a query has been made and we are in assert mode d_queryMade = true; - // reset global negation - d_globalNegation = false; + d_smtMode = SMT_MODE_ASSERT; + // push if there are assumptions bool didInternalPush = false; - - setProblemExtended(); - - if (isEntailmentCheck) - { - size_t size = assumptions.size(); - if (size > 1) - { - /* Assume: not (BIGAND assumptions) */ - d_assumptions.push_back( - d_exprManager->mkExpr(kind::AND, assumptions).notExpr()); - } - else if (size == 1) - { - /* Assume: not expr */ - d_assumptions.push_back(assumptions[0].notExpr()); - } - } - else - { - /* Assume: BIGAND assumptions */ - d_assumptions = assumptions; - } - - if (!d_assumptions.empty()) + if (!assumptions.empty()) { internalPush(); didInternalPush = true; } - Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - for (Expr e : d_assumptions) - { - // Substitute out any abstract values in ex. - Node n = d_absValues->substituteAbstractValues(Node::fromExpr(e)); - // Ensure expr is type-checked at this point. - ensureBoolean(n); + // then, initialize the assertions + d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck); - /* Add assumption */ - if (d_assertionList != NULL) - { - d_assertionList->push_back(n); - } - d_private->addFormula(n, inUnsatCore, true, true); - } - - if (d_globalDefineFunRecLemmas != nullptr) - { - // Global definitions are asserted at check-sat-time because we have to - // make sure that they are always present (they are essentially level - // zero assertions) - for (const Node& lemma : *d_globalDefineFunRecLemmas) - { - d_private->addFormula(lemma, false, true, false, false); - } - } - - r = check(); + // make the check + Result r = check(); if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -1404,7 +1243,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); } // flipped if we did a global negation - if (d_globalNegation) + if (d_asserts->isGlobalNegated()) { Trace("smt") << "SmtEngine::process global negate " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -1492,7 +1331,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, } } -vector<Expr> SmtEngine::getUnsatAssumptions(void) +std::vector<Node> SmtEngine::getUnsatAssumptions(void) { Trace("smt") << "SMT getUnsatAssumptions()" << endl; SmtScope smts(this); @@ -1514,10 +1353,14 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void) Dump("benchmark") << GetUnsatAssumptionsCommand(); } UnsatCore core = getUnsatCoreInternal(); - vector<Expr> res; - for (const Expr& e : d_assumptions) + std::vector<Node> res; + std::vector<Node>& assumps = d_asserts->getAssumptions(); + for (const Node& e : assumps) { - if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); } + if (std::find(core.begin(), core.end(), e.toExpr()) != core.end()) + { + res.push_back(e); + } } return res; } @@ -1537,12 +1380,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) // Substitute out any abstract values in ex Node n = d_absValues->substituteAbstractValues(formula); - ensureBoolean(n); - if(d_assertionList != NULL) { - d_assertionList->push_back(n); - } - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); - d_private->addFormula(n, inUnsatCore, true, false, maybeHasFv); + d_asserts->assertFormula(n, inUnsatCore); return quickCheck().asEntailmentResult(); }/* SmtEngine::assertFormula() */ @@ -1801,7 +1639,7 @@ Expr SmtEngine::simplify(const Expr& ex) } // Make sure all preprocessing is done - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); Node n = d_private->simplify(Node::fromExpr(e)); n = postprocess(n, TypeNode::fromType(e.getType())); return n.toExpr(); @@ -2233,9 +2071,10 @@ void SmtEngine::checkUnsatCore() { } void SmtEngine::checkModel(bool hardFailure) { + context::CDList<Node>* al = d_asserts->getAssertionList(); // --check-model implies --produce-assertions, which enables the // assertion list, so we should be ok. - Assert(d_assertionList != NULL) + Assert(al != nullptr) << "don't have an assertion list to check in SmtEngine::checkModel()"; TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); @@ -2354,7 +2193,7 @@ void SmtEngine::checkModel(bool hardFailure) { } // Now go through all our user assertions checking if they're satisfied. - for (const Node& assertion : *d_assertionList) + for (const Node& assertion : *al) { Notice() << "SmtEngine::checkModel(): checking assertion " << assertion << endl; @@ -2507,7 +2346,8 @@ void SmtEngine::checkSynthSolution() Trace("check-synth-sol") << "Retrieving assertions\n"; // Build conjecture from original assertions - if (d_assertionList == NULL) + context::CDList<Node>* al = d_asserts->getAssertionList(); + if (al == nullptr) { Trace("check-synth-sol") << "No assertions to check\n"; return; @@ -2516,7 +2356,7 @@ void SmtEngine::checkSynthSolution() std::vector<Node> auxAssertions; // expand definitions cache std::unordered_map<Node, Node, NodeHashFunction> cache; - for (const Node& assertion : *d_assertionList) + for (const Node& assertion : *al) { Notice() << "SmtEngine::checkSynthSolution(): checking assertion " << assertion << endl; @@ -2857,9 +2697,10 @@ vector<Expr> SmtEngine::getAssertions() { "Cannot query the current assertion list when not in produce-assertions mode."; throw ModalException(msg); } - Assert(d_assertionList != NULL); + context::CDList<Node>* al = d_asserts->getAssertionList(); + Assert(al != nullptr); std::vector<Expr> res; - for (const Node& n : *d_assertionList) + for (const Node& n : *al) { res.emplace_back(n.toExpr()); } @@ -2874,7 +2715,7 @@ void SmtEngine::push() doPendingPops(); Trace("smt") << "SMT push()" << endl; d_private->notifyPush(); - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); if(Dump.isOn("benchmark")) { Dump("benchmark") << PushCommand(); } @@ -2886,7 +2727,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 symmetric with pop. - setProblemExtended(); + d_smtMode = SMT_MODE_ASSERT; d_userLevels.push_back(d_userContext->getLevel()); internalPush(); @@ -2914,7 +2755,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(); + d_smtMode = SMT_MODE_ASSERT; AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); @@ -2924,6 +2765,7 @@ void SmtEngine::pop() { d_userLevels.pop_back(); // Clear out assertion queues etc., in case anything is still in there + d_asserts->clearCurrent(); d_private->notifyPop(); Trace("userpushpop") << "SmtEngine: popped to level " @@ -2937,7 +2779,7 @@ void SmtEngine::internalPush() { Trace("smt") << "SmtEngine::internalPush()" << endl; doPendingPops(); if(options::incrementalSolving()) { - d_private->processAssertions(); + d_private->processAssertions(*d_asserts); TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); d_userContext->push(); // the d_context push is done inside of the SAT solver |