From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 29 Jun 2020 22:35:44 +0000 (-0700)
Subject: Make ExprManager constructor private (#4669)
X-Git-Tag: cvc5-1.0.0~3166
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=19054b3b1d427e662d30d4322df2b2f2361353da;p=cvc5.git

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.
---

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 6168a8e22..cd74698d7 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -58,31 +58,34 @@ endmacro()
 
 cvc4_add_example(simple_vc_cxx "" "")
 cvc4_add_example(simple_vc_quant_cxx "" "")
-cvc4_add_example(translator "" ""
-    # argument to binary (for testing)
-    ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
+# TODO(project issue $206): Port example to new API
+# cvc4_add_example(translator "" ""
+#     # argument to binary (for testing)
+#     ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
 
 add_subdirectory(api)
-add_subdirectory(hashsmt)
-add_subdirectory(nra-translate)
-add_subdirectory(sets-translate)
+# TODO(project issue $206): Port example to new API
+# add_subdirectory(hashsmt)
+# add_subdirectory(nra-translate)
+# add_subdirectory(sets-translate)
 
 if(TARGET CVC4::cvc4jar)
   find_package(Java REQUIRED)
   include(UseJava)
 
-  get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE)
-
-  add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}")
-
-  add_test(
-    NAME java/SimpleVC
-    COMMAND
-      ${Java_JAVA_EXECUTABLE}
-        -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
-        -Djava.library.path=${CVC4_JNI_PATH}
-        SimpleVC
-  )
+  ## disabled until bindings for the new API are in place (issue #2284)
+  # get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE)
+  #
+  # add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}")
+  #
+  # add_test(
+  #   NAME java/SimpleVC
+  #   COMMAND
+  #     ${Java_JAVA_EXECUTABLE}
+  #       -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
+  #       -Djava.library.path=${CVC4_JNI_PATH}
+  #       SimpleVC
+  # )
 
   add_subdirectory(api/java)
 endif()
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 31f62db56..0afcec0e4 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -1,20 +1,19 @@
 set(EXAMPLES_API_JAVA
-  BitVectors
-  BitVectorsAndArrays
   ## disabled until bindings for the new API are in place (issue #2284)
-  #CVC4Streams
-  Combination
-  Datatypes
-  Exceptions
-  FloatingPointArith
-  HelloWorld
-  LinearArith
-  ## disabled until bindings for the new API are in place (issue #2284)
-  #PipedInput
-  Relations
-  Statistics
-  Strings
-  UnsatCores
+  # BitVectors
+  # BitVectorsAndArrays
+  # CVC4Streams
+  # Combination
+  # Datatypes
+  # Exceptions
+  # FloatingPointArith
+  # HelloWorld
+  # LinearArith
+  # PipedInput
+  # Relations
+  # Statistics
+  # Strings
+  # UnsatCores
 )
 
 foreach(example ${EXAMPLES_API_JAVA})
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 26d785edc..64c2b12c1 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -16,43 +16,42 @@
  ** identical.
  **/
 
-#include <iostream>
+#include <cvc4/api/cvc4cpp.h>
 
-#include <cvc4/cvc4.h>
+#include <iostream>
 
-using namespace std;
-using namespace CVC4;
+using namespace CVC4::api;
 
 int main() {
-  ExprManager em;
-  SmtEngine smt(&em);
+  Solver slv;
 
   // Prove that for integers x and y:
   //   x > 0 AND y > 0  =>  2x + y >= 3
 
-  Type integer = em.integerType();
+  Sort integer = slv.getIntegerSort();
 
-  Expr x = em.mkVar("x", integer);
-  Expr y = em.mkVar("y", integer);
-  Expr zero = em.mkConst(Rational(0));
+  Term x = slv.mkConst(integer, "x");
+  Term y = slv.mkConst(integer, "y");
+  Term zero = slv.mkReal(0);
 
-  Expr x_positive = em.mkExpr(kind::GT, x, zero);
-  Expr y_positive = em.mkExpr(kind::GT, y, zero);
+  Term x_positive = slv.mkTerm(Kind::GT, x, zero);
+  Term y_positive = slv.mkTerm(Kind::GT, y, zero);
 
-  Expr two = em.mkConst(Rational(2));
-  Expr twox = em.mkExpr(kind::MULT, two, x);
-  Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y);
+  Term two = slv.mkReal(2);
+  Term twox = slv.mkTerm(Kind::MULT, two, x);
+  Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y);
 
