Make ExprManager constructor private (#4669)

This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.

9 files changed, 147 insertions, 117 deletions

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index f07612119..f671fc869 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -17,15 +17,16 @@
 #include <cxxtest/TestSuite.h>
 
 //Used in some of the tests
-#include <vector>
 #include <sstream>
+#include <vector>
 
+#include "api/cvc4cpp.h"
+#include "expr/attribute.h"
 #include "expr/expr_manager.h"
-#include "expr/node_value.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/node.h"
-#include "expr/attribute.h"
+#include "expr/node_value.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -35,27 +36,20 @@ using namespace CVC4::smt;
 using namespace std;
 
 class AttributeBlack : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_exprManager;
-  NodeManager* d_nodeManager;
-  SmtEngine* d_smtEngine;
-  SmtScope* d_scope;
-
  public:
   void setUp() override
   {
-    d_exprManager = new ExprManager();
+    d_slv = new api::Solver();
+    d_exprManager = d_slv->getExprManager();
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
-    d_smtEngine = new SmtEngine(d_exprManager);
+    d_smtEngine = d_slv->getSmtEngine();
     d_scope = new SmtScope(d_smtEngine);
   }
 
   void tearDown() override
   {
     delete d_scope;
-    delete d_smtEngine;
-    delete d_exprManager;
+    delete d_slv;
   }
 
   struct PrimitiveIntAttributeId {};
@@ -135,4 +129,10 @@ private:
     delete node;
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_exprManager;
+  NodeManager* d_nodeManager;
+  SmtEngine* d_smtEngine;
+  SmtScope* d_scope;
 };
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index d28553e08..c632b913e 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -19,56 +19,28 @@
 #include <sstream>
 #include <string>
 
-#include "expr/expr_manager.h"
-#include "expr/expr.h"
+#include "api/cvc4cpp.h"
 #include "base/exception.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
 using namespace std;
 
 class ExprManagerPublic : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_exprManager;
-
-  void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) {
-    std::vector<Expr> worklist;
-    worklist.push_back(expr);
-
-    unsigned int childrenFound = 0;
-
-    while( !worklist.empty() ) {
-      Expr current = worklist.back();
-      worklist.pop_back();
-      if( current.getKind() == kind ) {
-        for( unsigned int i = 0; i < current.getNumChildren(); ++i ) {
-          worklist.push_back( current[i] );
-        }
-      } else {
-        childrenFound++;
-      }
-    }
-
-    TS_ASSERT_EQUALS( childrenFound, numChildren );
-  }
-
-  std::vector<Expr> mkVars(Type type, unsigned int n) {
-    std::vector<Expr> vars;
-    for( unsigned int i = 0; i < n; ++i ) {
-      vars.push_back( d_exprManager->mkVar(type) );
-    }
-    return vars;
-  }
-
  public:
-  void setUp() override { d_exprManager = new ExprManager; }
+  void setUp() override
+  {
+    d_slv = new api::Solver();
+    d_exprManager = d_slv->getExprManager();
+  }
 
   void tearDown() override
   {
     try
     {
-      delete d_exprManager;
+      delete d_slv;
     }
     catch (Exception& e)
     {
@@ -128,4 +100,44 @@ private:
                      IllegalArgumentException&);
   }
 
+ private:
+  void checkAssociative(Expr expr, Kind kind, unsigned int numChildren)
+  {
+    std::vector<Expr> worklist;
+    worklist.push_back(expr);
+
+    unsigned int childrenFound = 0;
+
+    while (!worklist.empty())
+    {
+      Expr current = worklist.back();
+      worklist.pop_back();
+      if (current.getKind() == kind)
+      {
+        for (unsigned int i = 0; i < current.getNumChildren(); ++i)
+        {
+          worklist.push_back(current[i]);
+        }
+      }
+      else
+      {
+        childrenFound++;
+      }
+    }
+
+    TS_ASSERT_EQUALS(childrenFound, numChildren);
+  }
+
+  std::vector<Expr> mkVars(Type type, unsigned int n)
+  {
+    std::vector<Expr> vars;
+    for (unsigned int i = 0; i < n; ++i)
+    {
+      vars.push_back(d_exprManager->mkVar(type));
+    }
+    return vars;
+  }
+
+  api::Solver* d_slv;
+  ExprManager* d_exprManager;
 };
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 09452cc7a..86de45fe9 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -19,9 +19,10 @@
 #include <sstream>
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "base/exception.h"
-#include "expr/expr_manager.h"
 #include "expr/expr.h"
