Split SmtEngineState from SmtEngine (#4855)

This splits a utility for tracking the "basic" state of the SmtEngine. This class tracks its high-level state, including the "SMT mode", last/expected status and manages the contexts. It is not responsible more detailed state information (e.g. the assertions).

1 files changed, 169 insertions, 289 deletions

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 */