-  Expr three = em.mkConst(Rational(3));
-  Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three);
+  Term three = slv.mkReal(3);
+  Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three);
 
-  Expr formula =
-    em.mkExpr(kind::AND, x_positive, y_positive).
-    impExpr(twox_plus_y_geq_3);
+  Term formula =
+      slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3);
 
-  cout << "Checking entailment of formula " << formula << " with CVC4." << endl;
-  cout << "CVC4 should report ENTAILED." << endl;
-  cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl;
+  std::cout << "Checking entailment of formula " << formula << " with CVC4."
+            << std::endl;
+  std::cout << "CVC4 should report ENTAILED." << std::endl;
+  std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula)
+            << std::endl;
 
   return 0;
 }
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 83d011993..4d5767ebb 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -14,64 +14,63 @@
  ** A simple demonstration of the C++ interface for quantifiers. 
  **/
 
-#include <iostream>
+#include <cvc4/api/cvc4cpp.h>
 
-#include <cvc4/cvc4.h>
+#include <iostream>
 
-using namespace std;
-using namespace CVC4;
+using namespace CVC4::api;
 
 int main() {
-  ExprManager em;
-  SmtEngine smt(&em);
+  Solver slv;
 
   // Prove that the following is unsatisfiable:
   //   forall x. P( x ) ^ ~P( 5 )
 
-  Type integer = em.integerType();
-  Type boolean = em.booleanType();
-  Type integerPredicate = em.mkFunctionType(integer, boolean);
-  
-  Expr p = em.mkVar("P", integerPredicate);
-  Expr x = em.mkBoundVar("x", integer);
-  
+  Sort integer = slv.getIntegerSort();
+  Sort boolean = slv.getBooleanSort();
+  Sort integerPredicate = slv.mkFunctionSort(integer, boolean);
+
+  Term p = slv.mkConst(integerPredicate, "P");
+  Term x = slv.mkVar(integer, "x");
+
   // make forall x. P( x )
-  Expr var_list = em.mkExpr(kind::BOUND_VAR_LIST, x);
-  Expr px = em.mkExpr(kind::APPLY_UF, p, x);
-  Expr quantpospx = em.mkExpr(kind::FORALL, var_list, px);
-  cout << "Made expression : " << quantpospx << endl;
-  
+  Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x);
+  Term px = slv.mkTerm(Kind::APPLY_UF, p, x);
+  Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px);
+  std::cout << "Made expression : " << quantpospx << std::endl;
+
   //make ~P( 5 )
-  Expr five = em.mkConst(Rational(5));
-  Expr pfive = em.mkExpr(kind::APPLY_UF, p, five);
-  Expr negpfive = em.mkExpr(kind::NOT, pfive);
-  cout << "Made expression : " << negpfive << endl;
-  
-  Expr formula = em.mkExpr(kind::AND, quantpospx, negpfive);
+  Term five = slv.mkReal(5);
+  Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five);
+  Term negpfive = slv.mkTerm(Kind::NOT, pfive);
+  std::cout << "Made expression : " << negpfive << std::endl;
 
-  smt.assertFormula(formula);
+  Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive);
 
-  cout << "Checking SAT after asserting " << formula << " to CVC4." << endl;
-  cout << "CVC4 should report unsat." << endl;
-  cout << "Result from CVC4 is: " << smt.checkSat() << endl;
+  slv.assertFormula(formula);
 