+#include "expr/expr_manager.h"
 #include "options/options.h"
 
 using namespace CVC4;
@@ -29,27 +30,6 @@ using namespace CVC4::kind;
 using namespace std;
 
 class ExprPublic : public CxxTest::TestSuite {
-private:
-
-  Options opts;
-
-  ExprManager* d_em;
-
-  Expr* a_bool;
-  Expr* b_bool;
-  Expr* c_bool_and;
-  Expr* and_op;
-  Expr* plus_op;
-  Type* fun_type;
-  Expr* fun_op;
-  Expr* d_apply_fun_bool;
-  Expr* null;
-
-  Expr* i1;
-  Expr* i2;
-  Expr* r1;
-  Expr* r2;
-
  public:
   void setUp() override
   {
@@ -62,7 +42,8 @@ private:
       free(argv[0]);
       free(argv[1]);
 
-      d_em = new ExprManager(opts);
+      d_slv = new api::Solver(&opts);
+      d_em = d_slv->getExprManager();
 
       a_bool = new Expr(d_em->mkVar("a", d_em->booleanType()));
       b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
@@ -105,7 +86,7 @@ private:
       delete b_bool;
       delete a_bool;
 
-      delete d_em;
+      delete d_slv;
     }
     catch (Exception& e)
     {
@@ -466,4 +447,25 @@ private:
     TS_ASSERT(r1->getExprManager() == d_em);
     TS_ASSERT(r2->getExprManager() == d_em);
   }
+
+ private:
+  Options opts;
+
+  api::Solver* d_slv;
+  ExprManager* d_em;
+
+  Expr* a_bool;
+  Expr* b_bool;
+  Expr* c_bool_and;
+  Expr* and_op;
+  Expr* plus_op;
+  Type* fun_type;
+  Expr* fun_op;
+  Expr* d_apply_fun_bool;
+  Expr* null;
+
+  Expr* i1;
+  Expr* i2;
+  Expr* r1;
+  Expr* r2;
 };
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 17bab05a4..12a55560d 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -19,6 +19,7 @@
 #include <sstream>
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "base/check.h"
 #include "base/exception.h"
 #include "context/context.h"
@@ -33,16 +34,13 @@ using namespace CVC4::context;
 using namespace std;
 
 class SymbolTableBlack : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_exprManager;
