diff options
| -rw-r--r-- | src/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/api/cvc4cpp.cpp | 19 | ||||
| -rw-r--r-- | src/smt/process_assertions.cpp | 1 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 458 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 185 | ||||
| -rw-r--r-- | src/smt/smt_engine_state.cpp | 298 | ||||
| -rw-r--r-- | src/smt/smt_engine_state.h | 254 | ||||
| -rw-r--r-- | src/smt/smt_mode.cpp | 37 | ||||
| -rw-r--r-- | src/smt/smt_mode.h | 57 | ||||
| -rw-r--r-- | test/unit/preprocessing/pass_bv_gauss_white.h | 2 | ||||
| -rw-r--r-- | test/unit/prop/cnf_stream_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/evaluator_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/sequences_rewriter_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_arith_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_bv_rewriter_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_bv_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_engine_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_quantifiers_bv_instantiator_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_sets_type_enumerator_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/theory_white.h | 2 | ||||
| -rw-r--r-- | test/unit/theory/type_enumerator_white.h | 2 |
21 files changed, 909 insertions, 428 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d8b778efa..d19719b6d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -261,8 +261,12 @@ libcvc4_add_sources( smt/smt_engine.h smt/smt_engine_scope.cpp smt/smt_engine_scope.h + smt/smt_engine_state.cpp + smt/smt_engine_state.h smt/smt_engine_stats.cpp smt/smt_engine_stats.h + smt/smt_mode.cpp + smt/smt_mode.h smt/smt_statistics_registry.cpp smt/smt_statistics_registry.h smt/term_formula_removal.cpp diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 7db0e41db..5ccb4c6c1 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -52,6 +52,7 @@ #include "options/smt_options.h" #include "smt/model.h" #include "smt/smt_engine.h" +#include "smt/smt_mode.h" #include "theory/logic_info.h" #include "theory/theory_model.h" #include "util/random.h" @@ -4819,8 +4820,7 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - == SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat assumptions unless in unsat mode."; std::vector<Node> uassumptions = d_smtEngine->getUnsatAssumptions(); @@ -4846,8 +4846,7 @@ std::vector<Term> Solver::getUnsatCore(void) const CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - == SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) << "Cannot get unsat core unless in unsat mode."; UnsatCore core = d_smtEngine->getUnsatCore(); /* Can not use @@ -4883,8 +4882,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const 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() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get value when in unsat mode."; std::vector<Term> res; for (size_t i = 0, n = terms.size(); i < n; ++i) @@ -4910,8 +4908,7 @@ Term Solver::getSeparationHeap() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get separtion heap term when in unsat mode."; theory::TheoryModel* m = @@ -4935,8 +4932,7 @@ Term Solver::getSeparationNilTerm() const CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; - CVC4_API_CHECK(d_smtEngine->getSmtMode() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get separtion nil term when in unsat mode."; theory::TheoryModel* m = @@ -5034,8 +5030,7 @@ void Solver::printModel(std::ostream& out) const 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() - != SmtEngine::SmtMode::SMT_MODE_UNSAT) + CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT) << "Cannot get value when in unsat mode."; out << *d_smtEngine->getModel(); CVC4_API_SOLVER_TRY_CATCH_END; diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index d2bf3ba46..492f3e105 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -462,7 +462,6 @@ bool ProcessAssertions::apply(Assertions& as) bool ProcessAssertions::simplifyAssertions(AssertionPipeline& assertions) { spendResource(ResourceManager::Resource::PreprocessStep); - Assert(d_smt.d_pendingPops == 0); try { ScopeCounter depth(d_simplifyAssertionsDepth); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c2d1a971e..13865b2ec 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -94,6 +94,7 @@ #include "smt/options_manager.h" #include "smt/preprocessor.h" #include "smt/smt_engine_scope.h" +#include "smt/smt_engine_state.h" #include "smt/smt_engine_stats.h" #include "smt/term_formula_removal.h" #include "smt/update_ostream.h" @@ -192,15 +193,13 @@ class SmtEnginePrivate }/* namespace CVC4::smt */ SmtEngine::SmtEngine(ExprManager* em, Options* optr) - : d_context(new Context()), - d_userContext(new UserContext()), - d_userLevels(), + : d_state(new SmtEngineState(*this)), 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_asserts(new Assertions(getUserContext(), *d_absValues.get())), + d_exprNames(new ExprNames(getUserContext())), + d_dumpm(new DumpManager(getUserContext())), d_routListener(new ResourceOutListener(*this)), d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())), d_theoryEngine(nullptr), @@ -214,13 +213,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_logic(), d_originalOptions(), d_isInternalSubsolver(false), - d_pendingPops(0), - d_fullyInited(false), - d_queryMade(false), - d_needPostsolve(false), - d_status(), - d_expectedStatus(), - d_smtMode(SMT_MODE_START), d_private(nullptr), d_statisticsRegistry(nullptr), d_stats(nullptr), @@ -253,7 +245,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) new ResourceManager(*d_statisticsRegistry.get(), d_options)); d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get())); d_pp.reset( - new smt::Preprocessor(*this, d_userContext.get(), *d_absValues.get())); + new smt::Preprocessor(*this, getUserContext(), *d_absValues.get())); d_private.reset(new smt::SmtEnginePrivate(*this)); // listen to node manager events d_nodeManager->subscribeEvents(d_snmListener.get()); @@ -277,12 +269,41 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_definedFunctions = new (true) DefinedFunctionMap(getUserContext()); } +bool SmtEngine::isFullyInited() const { return d_state->isFullyInited(); } +bool SmtEngine::isQueryMade() const { return d_state->isQueryMade(); } +size_t SmtEngine::getNumUserLevels() const +{ + return d_state->getNumUserLevels(); +} +SmtMode SmtEngine::getSmtMode() const { return d_state->getMode(); } +Result SmtEngine::getStatusOfLastCommand() const +{ + return d_state->getStatus(); +} +context::UserContext* SmtEngine::getUserContext() +{ + return d_state->getUserContext(); +} +context::Context* SmtEngine::getContext() { return d_state->getContext(); } + void SmtEngine::finishInit() { - // Notice that finishInit is called when options are finalized. If we are - // parsing smt2, this occurs at the moment we enter "Assert mode", page 52 + if (d_state->isFullyInited()) + { + // already initialized, return + return; + } + + // Notice that finishInitInternal is called when options are finalized. If we + // are parsing smt2, this occurs at the moment we enter "Assert mode", page 52 // of SMT-LIB 2.6 standard. + // set the logic + if (!d_logic.isLocked()) + { + setLogicInternal(); + } + // set the random seed Random::getRandom().setSeed(options::seed()); @@ -326,8 +347,7 @@ void SmtEngine::finishInit() // global push/pop around everything, to ensure proper destruction // of context-dependent data structures - d_userContext->push(); - d_context->push(); + d_state->setup(); Trace("smt-debug") << "Set up assertions..." << std::endl; d_asserts->finishInit(); @@ -363,35 +383,20 @@ void SmtEngine::finishInit() } }); d_pp->finishInit(); - Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; -} - -void SmtEngine::finalOptionsAreSet() { - if(d_fullyInited) { - return; - } - - if(! d_logic.isLocked()) { - setLogicInternal(); - } - - // finish initialization, create the prop engine, etc. - finishInit(); AlwaysAssert(d_propEngine->getAssertionLevel() == 0) << "The PropEngine has pushed but the SmtEngine " "hasn't finished initializing!"; - d_fullyInited = true; Assert(d_logic.isLocked()); + + // store that we are finished initializing + d_state->finishInit(); + Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl; } void SmtEngine::shutdown() { - doPendingPops(); - - while(options::incrementalSolving() && d_userContext->getLevel() > 1) { - internalPop(true); - } + d_state->shutdown(); if (d_propEngine != nullptr) { @@ -412,8 +417,7 @@ SmtEngine::~SmtEngine() // global push/pop around everything, to ensure proper destruction // of context-dependent data structures - d_context->popto(0); - d_userContext->popto(0); + d_state->cleanup(); if(d_assignments != NULL) { d_assignments->deleteSelf(); @@ -453,10 +457,8 @@ SmtEngine::~SmtEngine() // d_resourceManager must be destroyed before d_statisticsRegistry d_resourceManager.reset(nullptr); d_statisticsRegistry.reset(nullptr); - - - d_userContext.reset(nullptr); - d_context.reset(nullptr); + // destroy the state + d_state.reset(nullptr); } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl << e << endl; @@ -466,7 +468,8 @@ SmtEngine::~SmtEngine() void SmtEngine::setLogic(const LogicInfo& logic) { SmtScope smts(this); - if(d_fullyInited) { + if (d_state->isFullyInited()) + { throw ModalException("Cannot set logic in SmtEngine after the engine has " "finished initializing."); } @@ -510,18 +513,20 @@ LogicInfo SmtEngine::getUserLogicInfo() const void SmtEngine::notifyStartParsing(std::string filename) { - d_filename = filename; - + d_state->setFilename(filename); // Copy the original options. This is called prior to beginning parsing. // Hence reset should revert to these options, which note is after reading // the command line. d_originalOptions.copyValues(d_options); } -std::string SmtEngine::getFilename() const { return d_filename; } +const std::string& SmtEngine::getFilename() const +{ + return d_state->getFilename(); +} void SmtEngine::setLogicInternal() { - Assert(!d_fullyInited) + Assert(!d_state->isFullyInited()) << "setting logic in SmtEngine but the engine has already" " finished initializing for this run"; d_logic.lock(); @@ -555,7 +560,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } else if (key == "filename") { - d_filename = value.getValue(); + d_state->setFilename(value.getValue()); return; } else if (key == "smt-lib-version" && !options::inputLanguage.wasSetByUser()) @@ -599,7 +604,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) throw OptionException("argument to (set-info :status ..) must be " "`sat' or `unsat' or `unknown'"); } - d_expectedStatus = Result(s, d_filename); + d_state->notifyExpectedStatus(s); return; } throw UnrecognizedOptionException(); @@ -674,7 +679,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const if (key == "status") { // sat | unsat | unknown - switch (d_status.asSatisfiabilityResult().isSat()) + Result status = d_state->getStatus(); + switch (status.asSatisfiabilityResult().isSat()) { case Result::SAT: return SExpr(SExpr::Keyword("sat")); case Result::UNSAT: return SExpr(SExpr::Keyword("unsat")); @@ -683,10 +689,11 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const } if (key == "reason-unknown") { - if (!d_status.isNull() && d_status.isUnknown()) + Result status = d_state->getStatus(); + if (!status.isNull() && status.isUnknown()) { - stringstream ss; - ss << d_status.whyUnknown(); + std::stringstream ss; + ss << status.whyUnknown(); string s = ss.str(); transform(s.begin(), s.end(), s.begin(), ::tolower); return SExpr(SExpr::Keyword(s)); @@ -700,9 +707,9 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const } if (key == "assertion-stack-levels") { - AlwaysAssert(d_userLevels.size() - <= std::numeric_limits<unsigned long int>::max()); - return SExpr(static_cast<unsigned long int>(d_userLevels.size())); + size_t ulevel = d_state->getNumUserLevels(); + AlwaysAssert(ulevel <= std::numeric_limits<unsigned long int>::max()); + return SExpr(static_cast<unsigned long int>(ulevel)); } Assert(key == "all-options"); // get the options, like all-statistics @@ -766,8 +773,8 @@ void SmtEngine::defineFunction(Expr func, bool global) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SMT defineFunction(" << func << ")" << endl; debugCheckFormals(formals, func); @@ -820,8 +827,8 @@ void SmtEngine::defineFunctionsRec( bool global) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SMT defineFunctionsRec(...)" << endl; if (funcs.size() != formals.size() && funcs.size() != formulas.size()) @@ -919,18 +926,17 @@ bool SmtEngine::isDefinedFunction( Expr func ){ } Result SmtEngine::check() { - Assert(d_fullyInited); - Assert(d_pendingPops == 0); + Assert(d_state->isFullyReady()); Trace("smt") << "SmtEngine::check()" << endl; - + const std::string& filename = d_state->getFilename(); if (d_resourceManager->out()) { Result::UnknownExplanation why = d_resourceManager->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; - return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename); + return Result(Result::ENTAILMENT_UNKNOWN, why, filename); } d_resourceManager->beginCall(); @@ -950,14 +956,15 @@ Result SmtEngine::check() { << d_resourceManager->getTimeUsage() << ", resources " << d_resourceManager->getResourceUsage() << endl; - return Result(result, d_filename); + return Result(result, filename); } Result SmtEngine::quickCheck() { - Assert(d_fullyInited); + Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; + const std::string& filename = d_state->getFilename(); return Result( - Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename); + Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); } theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const @@ -969,7 +976,8 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - if (d_smtMode != SMT_MODE_SAT && d_smtMode != SMT_MODE_SAT_UNKNOWN) + if (d_state->getMode() != SmtMode::SAT + && d_state->getMode() != SmtMode::SAT_UNKNOWN) { std::stringstream ss; ss << "Cannot " << c @@ -999,12 +1007,25 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const return m; } +void SmtEngine::notifyPushPre() { processAssertionsInternal(); } +void SmtEngine::notifyPushPost() +{ + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); + d_propEngine->push(); +} +void SmtEngine::notifyPopPre() +{ + TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); + d_propEngine->pop(); +} +void SmtEngine::notifyPostSolvePre() { d_propEngine->resetTrail(); } +void SmtEngine::notifyPostSolvePost() { d_theoryEngine->postsolve(); } + void SmtEngine::processAssertionsInternal() { TimerStat::CodeTimer paTimer(d_stats->d_processAssertionsTime); d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep); - Assert(d_fullyInited); - Assert(d_pendingPops == 0); + Assert(d_state->isFullyReady()); AssertionPipeline& ap = d_asserts->getAssertionPipeline(); @@ -1109,30 +1130,14 @@ Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions, try { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "checkEntailed" : "checkSat") << "(" << assumptions << ")" << endl; - - if(d_queryMade && !options::incrementalSolving()) { - throw ModalException("Cannot make multiple queries unless " - "incremental solving is enabled " - "(try --incremental)"); - } - - // Note that a query has been made and we are in assert mode - d_queryMade = true; - d_smtMode = SMT_MODE_ASSERT; - - // push if there are assumptions - bool didInternalPush = false; - if (!assumptions.empty()) - { - internalPush(); - didInternalPush = true; - } + // update the state to indicate we are about to run a check-sat + bool hasAssumptions = !assumptions.empty(); + d_state->notifyCheckSat(hasAssumptions); // then, initialize the assertions d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck); @@ -1168,37 +1173,8 @@ Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions, Trace("smt") << "SmtEngine::global negate returned " << r << std::endl; } - d_needPostsolve = true; - - // Pop the context - if (didInternalPush) - { - internalPop(); - } - - // Remember the status - d_status = r; - // Check against expected status - if (!d_expectedStatus.isUnknown() && !d_status.isUnknown() - && d_status != d_expectedStatus) - { - CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got " - << d_status; - } - d_expectedStatus = Result(); - // Update the SMT mode - if (d_status.asSatisfiabilityResult().isSat() == Result::UNSAT) - { - d_smtMode = SMT_MODE_UNSAT; - } - else if (d_status.asSatisfiabilityResult().isSat() == Result::SAT) - { - d_smtMode = SMT_MODE_SAT; - } - else - { - d_smtMode = SMT_MODE_SAT_UNKNOWN; - } + // notify our state of the check-sat result + d_state->notifyCheckSatResult(hasAssumptions, r); Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat") << "(" << assumptions << ") => " << r << endl; @@ -1227,10 +1203,14 @@ Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions, return r; } catch (UnsafeInterruptException& e) { AlwaysAssert(d_resourceManager->out()); + // Notice that we do not notify the state of this result. If we wanted to + // make the solver resume a working state after an interupt, then we would + // implement a different callback and use it here, e.g. + // d_state.notifyCheckSatInterupt. Result::UnknownExplanation why = d_resourceManager->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; - return Result(Result::SAT_UNKNOWN, why, d_filename); + return Result(Result::SAT_UNKNOWN, why, d_state->getFilename()); } } @@ -1244,13 +1224,13 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void) "Cannot get unsat assumptions when produce-unsat-assumptions option " "is off."); } - if (d_smtMode != SMT_MODE_UNSAT) + if (d_state->getMode() != SmtMode::UNSAT) { throw RecoverableModalException( "Cannot get unsat assumptions unless immediately preceded by " "UNSAT/ENTAILED."); } - finalOptionsAreSet(); + finishInit(); if (Dump.isOn("benchmark")) { Dump("benchmark") << GetUnsatAssumptionsCommand(); @@ -1271,8 +1251,8 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void) Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl; @@ -1296,7 +1276,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n"; Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); @@ -1308,7 +1288,7 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id, Type type) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); d_private->d_sygusVars.push_back(Node::fromExpr(var)); Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n"; Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type); @@ -1323,8 +1303,8 @@ void SmtEngine::declareSynthFun(const std::string& id, const std::vector<Expr>& vars) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Node fn = Node::fromExpr(func); d_private->d_sygusFunSymbols.push_back(fn); if (!vars.empty()) @@ -1354,7 +1334,7 @@ void SmtEngine::declareSynthFun(const std::string& id, void SmtEngine::assertSygusConstraint(const Node& constraint) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); d_private->d_sygusConstraints.push_back(constraint); Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n"; @@ -1369,7 +1349,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv, const Expr& post) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); // build invariant constraint // get variables (regular and their respective primed versions) @@ -1489,17 +1469,8 @@ Result SmtEngine::checkSynth() d_private->d_sygusConjectureStale = false; - if (options::incrementalSolving()) - { - // we push a context so that this conjecture is removed if we modify it - // later - internalPush(); - assertFormula(body, true); - } - else - { - query = body.toExpr(); - } + // TODO (project #7): if incremental, we should push a context and assert + query = body.toExpr(); } Result r = checkSatisfiability(query, true, false); @@ -1522,8 +1493,8 @@ Result SmtEngine::checkSynth() Node SmtEngine::simplify(const Node& ex) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); // ensure we've processed assertions processAssertionsInternal(); return d_pp->simplify(ex); @@ -1534,8 +1505,8 @@ Node SmtEngine::expandDefinitions(const Node& ex) d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep); SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); // set expandOnly flag to true return d_pp->expandDefinitions(ex, true); } @@ -1608,8 +1579,8 @@ vector<Expr> SmtEngine::getValues(const vector<Expr>& exprs) bool SmtEngine::addToAssignment(const Expr& ex) { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); // Substitute out any abstract values in ex Node n = d_absValues->substituteAbstractValues(Node::fromExpr(ex)); TypeNode type = n.getType(options::typeChecking()); @@ -1643,7 +1614,7 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment() { Trace("smt") << "SMT getAssignment()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssignmentCommand(); } @@ -1703,7 +1674,7 @@ Model* SmtEngine::getModel() { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetModelCommand(); @@ -1723,8 +1694,8 @@ Model* SmtEngine::getModel() { std::vector<Expr> eassertsProc = getExpandedAssertions(); ModelCoreBuilder::setModelCore(eassertsProc, m, options::modelCoresMode()); } - m->d_inputName = d_filename; - m->d_isKnownSat = (d_smtMode == SMT_MODE_SAT); + m->d_inputName = d_state->getFilename(); + m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT); return m; } @@ -1733,7 +1704,7 @@ Result SmtEngine::blockModel() Trace("smt") << "SMT blockModel()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if (Dump.isOn("benchmark")) { @@ -1761,7 +1732,7 @@ Result SmtEngine::blockModelValues(const std::vector<Expr>& exprs) Trace("smt") << "SMT blockModelValues()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); PrettyCheckArgument( !exprs.empty(), @@ -1867,7 +1838,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal() throw ModalException( "Cannot get an unsat core when produce-unsat-cores option is off."); } - if (d_smtMode != SMT_MODE_UNSAT) + if (d_state->getMode() != SmtMode::UNSAT) { throw RecoverableModalException( "Cannot get an unsat core unless immediately preceded by " @@ -2311,7 +2282,7 @@ void SmtEngine::checkAbduct(Node a) UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetUnsatCoreCommand(); } @@ -2323,7 +2294,7 @@ const Proof& SmtEngine::getProof() { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetProofCommand(); } @@ -2331,7 +2302,7 @@ const Proof& SmtEngine::getProof() if(!options::proof()) { throw ModalException("Cannot get a proof when produce-proofs option is off."); } - if (d_smtMode != SMT_MODE_UNSAT) + if (d_state->getMode() != SmtMode::UNSAT) { throw RecoverableModalException( "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED " @@ -2346,10 +2317,11 @@ const Proof& SmtEngine::getProof() void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if (options::instFormatMode() == options::InstFormatMode::SZS) { - out << "% SZS output start Proof for " << d_filename.c_str() << std::endl; + out << "% SZS output start Proof for " << d_state->getFilename() + << std::endl; } if( d_theoryEngine ){ d_theoryEngine->printInstantiations( out ); @@ -2358,13 +2330,13 @@ void SmtEngine::printInstantiations( std::ostream& out ) { } if (options::instFormatMode() == options::InstFormatMode::SZS) { - out << "% SZS output end Proof for " << d_filename.c_str() << std::endl; + out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; } } void SmtEngine::printSynthSolution( std::ostream& out ) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if( d_theoryEngine ){ d_theoryEngine->printSynthSolution( out ); }else{ @@ -2375,7 +2347,7 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); std::map<Node, std::map<Node, Node>> sol_mapn; Assert(d_theoryEngine != nullptr); // fail if the theory engine does not have synthesis solutions @@ -2396,7 +2368,7 @@ bool SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map) Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } @@ -2478,15 +2450,11 @@ bool SmtEngine::getAbduct(const Node& conj, const TypeNode& grammarType, Node& abd) { - if (d_abductSolver->getAbduct(conj, grammarType, 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 success = d_abductSolver->getAbduct(conj, grammarType, abd); + // notify the state of whether the get-abduct call was successfuly, which + // impacts the SMT mode. + d_state->notifyGetAbduct(success); + return success; } bool SmtEngine::getAbduct(const Node& conj, Node& abd) @@ -2539,10 +2507,11 @@ void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< E } } -vector<Expr> SmtEngine::getAssertions() { +std::vector<Expr> SmtEngine::getAssertions() +{ SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssertionsCommand(); } @@ -2566,57 +2535,24 @@ vector<Expr> SmtEngine::getAssertions() { void SmtEngine::push() { SmtScope smts(this); - finalOptionsAreSet(); - doPendingPops(); + finishInit(); + d_state->doPendingPops(); Trace("smt") << "SMT push()" << endl; processAssertionsInternal(); if(Dump.isOn("benchmark")) { Dump("benchmark") << PushCommand(); } - if(!options::incrementalSolving()) { - throw ModalException("Cannot push when not solving incrementally (use --incremental)"); - } - - - // The problem isn't really "extended" yet, but this disallows - // get-model after a push, simplifying our lives somewhat and - // staying symmetric with pop. - d_smtMode = SMT_MODE_ASSERT; - - d_userLevels.push_back(d_userContext->getLevel()); - internalPush(); - Trace("userpushpop") << "SmtEngine: pushed to level " - << d_userContext->getLevel() << endl; + d_state->userPush(); } void SmtEngine::pop() { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); Trace("smt") << "SMT pop()" << endl; if(Dump.isOn("benchmark")) { Dump("benchmark") << PopCommand(); } - if(!options::incrementalSolving()) { - throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); - } - if(d_userLevels.size() == 0) { - throw ModalException("Cannot pop beyond the first user frame"); - } - - // The problem isn't really "extended" yet, but this disallows - // get-model after a pop, simplifying our lives somewhat. It might - // not be strictly necessary to do so, since the pops occur lazily, - // 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_smtMode = SMT_MODE_ASSERT; - - AlwaysAssert(d_userContext->getLevel() > 0); - AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); - while (d_userLevels.back() < d_userContext->getLevel()) { - internalPop(true); - } - d_userLevels.pop_back(); + d_state->userPop(); // Clear out assertion queues etc., in case anything is still in there d_asserts->clearCurrent(); @@ -2624,57 +2560,11 @@ void SmtEngine::pop() { d_pp->clearLearnedLiterals(); Trace("userpushpop") << "SmtEngine: popped to level " - << d_userContext->getLevel() << endl; - // FIXME: should we reset d_status here? + << getUserContext()->getLevel() << endl; + // should we reset d_status here? // SMT-LIBv2 spec seems to imply no, but it would make sense to.. } -void SmtEngine::internalPush() { - Assert(d_fullyInited); - Trace("smt") << "SmtEngine::internalPush()" << endl; - doPendingPops(); - if(options::incrementalSolving()) { - processAssertionsInternal(); - TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - d_userContext->push(); - // the d_context push is done inside of the SAT solver - d_propEngine->push(); - } -} - -void SmtEngine::internalPop(bool immediate) { - Assert(d_fullyInited); - Trace("smt") << "SmtEngine::internalPop()" << endl; - if(options::incrementalSolving()) { - ++d_pendingPops; - } - if(immediate) { - doPendingPops(); - } -} - -void SmtEngine::doPendingPops() { - Trace("smt") << "SmtEngine::doPendingPops()" << endl; - Assert(d_pendingPops == 0 || options::incrementalSolving()); - // check to see if a postsolve() is pending - if (d_needPostsolve) - { - d_propEngine->resetTrail(); - } - while(d_pendingPops > 0) { - TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime); - d_propEngine->pop(); - // the d_context pop is done inside of the SAT solver - d_userContext->pop(); - --d_pendingPops; - } - if (d_needPostsolve) - { - d_theoryEngine->postsolve(); - d_needPostsolve = false; - } -} - void SmtEngine::reset() { SmtScope smts(this); @@ -2693,17 +2583,16 @@ void SmtEngine::resetAssertions() { SmtScope smts(this); - if (!d_fullyInited) + if (!d_state->isFullyInited()) { // We're still in Start Mode, nothing asserted yet, do nothing. // (see solver execution modes in the SMT-LIB standard) - Assert(d_context->getLevel() == 0); - Assert(d_userContext->getLevel() == 0); + Assert(getContext()->getLevel() == 0); + Assert(getUserContext()->getLevel() == 0); d_dumpm->resetAssertions(); return; } - doPendingPops(); Trace("smt") << "SMT resetAssertions()" << endl; if (Dump.isOn("benchmark")) @@ -2711,19 +2600,10 @@ void SmtEngine::resetAssertions() Dump("benchmark") << ResetAssertionsCommand(); } - while (!d_userLevels.empty()) - { - pop(); - } - - // Remember the global push/pop around everything when beyond Start mode - // (see solver execution modes in the SMT-LIB standard) - Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1); - d_context->popto(0); - d_userContext->popto(0); + d_state->notifyResetAssertions(); d_dumpm->resetAssertions(); - d_userContext->push(); - d_context->push(); + // push the state to maintain global context around everything + d_state->setup(); /* Create new PropEngine. * First force destruction of referenced PropEngine to enforce that @@ -2737,7 +2617,8 @@ void SmtEngine::resetAssertions() void SmtEngine::interrupt() { - if(!d_fullyInited) { + if (!d_state->isFullyInited()) + { return; } d_propEngine->interrupt(); @@ -2790,9 +2671,10 @@ void SmtEngine::setUserAttribute(const std::string& attr, const std::string& str_value) { SmtScope smts(this); - finalOptionsAreSet(); + finishInit(); std::vector<Node> node_values; - for( unsigned i=0; i<expr_values.size(); i++ ){ + for (std::size_t i = 0, n = expr_values.size(); i < n; i++) + { node_values.push_back( expr_values[i].getNode() ); } d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value); @@ -2803,7 +2685,8 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) // Always check whether the SmtEngine has been initialized (which is done // upon entering Assert mode the first time). No option can be set after // initialized. - if(d_fullyInited) { + if (d_state->isFullyInited()) + { throw ModalException("SmtEngine::setOption called after initialization."); } NodeManagerScope nms(d_nodeManager); @@ -2926,10 +2809,7 @@ void SmtEngine::setSygusConjectureStale() return; } d_private->d_sygusConjectureStale = true; - if (options::incrementalSolving()) - { - internalPop(); - } + // TODO (project #7): if incremental, we should pop a context } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3ae04a720..4df57accb 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -31,6 +31,7 @@ #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" +#include "smt/smt_mode.h" #include "theory/logic_info.h" #include "util/hash.h" #include "util/proof.h" @@ -92,6 +93,7 @@ namespace prop { namespace smt { /** Utilities */ +class SmtEngineState; class AbstractValues; class Assertions; class ExprNames; @@ -144,6 +146,7 @@ class CVC4_PUBLIC SmtEngine // TODO (Issue #1096): Remove this friend relationship. friend class ::CVC4::preprocessing::PreprocessingPassContext; friend class ::CVC4::smt::SmtEnginePrivate; + friend class ::CVC4::smt::SmtEngineState; friend class ::CVC4::smt::SmtScope; friend class ::CVC4::smt::ProcessAssertions; friend ProofManager* ::CVC4::smt::currentProofManager(); @@ -156,29 +159,6 @@ class CVC4_PUBLIC SmtEngine /* ....................................................................... */ /** - * The current mode of the solver, which is an extension of 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" - SMT_MODE_SAT, - // immediately after a check-sat returning "unknown" - SMT_MODE_SAT_UNKNOWN, - // immediately after a check-sat returning "unsat" - SMT_MODE_UNSAT, - // immediately after a successful call to get-abduct - SMT_MODE_ABDUCT, - // immediately after a successful call to get-interpol - SMT_MODE_INTERPOL - }; - - /** * Construct an SmtEngine with the given expression manager. * If provided, optr is a pointer to a set of options that should initialize the values * of the options object owned by this class. @@ -187,24 +167,43 @@ class CVC4_PUBLIC SmtEngine /** Destruct the SMT engine. */ ~SmtEngine(); + //--------------------------------------------- concerning the state + /** - * Return true if this SmtEngine is fully initialized (post-construction). + * This is the main initialization procedure of the SmtEngine. + * + * Should be called whenever the final options and logic for the problem are + * set (at least, those options that are not permitted to change after + * assertions and queries are made). + * + * Internally, this creates the theory engine, prop engine, decision engine, + * and other utilities whose initialization depends on the final set of + * options being set. + * * This post-construction initialization is automatically triggered by the * use of the SmtEngine; e.g. when the first formula is asserted, a call * to simplify() is issued, a scope is pushed, etc. */ - bool isFullyInited() { return d_fullyInited; } - + void finishInit(); + /** + * Return true if this SmtEngine is fully initialized (post-construction) + * by the above call. + */ + bool isFullyInited() const; /** * Return true if a checkEntailed() or checkSatisfiability() has been made. */ - bool isQueryMade() { return d_queryMade; } - + bool isQueryMade() const; /** Return the user context level. */ - size_t getNumUserLevels() { return d_userLevels.size(); } - + size_t getNumUserLevels() const; /** Return the current mode of the solver. */ - SmtMode getSmtMode() { return d_smtMode; } + SmtMode getSmtMode() const; + /** + * Returns the most recent result of checkSat/checkEntailed or + * (set-info :status). + */ + Result getStatusOfLastCommand() const; + //--------------------------------------------- end concerning the state /** * Set the logic of the script. @@ -269,7 +268,7 @@ class CVC4_PUBLIC SmtEngine */ void notifyStartParsing(std::string filename); /** return the input name (if any) */ - std::string getFilename() const; + const std::string& getFilename() const; /** * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED @@ -842,12 +841,6 @@ class CVC4_PUBLIC SmtEngine void safeFlushStatistics(int fd) const; /** - * Returns the most recent result of checkSat/checkEntailed or - * (set-info :status). - */ - Result getStatusOfLastCommand() const { return d_status; } - - /** * Set user attribute. * This function is called when an attribute is set by a user. * In SMT-LIBv2 this is done via the syntax (! expr :attr) @@ -908,18 +901,18 @@ class CVC4_PUBLIC SmtEngine /** Set solver instance that owns this SmtEngine. */ void setSolver(api::Solver* solver) { d_solver = solver; } + /** Get a pointer to the UserContext owned by this SmtEngine. */ + context::UserContext* getUserContext(); + + /** Get a pointer to the Context owned by this SmtEngine. */ + context::Context* getContext(); + /** Get a pointer to the TheoryEngine owned by this SmtEngine. */ TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); } /** Get a pointer to the PropEngine owned by this SmtEngine. */ prop::PropEngine* getPropEngine() { return d_propEngine.get(); } - /** Get a pointer to the UserContext owned by this SmtEngine. */ - context::UserContext* getUserContext() { return d_userContext.get(); }; - - /** Get a pointer to the Context owned by this SmtEngine. */ - context::Context* getContext() { return d_context.get(); }; - /** Get a pointer to the ProofManager owned by this SmtEngine. */ ProofManager* getProofManager() { return d_proofManager.get(); }; @@ -988,20 +981,6 @@ class CVC4_PUBLIC SmtEngine void checkAbduct(Node a); /** - * This is something of an "init" procedure, but is idempotent; call - * as often as you like. Should be called whenever the final options - * and logic for the problem are set (at least, those options that are - * not permitted to change after assertions and queries are made). - */ - void finalOptionsAreSet(); - - /** - * Create theory engine, prop engine, decision engine. Called by - * finalOptionsAreSet() - */ - void finishInit(); - - /** * This is called by the destructor, just before destroying the * PropEngine, TheoryEngine, and DecisionEngine (in that order). It * is important because there are destruction ordering issues @@ -1034,11 +1013,35 @@ class CVC4_PUBLIC SmtEngine */ theory::TheoryModel* getAvailableModel(const char* c) const; - void internalPush(); - - void internalPop(bool immediate = false); - - void doPendingPops(); + // --------------------------------------- callbacks from the state + /** + * Notify push pre, which is called just before the user context of the state + * pushes. This processes all pending assertions. + */ + void notifyPushPre(); + /** + * Notify push post, which is called just after the user context of the state + * pushes. This performs a push on the underlying prop engine. + */ + void notifyPushPost(); + /** + * Notify pop pre, which is called just before the user context of the state + * pops. This performs a pop on the underlying prop engine. + */ + void notifyPopPre(); + /** + * Notify post solve pre, which is called once per check-sat query. It + * is triggered when the first d_state.doPendingPops() is issued after the + * check-sat. This method is called before the contexts pop in the method + * doPendingPops. + */ + void notifyPostSolvePre(); + /** + * Same as above, but after contexts are popped. This calls the postsolve + * method of the underlying TheoryEngine. + */ + void notifyPostSolvePost(); + // --------------------------------------- end callbacks from the state /** * Internally handle the setting of a logic. This function should always @@ -1099,12 +1102,11 @@ class CVC4_PUBLIC SmtEngine /** Solver instance that owns this SmtEngine instance. */ api::Solver* d_solver = nullptr; - /** Expr manager context */ - std::unique_ptr<context::Context> d_context; - /** User level context */ - std::unique_ptr<context::UserContext> d_userContext; - /** The context levels of user pushes */ - std::vector<int> d_userLevels; + /** + * The state of this SmtEngine, which is responsible for maintaining which + * SMT mode we are in, the contexts, the last result, etc. + */ + std::unique_ptr<smt::SmtEngineState> d_state; /** Our expression manager */ ExprManager* d_exprManager; @@ -1173,51 +1175,6 @@ class CVC4_PUBLIC SmtEngine bool d_isInternalSubsolver; /** - * Number of internal pops that have been deferred. - */ - unsigned d_pendingPops; - - /** - * Whether or not this SmtEngine is fully initialized (post-construction). - * This post-construction initialization is automatically triggered by the - * use of the SmtEngine; e.g. when the first formula is asserted, a call - * to simplify() is issued, a scope is pushed, etc. - */ - bool d_fullyInited; - - /** - * Whether or not a checkEntailed() or checkSatisfiability() has already been - * made through this SmtEngine. If true, and incrementalSolving is false, - * then attempting an additional checkEntailed() or checkSat() will fail with - * a ModalException. - */ - bool d_queryMade; - - /** - * Internal status flag to indicate whether we've sent a theory - * presolve() notification and need to match it with a postsolve(). - */ - bool d_needPostsolve; - - /** - * Most recent result of last checkSatisfiability/checkEntailed or - * (set-info :status). - */ - Result d_status; - - /** - * The expected status of the next satisfiability check. - */ - Result d_expectedStatus; - - SmtMode d_smtMode; - - /** - * The input file name (if any) or the name set through setInfo (if any) - */ - std::string d_filename; - - /** * Verbosity of various commands. */ std::map<std::string, Integer> d_commandVerbosity; diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp new file mode 100644 index 000000000..07f1d3321 --- /dev/null +++ b/src/smt/smt_engine_state.cpp @@ -0,0 +1,298 @@ +/********************* */ +/*! \file smt_engine_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for maintaining the state of the SMT engine. + **/ + +#include "smt/smt_engine_state.h" + +#include "options/smt_options.h" +#include "smt/smt_engine.h" + +namespace CVC4 { +namespace smt { + +SmtEngineState::SmtEngineState(SmtEngine& smt) + : d_smt(smt), + d_context(new context::Context()), + d_userContext(new context::UserContext()), + d_pendingPops(0), + d_fullyInited(false), + d_queryMade(false), + d_needPostsolve(false), + d_status(), + d_expectedStatus(), + d_smtMode(SmtMode::START) +{ +} + +void SmtEngineState::notifyExpectedStatus(const std::string& status) +{ + Assert(status == "sat" || status == "unsat" || status == "unknown") + << "SmtEngineState::notifyExpectedStatus: unexpected status string " + << status; + d_expectedStatus = Result(status, d_filename); +} + +void SmtEngineState::notifyResetAssertions() +{ + doPendingPops(); + while (!d_userLevels.empty()) + { + userPop(); + } + // Remember the global push/pop around everything when beyond Start mode + // (see solver execution modes in the SMT-LIB standard) + Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1); + popto(0); +} + +void SmtEngineState::notifyCheckSat(bool hasAssumptions) +{ + // process the pending pops + doPendingPops(); + if (d_queryMade && !options::incrementalSolving()) + { + throw ModalException( + "Cannot make multiple queries unless " + "incremental solving is enabled " + "(try --incremental)"); + } + + // Note that a query has been made and we are in assert mode + d_queryMade = true; + d_smtMode = SmtMode::ASSERT; + + // push if there are assumptions + if (hasAssumptions) + { + internalPush(); + } +} + +void SmtEngineState::notifyCheckSatResult(bool hasAssumptions, Result r) +{ + d_needPostsolve = true; + + // Pop the context + if (hasAssumptions) + { + internalPop(); + } + + // Remember the status + d_status = r; + // Check against expected status + if (!d_expectedStatus.isUnknown() && !d_status.isUnknown() + && d_status != d_expectedStatus) + { + CVC4_FATAL() << "Expected result " << d_expectedStatus << " but got " + << d_status; + } + // clear expected status + d_expectedStatus = Result(); + // Update the SMT mode + switch (d_status.asSatisfiabilityResult().isSat()) + { + case Result::UNSAT: d_smtMode = SmtMode::UNSAT; break; + case Result::SAT: d_smtMode = SmtMode::SAT; break; + default: d_smtMode = SmtMode::SAT_UNKNOWN; + } +} + +void SmtEngineState::notifyGetAbduct(bool success) +{ + if (success) + { + // successfully generated an abduct, update to abduct state + d_smtMode = SmtMode::ABDUCT; + } + else + { + // failed, we revert to the assert state + d_smtMode = SmtMode::ASSERT; + } +} + +void SmtEngineState::setup() +{ + // push a context + push(); +} + +void SmtEngineState::finishInit() +{ + // set the flag to remember that we are fully initialized + d_fullyInited = true; +} + +void SmtEngineState::shutdown() +{ + doPendingPops(); + + while (options::incrementalSolving() && d_userContext->getLevel() > 1) + { + internalPop(true); + } +} + +void SmtEngineState::cleanup() +{ + // pop to level zero + popto(0); +} + +void SmtEngineState::setFilename(const std::string& filename) +{ + d_filename = filename; +} + +void SmtEngineState::userPush() +{ + if (!options::incrementalSolving()) + { + throw ModalException( + "Cannot push when not solving incrementally (use --incremental)"); + } + // The problem isn't really "extended" yet, but this disallows + // get-model after a push, simplifying our lives somewhat and + // staying symmetric with pop. + d_smtMode = SmtMode::ASSERT; + + d_userLevels.push_back(d_userContext->getLevel()); + internalPush(); + Trace("userpushpop") << "SmtEngineState: pushed to level " + << d_userContext->getLevel() << std::endl; +} + +void SmtEngineState::userPop() +{ + if (!options::incrementalSolving()) + { + throw ModalException( + "Cannot pop when not solving incrementally (use --incremental)"); + } + if (d_userLevels.size() == 0) + { + throw ModalException("Cannot pop beyond the first user frame"); + } + // The problem isn't really "extended" yet, but this disallows + // get-model after a pop, simplifying our lives somewhat. It might + // not be strictly necessary to do so, since the pops occur lazily, + // 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_smtMode = SmtMode::ASSERT; + + AlwaysAssert(d_userContext->getLevel() > 0); + AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); + while (d_userLevels.back() < d_userContext->getLevel()) + { + internalPop(true); + } + d_userLevels.pop_back(); +} + +void SmtEngineState::push() +{ + d_userContext->push(); + d_context->push(); +} + +void SmtEngineState::pop() +{ + d_userContext->pop(); + d_context->pop(); +} + +void SmtEngineState::popto(int toLevel) +{ + d_context->popto(toLevel); + d_userContext->popto(toLevel); +} + +context::UserContext* SmtEngineState::getUserContext() +{ + return d_userContext.get(); +} + +context::Context* SmtEngineState::getContext() { return d_context.get(); } + +Result SmtEngineState::getStatus() const { return d_status; } + +bool SmtEngineState::isFullyInited() const { return d_fullyInited; } +bool SmtEngineState::isFullyReady() const +{ + return d_fullyInited && d_pendingPops == 0; +} +bool SmtEngineState::isQueryMade() const { return d_queryMade; } +size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); } + +SmtMode SmtEngineState::getMode() const { return d_smtMode; } + +const std::string& SmtEngineState::getFilename() const { return d_filename; } + +void SmtEngineState::internalPush() +{ + Assert(d_fullyInited); + Trace("smt") << "SmtEngineState::internalPush()" << std::endl; + doPendingPops(); + if (options::incrementalSolving()) + { + // notifies the SmtEngine to process the assertions immediately + d_smt.notifyPushPre(); + d_userContext->push(); + // the context push is done inside of the SAT solver + d_smt.notifyPushPost(); + } +} + +void SmtEngineState::internalPop(bool immediate) +{ + Assert(d_fullyInited); + Trace("smt") << "SmtEngineState::internalPop()" << std::endl; + if (options::incrementalSolving()) + { + ++d_pendingPops; + } + if (immediate) + { + doPendingPops(); + } +} + +void SmtEngineState::doPendingPops() +{ + Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl; + Assert(d_pendingPops == 0 || options::incrementalSolving()); + // check to see if a postsolve() is pending + if (d_needPostsolve) + { + d_smt.notifyPostSolvePre(); + } + while (d_pendingPops > 0) + { + // the context pop is done inside of the SAT solver + d_smt.notifyPopPre(); + // pop the context + d_userContext->pop(); + --d_pendingPops; + // no need for pop post (for now) + } + if (d_needPostsolve) + { + d_smt.notifyPostSolvePost(); + d_needPostsolve = false; + } +} + +} // namespace smt +} // namespace CVC4 diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h new file mode 100644 index 000000000..efb86ca88 --- /dev/null +++ b/src/smt/smt_engine_state.h @@ -0,0 +1,254 @@ +/********************* */ +/*! \file smt_engine_state.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for maintaining the state of the SMT engine. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__SMT_ENGINE_STATE_H +#define CVC4__SMT__SMT_ENGINE_STATE_H + +#include <string> + +#include "context/context.h" +#include "smt/smt_mode.h" +#include "util/result.h" + +namespace CVC4 { + +class SmtEngine; + +namespace smt { + +/** + * This utility is responsible for maintaining the basic state of the SmtEngine. + * + * It has no concept of anything related to the assertions of the SmtEngine, + * or more generally it does not depend on Node. + * + * This class has three sets of interfaces: + * (1) notification methods that are used by SmtEngine to notify when an event + * occurs (e.g. the beginning of a check-sat call), + * (2) maintaining the SAT and user contexts to be used by the SmtEngine, + * (3) general information queries, including the mode that the SmtEngine is + * in, based on the notifications it has received. + * + * It maintains a reference to the SmtEngine for the sake of making callbacks. + */ +class SmtEngineState +{ + public: + SmtEngineState(SmtEngine& smt); + ~SmtEngineState() {} + /** + * Notify that the expected status of the next check-sat is given by the + * string status, which should be one of "sat", "unsat" or "unknown". + */ + void notifyExpectedStatus(const std::string& status); + /** + * Notify that the SmtEngine is fully initialized, which is called when + * options are finalized. + */ + void notifyFullyInited(); + /** + * Notify that we are resetting the assertions, called when a reset-assertions + * command is issued by the user. + */ + void notifyResetAssertions(); + /** + * Notify that we are about to call check-sat. This call is made prior to + * initializing the assertions. It processes pending pops and pushes a + * (user) context if necessary. + * + * @param hasAssumptions Whether the call to check-sat has assumptions. If + * so, we push a context. + */ + void notifyCheckSat(bool hasAssumptions); + /** + * Notify that the result of the last check-sat was r. This should be called + * once immediately following notifyCheckSat() if the check-sat call + * returned normal (i.e. it was not interupted). + * + * @param hasAssumptions Whether the prior call to check-sat had assumptions. + * If so, we pop a context. + * @param r The result of the check-sat call. + */ + void notifyCheckSatResult(bool hasAssumptions, Result r); + /** + * Notify that we finished an abduction query, where success is whether the + * command was successful. This is managed independently of the above + * calls for notifying check-sat. In other words, if a get-abduct command + * is issued to an SmtEngine, it may use a satisfiability call (if desired) + * to solve the abduction query. This method is called *in addition* to + * the above calls to notifyCheckSat / notifyCheckSatResult in this case. + * In particular, it is called after these two methods are completed. + * This overwrites the SMT mode to the "ABDUCT" mode if the call to abduction + * was successful. + */ + void notifyGetAbduct(bool success); + /** + * Setup the context, which makes a single push to maintain a global + * context around everything. + */ + void setup(); + /** + * Set that we are in a fully initialized state. + */ + void finishInit(); + /** + * Prepare for a shutdown of the SmtEngine, which does pending pops and + * pops the user context to zero. + */ + void shutdown(); + /** + * Cleanup, which pops all contexts to level zero. + */ + void cleanup(); + /** + * Set that the file name of the current instance is the given string. This + * is used for various purposes (e.g. get-info, SZS status). + */ + void setFilename(const std::string& filename); + + //---------------------------- context management + /** + * Do all pending pops, which ensures that the context levels are up-to-date. + * This method should be called by the SmtEngine before using any of its + * members that rely on the context (e.g. PropEngine or TheoryEngine). + */ + void doPendingPops(); + /** + * Called when the user of SmtEngine issues a push. This corresponds to + * the SMT-LIB command push. + */ + void userPush(); + /** + * Called when the user of SmtEngine issues a pop. This corresponds to + * the SMT-LIB command pop. + */ + void userPop(); + /** Get a pointer to the UserContext owned by this SmtEngine. */ + context::UserContext* getUserContext(); + /** Get a pointer to the Context owned by this SmtEngine. */ + context::Context* getContext(); + //---------------------------- end context management + + //---------------------------- queries + /** + * Return true if the SmtEngine is fully initialized (post-construction). + * This post-construction initialization is automatically triggered by the + * use of the SmtEngine; e.g. when the first formula is asserted, a call + * to simplify() is issued, a scope is pushed, etc. + */ + bool isFullyInited() const; + /** + * Return true if the SmtEngine is fully initialized and there are no + * pending pops. + */ + bool isFullyReady() const; + /** + * Return true if a notifyCheckSat call has been made, e.g. a query has been + * issued to the SmtEngine. + */ + bool isQueryMade() const; + /** Return the user context level. */ + size_t getNumUserLevels() const; + /** Get the status of the last check-sat */ + Result getStatus() const; + /** Get the SMT mode we are in */ + SmtMode getMode() const; + /** return the input name (if any) */ + const std::string& getFilename() const; + //---------------------------- end queries + + private: + /** Pushes the user and SAT contexts */ + void push(); + /** Pops the user and SAT contexts */ + void pop(); + /** Pops the user and SAT contexts to the given level */ + void popto(int toLevel); + /** + * Internal push, which processes any pending pops, and pushes (if in + * incremental mode). + */ + void internalPush(); + /** + * Internal pop. If immediate is true, this processes any pending pops, and + * pops (if in incremental mode). Otherwise, it increments the pending pop + * counter and does nothing. + */ + void internalPop(bool immediate = false); + /** Reference to the SmtEngine */ + SmtEngine& d_smt; + /** Expr manager context */ + std::unique_ptr<context::Context> d_context; + /** User level context */ + std::unique_ptr<context::UserContext> d_userContext; + /** The context levels of user pushes */ + std::vector<int> d_userLevels; + + /** + * Number of internal pops that have been deferred. + */ + unsigned d_pendingPops; + + /** + * Whether or not the SmtEngine is fully initialized (post-construction). + * This post-construction initialization is automatically triggered by the + * use of the SmtEngine which calls the finishInit method above; e.g. when + * the first formula is asserted, a call to simplify() is issued, a scope is + * pushed, etc. + */ + bool d_fullyInited; + + /** + * Whether or not a notifyCheckSat call has been made, which corresponds to + * when a checkEntailed() or checkSatisfiability() has already been + * made through the SmtEngine. If true, and incrementalSolving is false, + * then attempting an additional checks for satisfiability will fail with + * a ModalException during notifyCheckSat. + */ + bool d_queryMade; + + /** + * Internal status flag to indicate whether we have been issued a + * notifyCheckSat call and have yet to process the "postsolve" methods of + * SmtEngine via SmtEngine::notifyPostSolvePre/notifyPostSolvePost. + */ + bool d_needPostsolve; + + /** + * Most recent result of last checkSatisfiability/checkEntailed in the + * SmtEngine. + */ + Result d_status; + + /** + * The expected status of the next satisfiability check. + */ + Result d_expectedStatus; + + /** The SMT mode, for details see enumeration above. */ + SmtMode d_smtMode; + + /** + * The input file name or the name set through (set-info :filename ...), if + * any. + */ + std::string d_filename; +}; + +} // namespace smt +} // namespace CVC4 + +#endif diff --git a/src/smt/smt_mode.cpp b/src/smt/smt_mode.cpp new file mode 100644 index 000000000..b97983854 --- /dev/null +++ b/src/smt/smt_mode.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \file smt_mode.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Enumeration type for the mode of an SmtEngine. + **/ + +#include "smt/smt_mode.h" + +#include <iostream> + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, SmtMode m) +{ + switch (m) + { + case SmtMode::START: out << "START"; break; + case SmtMode::ASSERT: out << "ASSERT"; break; + case SmtMode::SAT: out << "SAT"; break; + case SmtMode::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; + case SmtMode::UNSAT: out << "UNSAT"; break; + case SmtMode::ABDUCT: out << "ABDUCT"; break; + case SmtMode::INTERPOL: out << "INTERPOL"; break; + default: out << "SmtMode!Unknown"; break; + } + return out; +} + +} // namespace CVC4 diff --git a/src/smt/smt_mode.h b/src/smt/smt_mode.h new file mode 100644 index 000000000..4afd56f54 --- /dev/null +++ b/src/smt/smt_mode.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file smt_mode.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Enumeration type for the mode of an SmtEngine. + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__SMT__SMT_MODE_H +#define CVC4__SMT__SMT_MODE_H + +#include <iosfwd> + +namespace CVC4 { + +/** + * The mode of the solver, which is an extension of 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 class SmtMode +{ + // the initial state of the solver + START, + // normal state of the solver, after assert/push/pop/declare/define + ASSERT, + // immediately after a check-sat returning "sat" + SAT, + // immediately after a check-sat returning "unknown" + SAT_UNKNOWN, + // immediately after a check-sat returning "unsat" + UNSAT, + // immediately after a successful call to get-abduct + ABDUCT, + // immediately after a successful call to get-interpol + INTERPOL +}; +/** + * Writes a SmtMode to a stream. + * + * @param out The stream to write to + * @param m The mode to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, SmtMode m); + +} // namespace CVC4 + +#endif diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index a746040f5..6086abcdd 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -176,7 +176,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); d_zero = bv::utils::mkZero(16); diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 24dd5ae62..f0253fdbf 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -139,7 +139,7 @@ class CnfStreamWhite : public CxxTest::TestSuite { // Notice that this unit test uses the theory engine of a created SMT // engine d_smt. We must ensure that d_smt is properly initialized via // the following call, which constructs its underlying theory engine. - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); d_theoryEngine = d_smt->getTheoryEngine(); d_satSolver = new FakeSatSolver(); diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index 0a50bae2d..9ab7637e0 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -52,7 +52,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); } void tearDown() override diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index 347289693..541c387dd 100644 --- a/test/unit/theory/sequences_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -49,7 +49,7 @@ class SequencesRewriterWhite : public CxxTest::TestSuite d_em = new ExprManager; d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); d_rewriter = new ExtendedRewriter(true); d_nm = NodeManager::currentNM(); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 58c85c8aa..dd0be5550 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -112,7 +112,7 @@ public: // Notice that this unit test uses the theory engine of a created SMT // engine d_smt. We must ensure that d_smt is properly initialized via // the following call, which constructs its underlying theory engine. - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]->setOutputChannel( d_outputChannel); diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h index e6110256a..0483d0cd9 100644 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -43,7 +43,7 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite d_em = new ExprManager; d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); d_nm = NodeManager::currentNM(); } diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index f7391d64a..ff1ce31b6 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -75,7 +75,7 @@ public: // Notice that this unit test uses the theory engine of a created SMT // engine d_smt. We must ensure that d_smt is properly initialized via // the following call, which constructs its underlying theory engine. - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); EagerBitblaster* bb = new EagerBitblaster( dynamic_cast<TheoryBV*>( d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]), diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index fbcfbdb37..a67d0aeb2 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -210,7 +210,7 @@ public: // Notice that this unit test uses the theory engine of a created SMT // engine d_smt. We must ensure that d_smt is properly initialized via // the following call, which constructs its underlying theory engine. - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); d_theoryEngine = d_smt->getTheoryEngine(); for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) { delete d_theoryEngine->d_theoryOut[id]; diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h index 1884f2c72..38b0d774f 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h @@ -65,7 +65,7 @@ void BvInstantiatorWhite::setUp() d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); } void BvInstantiatorWhite::tearDown() diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h index b6726e540..dff4b2e98 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.h +++ b/test/unit/theory/theory_sets_type_enumerator_white.h @@ -39,7 +39,7 @@ class SetEnumeratorWhite : public CxxTest::TestSuite d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); d_scope = new SmtScope(d_smt); - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); } void tearDown() override diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 5ed7afbe1..5da5a7c62 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -180,7 +180,7 @@ class TheoryBlack : public CxxTest::TestSuite { // Notice that this unit test uses the theory engine of a created SMT // engine d_smt. We must ensure that d_smt is properly initialized via // the following call, which constructs its underlying theory engine. - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); // guard against duplicate statistics assertion errors delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN]; delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN]; diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index cf1f002aa..c86408a52 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -44,7 +44,7 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite { d_smt = new SmtEngine(d_em); d_nm = NodeManager::fromExprManager(d_em); d_scope = new SmtScope(d_smt); - d_smt->finalOptionsAreSet(); + d_smt->finishInit(); } void tearDown() override |