+  std::cout << "Checking SAT after asserting " << formula << " to CVC4."
+            << std::endl;
+  std::cout << "CVC4 should report unsat." << std::endl;
+  std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
 
-  SmtEngine smtp(&em);
-  
-  // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
-  Expr pattern = em.mkExpr(kind::INST_PATTERN, px);
-  Expr pattern_list = em.mkExpr(kind::INST_PATTERN_LIST, pattern);
-  Expr quantpospx_pattern = em.mkExpr(kind::FORALL, var_list, px, pattern_list);
-  cout << "Made expression : " << quantpospx_pattern << endl;
+  slv.resetAssertions();
 
-  Expr formula_pattern = em.mkExpr(kind::AND, quantpospx_pattern, negpfive);
+  // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
+  Term pattern = slv.mkTerm(Kind::INST_PATTERN, px);
+  Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern);
+  Term quantpospx_pattern =
+      slv.mkTerm(Kind::FORALL, var_list, px, pattern_list);
+  std::cout << "Made expression : " << quantpospx_pattern << std::endl;
 
-  smtp.assertFormula(formula_pattern);
+  Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive);
 
-  cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." << endl;
-  cout << "CVC4 should report unsat." << endl;
-  cout << "Result from CVC4 is: " << smtp.checkSat() << endl;
+  slv.assertFormula(formula_pattern);
 
