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.

10 files changed, 37 insertions, 44 deletions

diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h
index f30f6b0ad..eee067ef2 100644
--- a/test/unit/api/grammar_black.h
+++ b/test/unit/api/grammar_black.h
@@ -37,7 +37,7 @@ class GrammarBlack : public CxxTest::TestSuite
 
 void GrammarBlack::setUp() { d_solver.reset(new Solver()); }
 
-void GrammarBlack::tearDown() {}
+void GrammarBlack::tearDown() { d_solver.reset(nullptr); }
 
 void GrammarBlack::testAddRule()
 {
diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
index cbfc9cf23..f9f37a019 100644
--- a/test/unit/api/result_black.h
+++ b/test/unit/api/result_black.h
@@ -22,7 +22,7 @@ class ResultBlack : public CxxTest::TestSuite
 {
  public:
   void setUp() { d_solver.reset(new Solver()); }
-  void tearDown() override {}
+  void tearDown() override { d_solver.reset(nullptr); }
 
   void testIsNull();
   void testEq();
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 4a7b74c8e..d10813f58 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -167,7 +167,7 @@ class SolverBlack : public CxxTest::TestSuite
 
 void SolverBlack::setUp() { d_solver.reset(new Solver()); }
 
-void SolverBlack::tearDown() {}
+void SolverBlack::tearDown() { d_solver.reset(nullptr); }
 
 void SolverBlack::testGetBooleanSort()
 {
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 1b8a7c92f..91242322a 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -22,6 +22,8 @@
 #include <string>
 #include <vector>
 
+#include "api/cvc4cpp.h"
+#include "smt/smt_engine.h"
 #include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
@@ -50,15 +52,13 @@ std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, int N,
 
 class NodeBlack : public CxxTest::TestSuite {
  private:
-  Options opts;
   NodeManager* d_nodeManager;
-  NodeManagerScope* d_scope;
-  TypeNode* d_booleanType;
-  TypeNode* d_realType;
-
+  api::Solver* d_slv;
  public:
   void setUp() override
   {
+    // setup a SMT engine so that options are in scope
+    Options opts;
     char* argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-lang=ast");
@@ -66,18 +66,12 @@ class NodeBlack : public CxxTest::TestSuite {
     free(argv[0]);
     free(argv[1]);
 
-    d_nodeManager = new NodeManager(NULL, opts);
-    d_scope = new NodeManagerScope(d_nodeManager);
-    d_booleanType = new TypeNode(d_nodeManager->booleanType());
-    d_realType = new TypeNode(d_nodeManager->realType());
+    d_slv = new api::Solver(&opts);
+    d_nodeManager = d_slv->getSmtEngine()->getNodeManager();
   }
 
-  void tearDown() override
-  {
-    delete d_realType;
-    delete d_booleanType;
-    delete d_scope;
-    delete d_nodeManager;
+  void tearDown() override { 
+    delete d_slv;
   }
 
   bool imp(bool a, bool b) const { return (!a) || (b); }
@@ -114,12 +108,12 @@ class NodeBlack : public CxxTest::TestSuite {
   void testOperatorEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+    Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
 
     TS_ASSERT(a == a);
     TS_ASSERT(a == b);
@@ -148,12 +142,12 @@ class NodeBlack : public CxxTest::TestSuite {
   void testOperatorNotEquals() {
     Node a, b, c;
 
-    b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     a = b;
     c = a;
 
-    Node d = d_nodeManager->mkSkolem("d", *d_booleanType);
+    Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType());
 
     /*structed assuming operator == works */
     TS_ASSERT(iff(a != a, !(a == a)));
@@ -208,7 +202,7 @@ class NodeBlack : public CxxTest::TestSuite {
   void testOperatorAssign() {
     Node a, b;
     Node c = d_nodeManager->mkNode(
-        NOT, d_nodeManager->mkSkolem("c", *d_booleanType));
+        NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()));
 
     b = c;
     TS_ASSERT(b == c);
@@ -324,8 +318,8 @@ class NodeBlack : public CxxTest::TestSuite {
   void testIteNode() {
     /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
-    Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
-    Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     Node cnd = d_nodeManager->mkNode(OR, a, b);
     Node thenBranch = d_nodeManager->mkConst(true);
@@ -383,8 +377,8 @@ class NodeBlack : public CxxTest::TestSuite {
   void testGetKind() {
     /*inline Kind getKind() const; */
 
-    Node a = d_nodeManager->mkSkolem("a", *d_booleanType);
-    Node b = d_nodeManager->mkSkolem("b", *d_booleanType);
+    Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType());
+    Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType());
 
     Node n = d_nodeManager->mkNode(NOT, a);
     TS_ASSERT(NOT == n.getKind());
@@ -392,8 +386,8 @@ class NodeBlack : public CxxTest::TestSuite {
     n = d_nodeManager->mkNode(EQUAL, a, b);
     TS_ASSERT(EQUAL == n.getKind());
 
-    Node x = d_nodeManager->mkSkolem("x", *d_realType);
-    Node y = d_nodeManager->mkSkolem("y", *d_realType);
+    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType());
+    Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType());
 
     n = d_nodeManager->mkNode(PLUS, x, y);
     TS_ASSERT(PLUS == n.getKind());
@@ -470,9 +464,9 @@ class NodeBlack : public CxxTest::TestSuite {
   // test iterators
   void testIterator() {
     NodeBuilder<> b;
-    Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
-    Node y = d_nodeManager->mkSkolem("y", *d_booleanType);
-    Node z = d_nodeManager->mkSkolem("z", *d_booleanType);
+    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
+    Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType());
+    Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType());
     Node n = b << x << y << z << kind::AND;
 
     {  // iterator
@@ -717,7 +711,7 @@ class NodeBlack : public CxxTest::TestSuite {
   //  This is for demonstrating what a certain type of user error looks like.
   //   Node level0(){
   //     NodeBuilder<> nb(kind::AND);
-  //     Node x = d_nodeManager->mkSkolem("x", *d_booleanType);
+  //     Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType());
   //     nb << x;
   //     nb << x;
   //     return Node(nb.constructNode());
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 9d5a0fc8d..8668f746b 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -209,8 +209,7 @@ class ParserBlack
     d_solver.reset(new api::Solver(&d_options));
   }
 
-  void tearDown() {
-  }
+  void tearDown() { d_solver.reset(nullptr); }
 
  private:
   InputLanguage d_lang;
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 4a30b4179..24dd5ae62 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -145,7 +145,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_satSolver = new FakeSatSolver();
     d_cnfContext = new context::Context();
     d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
-    ResourceManager * rm = d_nodeManager->getResourceManager();
+    ResourceManager* rm = d_smt->getResourceManager();
     d_cnfStream = new CVC4::prop::TseitinCnfStream(
         d_satSolver, d_cnfRegistrar, d_cnfContext, rm);
   }
diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 3fc95b2a5..0a50bae2d 100644
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -48,9 +48,9 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    d_em = new ExprManager(opts);
+    d_em = new ExprManager;
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_em, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finalOptionsAreSet();
   }
diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h
index c9c897f5f..347289693 100644
--- a/test/unit/theory/sequences_rewriter_white.h
+++ b/test/unit/theory/sequences_rewriter_white.h
@@ -46,8 +46,8 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    d_em = new ExprManager(opts);
-    d_smt = new SmtEngine(d_em);
+    d_em = new ExprManager;
+    d_smt = new SmtEngine(d_em, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finalOptionsAreSet();
     d_rewriter = new ExtendedRewriter(true);
diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
index d2284aa8f..e6110256a 100644
--- a/test/unit/theory/theory_bv_rewriter_white.h
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -40,8 +40,8 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    d_em = new ExprManager(opts);
-    d_smt = new SmtEngine(d_em);
+    d_em = new ExprManager;
+    d_smt = new SmtEngine(d_em, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finalOptionsAreSet();
 
diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h
index 2e29d50b8..048d1d707 100644
--- a/test/unit/theory/theory_strings_word_white.h
+++ b/test/unit/theory/theory_strings_word_white.h
@@ -37,8 +37,8 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    d_em = new ExprManager(opts);
-    d_smt = new SmtEngine(d_em);
+    d_em = new ExprManager;
+    d_smt = new SmtEngine(d_em, &opts);
     d_scope = new SmtScope(d_smt);
 
     d_nm = NodeManager::currentNM();