-
  public:
   void setUp() override
   {
     try
     {
-      d_exprManager = new ExprManager;
+      d_slv = new api::Solver();
+      d_exprManager = d_slv->getExprManager();
     }
     catch (Exception& e)
     {
@@ -54,7 +52,7 @@ private:
   void tearDown() override
   {
     try {
-      delete d_exprManager;
+      delete d_slv;
     }
     catch (Exception& e)
     {
@@ -164,4 +162,8 @@ private:
     // TODO: What kind of exception gets thrown here?
     TS_ASSERT_THROWS(symtab.popScope(), ScopeException&);
   }
+
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_exprManager;
 };/* class SymbolTableBlack */
diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index 29d9f5dc2..49d6bd9fd 100644
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -17,12 +17,13 @@
 #include <cxxtest/TestSuite.h>
 
 #include <iostream>
-#include <string>
 #include <sstream>
+#include <string>
 
+#include "api/cvc4cpp.h"
+#include "expr/expr_manager.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "expr/expr_manager.h"
 #include "util/cardinality.h"
 
 using namespace CVC4;
@@ -30,12 +31,14 @@ using namespace CVC4::kind;
 using namespace std;
 
 class TypeCardinalityPublic : public CxxTest::TestSuite {
-  ExprManager* d_em;
-
  public:
-  void setUp() override { d_em = new ExprManager(); }
+  void setUp() override
+  {
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
+  }
 
-  void tearDown() override { delete d_em; }
+  void tearDown() override { delete d_slv; }
 
   void testTheBasics()
   {
@@ -226,4 +229,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite {
     }
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_em;
 };/* TypeCardinalityPublic */
diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h
index f42207c49..6e01392ab 100644
--- a/test/unit/theory/regexp_operation_black.h
+++ b/test/unit/theory/regexp_operation_black.h
@@ -14,17 +14,19 @@
  ** Unit tests for symbolic regular expression operations.
  **/
 
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#include "api/cvc4cpp.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/strings/regexp_operation.h"
 
-#include <cxxtest/TestSuite.h>
-#include <iostream>
-#include <memory>
-#include <vector>
-
 using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::smt;
@@ -40,8 +42,9 @@ class RegexpOperationBlack : public CxxTest::TestSuite
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    d_em = new ExprManager(opts);
-    d_smt = new SmtEngine(d_em);
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
+    d_smt = d_slv->getSmtEngine();
     d_scope = new SmtScope(d_smt);
     d_regExpOpr = new RegExpOpr();
 
@@ -56,8 +59,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite
   {
     delete d_regExpOpr;
     delete d_scope;
-    delete d_smt;
-    delete d_em;
+    delete d_slv;
   }
 
   void includes(Node r1, Node r2)
@@ -147,6 +149,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite
   }
 
  private:
+  api::Solver* d_slv;
   ExprManager* d_em;
   SmtEngine* d_smt;
   SmtScope* d_scope;
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 37999b73a..45d13d416 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -17,14 +17,15 @@
 #include <cxxtest/TestSuite.h>
 
 //Used in some of the tests
-#include <vector>
 #include <sstream>
+#include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
-#include "expr/node_value.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/node.h"
+#include "expr/node_value.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
@@ -40,8 +41,9 @@ class TheoryBlack : public CxxTest::TestSuite {
  public:
   void setUp() override
   {
-    d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
+    d_smt = d_slv->getSmtEngine();
     d_scope = new SmtScope(d_smt);
     // Ensure that the SMT engine is fully initialized (required for the
     // rewriter)
@@ -53,8 +55,7 @@ class TheoryBlack : public CxxTest::TestSuite {
   void tearDown() override
   {
     delete d_scope;
-    delete d_smt;
-    delete d_em;
+    delete d_slv;
   }
 
   void testArrayConst() {
@@ -149,6 +150,7 @@ class TheoryBlack : public CxxTest::TestSuite {
   }
 
  private:
+  api::Solver* d_slv;
   ExprManager* d_em;
   SmtEngine* d_smt;
   NodeManager* d_nm;
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 3b00fa192..bf0163317 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -16,6 +16,7 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "api/cvc4cpp.h"
 #include "expr/array_store_all.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
@@ -27,18 +28,14 @@ using namespace CVC4;
 using namespace std;
 
 class ArrayStoreAllBlack : public CxxTest::TestSuite {
-  ExprManager* d_em;
-
  public:
   void setUp() override
   {
-    d_em = new ExprManager();
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
   }
 
-  void tearDown() override
-  {
-    delete d_em;
-  }
+  void tearDown() override { delete d_slv; }
 
   void testStoreAll() {
     Type usort = d_em->mkSort("U");
@@ -80,4 +77,7 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite {
                                    d_em->mkConst(Rational(0)))));
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_em;
 }; /* class ArrayStoreAllBlack */
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index f69cc12ea..ac27acfb5 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -15,8 +15,10 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "expr/datatype.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
@@ -27,14 +29,11 @@ using namespace CVC4;
 using namespace std;
 
 class DatatypeBlack : public CxxTest::TestSuite {
-
-  ExprManager* d_em;
-  ExprManagerScope* d_scope;
-
  public:
   void setUp() override
   {
-    d_em = new ExprManager();
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
     d_scope = new ExprManagerScope(*d_em);
     Debug.on("datatypes");
     Debug.on("groundterms");
@@ -43,7 +42,7 @@ class DatatypeBlack : public CxxTest::TestSuite {
   void tearDown() override
   {
     delete d_scope;
-    delete d_em;
+    delete d_slv;
   }
 
   void testEnumeration() {
@@ -436,4 +435,8 @@ class DatatypeBlack : public CxxTest::TestSuite {
     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt);
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_em;
+  ExprManagerScope* d_scope;
 };/* class DatatypeBlack */