+  std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4."
+            << std::endl;
+  std::cout << "CVC4 should report unsat." << std::endl;
+  std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
 
   return 0;
 }
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 1809eb2d0..3a4498ab7 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -36,6 +36,10 @@ ${includes}
 
 namespace CVC4 {
 
+namespace api {
+class Solver;
+}
+
 class Expr;
 class SmtEngine;
 class NodeManager;
@@ -45,7 +49,8 @@ struct ExprManagerMapCollection;
 class ResourceManager;
 
 class CVC4_PUBLIC ExprManager {
-private:
+ private:
+  friend api::Solver;
   /** The internal node manager */
   NodeManager* d_nodeManager;
 
@@ -83,7 +88,6 @@ private:
   /** A list of datatypes owned by this expr manager. */
   std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
 
- public:
   /**
    * Creates an expression manager with default options.
    */
@@ -97,6 +101,7 @@ private:
    */
   explicit ExprManager(const Options& options);
 
+ public:
   /**
    * Destroys the expression manager. No will be deallocated at this point, so
    * any expression references that used to be managed by this expression
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 0454b6412..fc3474df4 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/candidate_rewrite_database.h"
 
+#include "api/cvc4cpp.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -137,8 +138,15 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
         // options as the SmtEngine we belong to, where we ensure that
         // produce-models is set.
         bool needExport = false;
-        ExprManager em(nm->getOptions());
-        std::unique_ptr<SmtEngine> rrChecker;
+
+        // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+        // This is only temporarily until we have separate options for each
+        // SmtEngine instance. We should reuse the same ExprManager with
+        // a different SmtEngine (and different options) here, eventually.
+        // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+        api::Solver slv(&nm->getOptions());
+        ExprManager* em = slv.getExprManager();
+        SmtEngine* rrChecker = slv.getSmtEngine();
         ExprManagerMapCollection varMap;
         initializeChecker(rrChecker, em, varMap, crr, needExport);
         Result r = rrChecker->checkSat();
@@ -175,7 +183,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
               if (needExport)
               {
-                Expr erefv = refv.toExpr().exportTo(&em, varMap);
+                Expr erefv = refv.toExpr().exportTo(em, varMap);
                 val = Node::fromExpr(rrChecker->getValue(erefv).exportTo(
                     nm->toExprManager(), varMap));
               }
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 01a46d84a..b209fc6ff 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/expr_miner.h"
 
+#include "api/cvc4cpp.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -68,8 +69,8 @@ Node ExprMiner::convertToSkolem(Node n)
   return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
 }
 
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                                  ExprManager& em,
+void ExprMiner::initializeChecker(SmtEngine* checker,
+                                  ExprManager* em,
                                   ExprManagerMapCollection& varMap,
                                   Node query,
                                   bool& needExport)
@@ -110,10 +111,16 @@ Result ExprMiner::doCheck(Node query)
       return Result(Result::SAT);
     }
   }
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  // This is only temporarily until we have separate options for each
+  // SmtEngine instance. We should reuse the same ExprManager with
+  // a different SmtEngine (and different options) here, eventually.
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
   NodeManager* nm = NodeManager::currentNM();
   bool needExport = false;
-  ExprManager em(nm->getOptions());
-  std::unique_ptr<SmtEngine> smte;
+  api::Solver slv(&nm->getOptions());
+  ExprManager* em = slv.getExprManager();
+  SmtEngine* smte = slv.getSmtEngine();
   ExprManagerMapCollection varMap;
   initializeChecker(smte, em, varMap, queryr, needExport);
   return smte->checkSat();
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index d69ef45b4..eebcebf88 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -89,8 +89,8 @@ class ExprMiner
    * (for instance, model values) must be exported to the current expression
    * manager.
    */
-  void initializeChecker(std::unique_ptr<SmtEngine>& smte,
-                         ExprManager& em,
+  void initializeChecker(SmtEngine* smte,
+                         ExprManager* em,
                          ExprManagerMapCollection& varMap,
                          Node query,
                          bool& needExport);
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 9f08ebec7..4cf65b24a 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -16,6 +16,8 @@
 #include "theory/quantifiers/query_generator.h"
 
 #include <fstream>
+
+#include "api/cvc4cpp.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -157,9 +159,16 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
     Trace("sygus-qgen-check") << "  query: check " << qy << "..." << std::endl;
     NodeManager* nm = NodeManager::currentNM();
     // make the satisfiability query
+    //
+    // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+    // This is only temporarily until we have separate options for each
+    // SmtEngine instance. We should reuse the same ExprManager with
+    // a different SmtEngine (and different options) here, eventually.
+    // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
     bool needExport = false;
-    ExprManager em(nm->getOptions());
-    std::unique_ptr<SmtEngine> queryChecker;
+    api::Solver slv(&nm->getOptions());
+    ExprManager* em = slv.getExprManager();
+    SmtEngine* queryChecker = slv.getSmtEngine();
     ExprManagerMapCollection varMap;
     initializeChecker(queryChecker, em, varMap, qy, needExport);
     Result r = queryChecker->checkSat();
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index de75af083..5784e42c0 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -735,8 +735,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
   {
     addSuccess = false;
     // try a new core
-    std::unique_ptr<SmtEngine> checkSol;
-    initializeSubsolver(checkSol);
+    std::unique_ptr<SmtEngine> checkSol(
+        new SmtEngine(NodeManager::currentNM()->toExprManager()));
+    initializeSubsolver(checkSol.get());
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -775,8 +776,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
         {
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
-          std::unique_ptr<SmtEngine> checkSc;
-          initializeSubsolver(checkSc);
+          std::unique_ptr<SmtEngine> checkSc(
+              new SmtEngine(NodeManager::currentNM()->toExprManager()));
+          initializeSubsolver(checkSc.get());
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 1c34bd73a..d34903805 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
+#include "api/cvc4cpp.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -100,36 +101,6 @@ bool SygusRepairConst::isActive() const
   return !d_base_inst.isNull() && d_allow_constant_grammar;
 }
 
-void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                                         ExprManager& em,
-                                         ExprManagerMapCollection& varMap,
-                                         Node query,
-                                         bool& needExport)
-{
-  if (options::sygusRepairConstTimeout.wasSetByUser())
-  {
-    // To support a separate timeout for the subsolver, we need to create
-    // a separate ExprManager with its own options. This requires that
-    // the expressions sent to the subsolver can be exported from on
-    // ExprManager to another.
-    initializeSubsolverWithExport(checker,
-                                  em,
-                                  varMap,
-                                  query.toExpr(),
-                                  true,
-                                  options::sygusRepairConstTimeout());
-    // renable options disabled by sygus
-    checker->setOption("miniscope-quant", true);
-    checker->setOption("miniscope-quant-fv", true);
-    checker->setOption("quant-split", true);
-  }
-  else
-  {
-    needExport = false;
-    initializeSubsolver(checker, query.toExpr());
-  }
-}
-
 bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                       const std::vector<Node>& candidate_values,
                                       std::vector<Node>& repair_cv,
@@ -258,11 +229,48 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
 
   Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
   // make the satisfiability query
+  //
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  // This is only temporarily until we have separate options for each
+  // SmtEngine instance. We should reuse the same ExprManager with
+  // a different SmtEngine (and different options) here, eventually.
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
   bool needExport = true;
+  std::unique_ptr<SmtEngine> simpleSmte;
+  std::unique_ptr<api::Solver> slv;
+  ExprManager* em = nullptr;
+  SmtEngine* repcChecker = nullptr;
   ExprManagerMapCollection varMap;
-  ExprManager em(nm->getOptions());
-  std::unique_ptr<SmtEngine> repcChecker;
-  initializeChecker(repcChecker, em, varMap, fo_body, needExport);
+
+  if (options::sygusRepairConstTimeout.wasSetByUser())
+  {
+    // To support a separate timeout for the subsolver, we need to create
+    // a separate ExprManager with its own options. This requires that
+    // the expressions sent to the subsolver can be exported from on
+    // ExprManager to another.
+    slv.reset(new api::Solver(&nm->getOptions()));
+    em = slv->getExprManager();
+    repcChecker = slv->getSmtEngine();
+    initializeSubsolverWithExport(repcChecker,
+                                  em,
+                                  varMap,
+                                  fo_body.toExpr(),
+                                  true,
+                                  options::sygusRepairConstTimeout());
+    // renable options disabled by sygus
+    repcChecker->setOption("miniscope-quant", true);
+    repcChecker->setOption("miniscope-quant-fv", true);
+    repcChecker->setOption("quant-split", true);
+  }
+  else
+  {
+    needExport = false;
+    em = nm->toExprManager();
+    simpleSmte.reset(new SmtEngine(em));
+    repcChecker = simpleSmte.get();
+    initializeSubsolver(repcChecker, fo_body.toExpr());
+  }
+
   Result r = repcChecker->checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
@@ -279,7 +287,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
     Node fov_m;
     if (needExport)
     {
-      Expr e_fov = fov.toExpr().exportTo(&em, varMap);
+      Expr e_fov = fov.toExpr().exportTo(em, varMap);
       fov_m = Node::fromExpr(
           repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap));
     }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index dc721b42d..e02ca1f3e 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -209,26 +209,6 @@ class SygusRepairConst
    * If n is in the given logic, this method returns true.
    */
   bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
-  /** initialize checker
-   *
-   * This function initializes the smt engine checker to check the
-   * satisfiability of the argument "query"
-   *
-   * The arguments em and varMap are used for supporting cases where we
-   * want checker to use a different expression manager instead of the current
-   * expression manager. The motivation for this so that different options can
-   * be set for the subcall.
-   *
-   * We update the flag needExport to true if checker is using the expression
-   * manager em. In this case, subsequent expressions extracted from smte
-   * (for instance, model values) must be exported to the current expression
-   * manager.
-   */
-  void initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                         ExprManager& em,
-                         ExprManagerMapCollection& varMap,
-                         Node query,
-                         bool& needExport);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index f8349c834..590fdaa56 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -169,8 +169,9 @@ void SynthEngine::assignConjecture(Node q)
     if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
     {
       // create new smt engine to do quantifier elimination
-      std::unique_ptr<SmtEngine> smt_qe;
-      initializeSubsolver(smt_qe);
+      std::unique_ptr<SmtEngine> smt_qe(
+          new SmtEngine(NodeManager::currentNM()->toExprManager()));
+      initializeSubsolver(smt_qe.get());
       Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                             "QE to obtain single invocation."
                          << std::endl;
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 3386f3691..f529d3fea 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/smt_engine_subsolver.h"
 
+#include "api/cvc4cpp.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
@@ -40,16 +41,14 @@ Result quickCheck(Node& query)
   return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
 }
 
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte)
+void initializeSubsolver(SmtEngine* smte)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  smte.reset(new SmtEngine(nm->toExprManager()));
   smte->setIsInternalSubsolver();
   smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
 }
 
