Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)

This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.

The changes that were required for this PR include:

The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.

4 files changed, 6 insertions, 19 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index a5ce1bed0..bf12ee87d 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -35,7 +35,6 @@
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "smt/command.h"
-#include "util/resource_manager.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -47,8 +46,7 @@ Parser::Parser(api::Solver* solver,
                Input* input,
                bool strictMode,
                bool parseOnly)
-    : d_resourceManager(solver->getExprManager()->getResourceManager()),
-      d_input(input),
+    : d_input(input),
       d_symtabAllocated(),
       d_symtab(&d_symtabAllocated),
       d_assertionLevel(0),
@@ -743,19 +741,12 @@ Command* Parser::nextCommand()
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
-  if (cmd != NULL && dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
-      dynamic_cast<QuitCommand*>(cmd) == NULL) {
-    // don't count set-option commands as to not get stuck in an infinite
-    // loop of resourcing out
-    d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
-  }
   return cmd;
 }
 
 api::Term Parser::nextExpression()
 {
   Debug("parser") << "nextExpression()" << std::endl;
-  d_resourceManager->spendResource(ResourceManager::Resource::ParseStep);
   api::Term result;
   if (!done()) {
     try {
@@ -920,8 +911,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
 
 api::Term Parser::mkStringConstant(const std::string& s)
 {
-  ExprManager* em = d_solver->getExprManager();
-  if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage()))
+  if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
   {
     return api::Term(d_solver, d_solver->mkString(s, true).getExpr());
   }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 84dd4be0c..b993b08fb 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -135,8 +135,6 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
 class CVC4_PUBLIC Parser {
   friend class ParserBuilder;
 private:
- /** The resource manager associated with this expr manager */
- ResourceManager* d_resourceManager;
 
  /** The input that we're parsing. */
  Input* d_input;
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index aba409109..46a2e2c59 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -332,8 +332,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
 
 bool Smt2::isHoEnabled() const
 {
-  return getLogic().isHigherOrder()
-         && d_solver->getExprManager()->getOptions().getUfHo();
+  return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo();
 }
 
 bool Smt2::logicIsSet() {
@@ -999,7 +998,7 @@ void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt,
 
 InputLanguage Smt2::getLanguage() const
 {
-  return d_solver->getExprManager()->getOptions().getInputLanguage();
+  return d_solver->getOptions().getInputLanguage();
 }
 
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
@@ -1162,7 +1161,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
   }
   // Second phase: apply the arguments to the parse op
-  const Options& opts = d_solver->getExprManager()->getOptions();
+  const Options& opts = d_solver->getOptions();
   // handle special cases
   if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull())
   {
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 403cab42b..cb4d3fd9e 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -311,7 +311,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     isBuiltinKind = true;
   }
   assert(kind != api::NULL_EXPR);
-  const Options& opts = d_solver->getExprManager()->getOptions();
+  const Options& opts = d_solver->getOptions();
   // Second phase: apply parse op to the arguments
   if (isBuiltinKind)
   {