-void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
-                                   ExprManager& em,
+void initializeSubsolverWithExport(SmtEngine* smte,
+                                   ExprManager* em,
                                    ExprManagerMapCollection& varMap,
                                    Node query,
                                    bool needsTimeout,
@@ -62,14 +61,13 @@ void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
   // OptionException.
   try
   {
-    smte.reset(new SmtEngine(&em));
     smte->setIsInternalSubsolver();
     if (needsTimeout)
     {
       smte->setTimeLimit(timeout, true);
     }
     smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
-    Expr equery = query.toExpr().exportTo(&em, varMap);
+    Expr equery = query.toExpr().exportTo(em, varMap);
     smte->assertFormula(equery);
   }
   catch (const CVC4::ExportUnsupportedException& e)
@@ -82,13 +80,13 @@ void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
   }
 }
 
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+void initializeSubsolver(SmtEngine* smte, Node query)
 {
   initializeSubsolver(smte);
   smte->assertFormula(query.toExpr());
 }
 
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+Result checkWithSubsolver(SmtEngine* smte, Node query)
 {
   Assert(query.getType().isBoolean());
   Result r = quickCheck(query);
@@ -130,19 +128,33 @@ Result checkWithSubsolver(Node query,
     }
     return r;
   }
-  std::unique_ptr<SmtEngine> smte;
+
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  // This is only temporarily until we have separate options for each
+  // SmtEngine instance. We should reuse the same ExprManager with
+  // a different SmtEngine (and different options) here, eventually.
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  std::unique_ptr<SmtEngine> simpleSmte;
+  std::unique_ptr<api::Solver> slv;
+  ExprManager* em = nullptr;
+  SmtEngine* smte = nullptr;
   ExprManagerMapCollection varMap;
   NodeManager* nm = NodeManager::currentNM();
-  ExprManager em(nm->getOptions());
   bool needsExport = false;
   if (needsTimeout)
   {
+    slv.reset(new api::Solver(&nm->getOptions()));
+    em = slv->getExprManager();
+    smte = slv->getSmtEngine();
     needsExport = true;
     initializeSubsolverWithExport(
         smte, em, varMap, query, needsTimeout, timeout);
   }
   else
   {
+    em = nm->toExprManager();
+    simpleSmte.reset(new SmtEngine(em));
+    smte = simpleSmte.get();
     initializeSubsolver(smte, query);
   }
   r = smte->checkSat();
@@ -153,7 +165,7 @@ Result checkWithSubsolver(Node query,
       Expr val;
       if (needsExport)
       {
-        Expr ev = v.toExpr().exportTo(&em, varMap);
+        Expr ev = v.toExpr().exportTo(em, varMap);
         val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap);
       }
       else
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 23308e12e..b606657bb 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -34,7 +34,7 @@ namespace theory {
  * This function initializes the smt engine smte as a subsolver, e.g. it
  * creates a new SMT engine and sets the options of the current SMT engine.
  */
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte);
+void initializeSubsolver(SmtEngine* smte);
 
 /**
  * Initialize Smt subsolver with exporting
@@ -52,14 +52,14 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte);
  * manager.
  *
  * @param smte The smt engine pointer to initialize
- * @param em Reference to the expression manager to use
+ * @param em Reference to the expression manager used by smte
  * @param varMap Map used for exporting expressions
  * @param query The query to check
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
-void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
-                                   ExprManager& em,
+void initializeSubsolverWithExport(SmtEngine* smte,
+                                   ExprManager* em,
                                    ExprManagerMapCollection& varMap,
                                    Node query,
                                    bool needsTimeout = false,
@@ -73,7 +73,7 @@ void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
  * exporting since the Options and ExprManager are tied together.
  * TODO: eliminate this dependency (cvc4-projects #120).
  */
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+void initializeSubsolver(SmtEngine* smte, Node query);
 
 /**
  * This returns the result of checking the satisfiability of formula query.
@@ -81,7 +81,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
  * If necessary, smte is initialized to the SMT engine that checked its
  * satisfiability.
  */
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+Result checkWithSubsolver(SmtEngine* smte, Node query);
 
 /**
  * This returns the result of checking the satisfiability of formula query.
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index 420ce8e6f..041d14295 100644
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -32,5 +32,5 @@ cvc4_add_system_test(reset_assertions)
 cvc4_add_system_test(sep_log_api)
 cvc4_add_system_test(smt2_compliance)
 cvc4_add_system_test(statistics)
-cvc4_add_system_test(two_smt_engines)
+cvc4_add_system_test(two_solvers)
 # TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration)
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index 93f5dceb8..315cec7bf 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -19,18 +19,14 @@
 #include <iostream>
 #include <sstream>
 
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
 
-using namespace CVC4;
+using namespace CVC4::api;
 using namespace std;
 
 int main() {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
-  Result r = smt.checkEntailed(em.mkConst(true));
-
-  return (Result::ENTAILED == r) ? 0 : 1;
+  Solver slv;
+  Result r = slv.checkEntailed(slv.mkBoolean(true));
+  return r.isEntailed() ? 0 : 1;
 }
 
diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp
index 2a94dbd98..dc9bd24f6 100644
--- a/test/system/reset_assertions.cpp
+++ b/test/system/reset_assertions.cpp
@@ -20,34 +20,31 @@
 #include <iostream>
 #include <sstream>
 
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
 
-using namespace CVC4;
+using namespace CVC4::api;
 
 int main()
 {
-  ExprManager em;
-  SmtEngine smt(&em);
-
-  smt.setOption("incremental", SExpr(true));
-
-  Type real = em.realType();
-  Expr x = em.mkVar("x", real);
-  Expr four = em.mkConst(Rational(4));
-  Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four);
-  smt.assertFormula(xEqFour);
-  std::cout << smt.checkSat() << std::endl;
-
-  smt.resetAssertions();
-
-  Type elementType = em.integerType();
-  Type indexType = em.integerType();
-  Type arrayType = em.mkArrayType(indexType, elementType);
-  Expr array = em.mkVar("array", arrayType);
-  Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four);
-  Expr ten = em.mkConst(Rational(10));
-  Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten);
-  smt.assertFormula(arrayAtFour_eq_ten);
-  std::cout << smt.checkSat() << std::endl;
+  Solver slv;
+  slv.setOption("incremental", "true");
+
+  Sort real = slv.getRealSort();
+  Term x = slv.mkConst(real, "x");
+  Term four = slv.mkReal(4);
+  Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
+  slv.assertFormula(xEqFour);
+  std::cout << slv.checkSat() << std::endl;
+
+  slv.resetAssertions();
+
+  Sort elementType = slv.getIntegerSort();
+  Sort indexType = slv.getIntegerSort();
+  Sort arrayType = slv.mkArraySort(indexType, elementType);
+  Term array = slv.mkConst(arrayType, "array");
+  Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
+  Term ten = slv.mkReal(10);
+  Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
+  slv.assertFormula(arrayAtFour_eq_ten);
+  std::cout << slv.checkSat() << std::endl;
 }
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp
index 025aaed11..234246112 100644
--- a/test/system/statistics.cpp
+++ b/test/system/statistics.cpp
@@ -15,48 +15,52 @@
  ** minimally functional.
  **/
 
+#include "util/statistics.h"
+
 #include <iostream>
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "smt/smt_engine.h"
 #include "util/sexpr.h"
-#include "util/statistics.h"
 
 using namespace CVC4;
 using namespace std;
 
 int main() {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
-  smt.setOption("incremental", SExpr("true"));
-  Expr x = em.mkVar("x", em.integerType());
-  Expr y = em.mkVar("y", em.integerType());
-  smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5))));
-  Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0)));
-  Result r = smt.checkEntailed(q);
+  api::Solver slv;
+  ExprManager* em = slv.getExprManager();
+  SmtEngine* smt = slv.getSmtEngine();
+  smt->setOption("incremental", SExpr("true"));
+  Expr x = em->mkVar("x", em->integerType());
+  Expr y = em->mkVar("y", em->integerType());
+  smt->assertFormula(em->mkExpr(
+      kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5))));
+  Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0)));
+  Result r = smt->checkEntailed(q);
 
   if (r != Result::NOT_ENTAILED)
   {
     exit(1);
   }
 
-  Statistics stats = smt.getStatistics();
+  Statistics stats = smt->getStatistics();
   for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) {
     cout << "stat " << (*i).first << " is " << (*i).second << endl;
   }
 
-  smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5))));
-  r = smt.checkEntailed(q);
-  Statistics stats2 = smt.getStatistics();
+  smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5))));
+  r = smt->checkEntailed(q);
+  Statistics stats2 = smt->getStatistics();
   bool different = false;
   for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
     cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
     cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
-    if(smt.getStatistic((*i).first) != (*i).second) {
-      cout << "SMT engine reports different value for statistic "
-           << (*i).first << ": " << smt.getStatistic((*i).first) << endl;
+    if (smt->getStatistic((*i).first) != (*i).second)
+    {
+      cout << "SMT engine reports different value for statistic " << (*i).first
+           << ": " << smt->getStatistic((*i).first) << endl;
       exit(1);
     }
     different = different || stats.getStatistic((*i).first) != (*i).second;
diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp
deleted file mode 100644
index 71676482e..000000000
--- a/test/system/two_smt_engines.cpp
+++ /dev/null
@@ -1,36 +0,0 @@
-/*********************                                                        */
-/*! \file two_smt_engines.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Aina Niemetz
- ** 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 A simple test of multiple SmtEngines
- **
- ** A simple test of multiple SmtEngines.
- **/
-
-#include <iostream>
-#include <sstream>
-
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
-
-using namespace CVC4;
-using namespace std;
-
-int main() {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
-  SmtEngine smt2(&em);
-  Result r = smt.checkEntailed(em.mkConst(true));
-  Result r2 = smt2.checkEntailed(em.mkConst(true));
-
-  return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1;
-}
-
diff --git a/test/system/two_solvers.cpp b/test/system/two_solvers.cpp
new file mode 100644
index 000000000..c5bea4860
--- /dev/null
+++ b/test/system/two_solvers.cpp
@@ -0,0 +1,32 @@
+/*********************                                                        */
+/*! \file two_smt_engines.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Aina Niemetz
+ ** 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 A simple test of multiple SmtEngines
+ **
+ ** A simple test of multiple SmtEngines.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "api/cvc4cpp.h"
+
+using namespace CVC4::api;
+using namespace std;
+
+int main() {
+  Solver s1;
+  Solver s2;
+  Result r = s1.checkEntailed(s1.mkBoolean(true));
+  Result r2 = s2.checkEntailed(s2.mkBoolean(true));
+  return r.isEntailed() && r2.isEntailed() ? 0 : 1;
+}
+
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 */