Fully decouple SmtEngine and the Expr layer (#5532)

This removes the remaining dependencies of SmtEngine on the Expr layer. It now takes a NodeManager instead of a ExprManager.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 9b79b5c45b0f5e7abd422fb97b7f33f076619a17..5eabcfe62400a9c2fe40d2fdf555b372fd73a15f 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3093,7 +3093,7 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 Solver::Solver(Options* opts)
 {
   d_exprMgr.reset(new ExprManager);
-  d_smtEngine.reset(new SmtEngine(d_exprMgr.get(), opts));
+  d_smtEngine.reset(new SmtEngine(d_exprMgr->getNodeManager(), opts));
   d_smtEngine->setSolver(this);
   Options& o = d_smtEngine->getOptions();
   d_rng.reset(new Random(o[options::seed]));

diff --git a/src/expr/type.h b/src/expr/type.h
index 69a8363dc2d7d13d5a998bebbcb3bd2be3e9f80e..0b923f0274e7d6653712a812ae4a071c9bca62e2 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -33,7 +33,7 @@ class Expr;
 class TypeNode;
 struct CVC4_PUBLIC ExprManagerMapCollection;
 
-class CVC4_PUBLIC SmtEngine;
+class SmtEngine;
 
 class CVC4_PUBLIC Datatype;
 class Record;

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 154166eb704bb8c058bc6ac76564cd157a4fb15f..fa3eb66c0cdd06743d7e7c7aebfb12bcf0cd11d9 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1442,8 +1442,8 @@ void SetUserAttributeCommand::invoke(api::Solver* solver, SymbolManager* sm)
     {
       solver->getSmtEngine()->setUserAttribute(
           d_attr,
-          d_term.getExpr(),
-          api::termVectorToExprs(d_termValues),
+          d_term.getNode(),
+          api::termVectorToNodes(d_termValues),
           d_strValue);
     }
     d_commandStatus = CommandSuccess::instance();

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1d623fdef874bf3e8ac7b0cbc111483088166f4d..161c2eba6739d63e5eabc03895912d33066e8e16 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -73,10 +73,9 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-SmtEngine::SmtEngine(ExprManager* em, Options* optr)
+SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
     : d_state(new SmtEngineState(*this)),
-      d_exprManager(em),
-      d_nodeManager(d_exprManager->getNodeManager()),
+      d_nodeManager(nm),
       d_absValues(new AbstractValues(d_nodeManager)),
       d_asserts(new Assertions(getUserContext(), *d_absValues.get())),
       d_dumpm(new DumpManager(getUserContext())),
@@ -525,14 +524,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
   if (key == "all-statistics")
   {
     vector<SExpr> stats;
-    for (StatisticsRegistry::const_iterator i =
-             NodeManager::fromExprManager(d_exprManager)
-                 ->getStatisticsRegistry()
-                 ->begin();
-         i
-         != NodeManager::fromExprManager(d_exprManager)
-                ->getStatisticsRegistry()
-                ->end();
+    StatisticsRegistry* sr = d_nodeManager->getStatisticsRegistry();
+    for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end();
          ++i)
     {
       vector<SExpr> v;
@@ -1637,7 +1630,6 @@ void SmtEngine::pop() {
 void SmtEngine::reset()
 {
   SmtScope smts(this);
-  ExprManager *em = d_exprManager;
   Trace("smt") << "SMT reset()" << endl;
   if(Dump.isOn("benchmark")) {
     getOutputManager().getPrinter().toStreamCmdReset(
@@ -1647,7 +1639,7 @@ void SmtEngine::reset()
   Options opts;
   opts.copyValues(d_originalOptions);
   this->~SmtEngine();
-  new (this) SmtEngine(em, &opts);
+  new (this) SmtEngine(d_nodeManager, &opts);
   // Restore data set after creation
   notifyStartParsing(filename);
 }
@@ -1713,10 +1705,7 @@ unsigned long SmtEngine::getResourceRemaining() const
   return d_resourceManager->getResourceRemaining();
 }
 
-NodeManager* SmtEngine::getNodeManager() const
-{
-  return d_exprManager->getNodeManager();
-}
+NodeManager* SmtEngine::getNodeManager() const { return d_nodeManager; }
 
 Statistics SmtEngine::getStatistics() const
 {
@@ -1733,20 +1722,15 @@ void SmtEngine::safeFlushStatistics(int fd) const {
 }
 
 void SmtEngine::setUserAttribute(const std::string& attr,
-                                 Expr expr,
-                                 const std::vector<Expr>& expr_values,
+                                 Node expr,
+                                 const std::vector<Node>& expr_values,
                                  const std::string& str_value)
 {
   SmtScope smts(this);
   finishInit();
-  std::vector<Node> node_values;
-  for (std::size_t i = 0, n = expr_values.size(); i < n; i++)
-  {
-    node_values.push_back( expr_values[i].getNode() );
-  }
   TheoryEngine* te = getTheoryEngine();
   Assert(te != nullptr);
-  te->setUserAttribute(attr, expr.getNode(), node_values, str_value);
+  te->setUserAttribute(attr, expr, expr_values, str_value);
 }
 
 void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1c83fa61ffe1c7c06e02827ba5fa721777ab73aa..a55428b5531d146bcbd9f854373ef622ab36301e 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -21,13 +21,12 @@
 
 #include <string>
 #include <vector>
+#include <map>
 
 #include "base/modal_exception.h"
 #include "context/cdhashmap_forward.h"
 #include "context/cdhashset_forward.h"
 #include "context/cdlist_forward.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
 #include "options/options.h"
 #include "smt/logic_exception.h"
 #include "smt/output_manager.h"
@@ -48,9 +47,10 @@ namespace CVC4 {
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
+class TypeNode;
 struct NodeHashFunction;
 
-class SmtEngine;
+class NodeManager;
 class DecisionEngine;
 class TheoryEngine;
 class ProofManager;
@@ -58,6 +58,7 @@ class UnsatCore;
 class LogicRequest;
 class StatisticsRegistry;
 class Printer;
+class ResourceManager;
 
 /* -------------------------------------------------------------------------- */
 
@@ -147,7 +148,7 @@ class CVC4_PUBLIC SmtEngine
    * If provided, optr is a pointer to a set of options that should initialize the values
    * of the options object owned by this class.
    */
-  SmtEngine(ExprManager* em, Options* optr = nullptr);
+  SmtEngine(NodeManager* nm, Options* optr = nullptr);
   /** Destruct the SMT engine.  */
   ~SmtEngine();
 
@@ -691,7 +692,7 @@ class CVC4_PUBLIC SmtEngine
   /**
    * Completely reset the state of the solver, as though destroyed and
    * recreated.  The result is as if newly constructed (so it still
-   * retains the same options structure and ExprManager).
+   * retains the same options structure and NodeManager).
    */
   void reset();
 
@@ -785,9 +786,6 @@ class CVC4_PUBLIC SmtEngine
    */
   unsigned long getResourceRemaining() const;
 
-  /** Permit access to the underlying ExprManager. */
-  ExprManager* getExprManager() const { return d_exprManager; }
-
   /** Permit access to the underlying NodeManager. */
   NodeManager* getNodeManager() const;
 
@@ -806,8 +804,8 @@ class CVC4_PUBLIC SmtEngine
    * In SMT-LIBv2 this is done via the syntax (! expr :attr)
    */
   void setUserAttribute(const std::string& attr,
-                        Expr expr,
-                        const std::vector<Expr>& expr_values,
+                        Node expr,
+                        const std::vector<Node>& expr_values,
                         const std::string& str_value);
 
   /** Get the options object (const and non-const versions) */
@@ -1013,9 +1011,7 @@ class CVC4_PUBLIC SmtEngine
    */
   std::unique_ptr<smt::SmtEngineState> d_state;
 
-  /** Our expression manager */
-  ExprManager* d_exprManager;
-  /** Our internal expression/node manager */
+  /** Our internal node manager */
   NodeManager* d_nodeManager;
   /** Abstract values */
   std::unique_ptr<smt::AbstractValues> d_absValues;

diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index ed10e85ae13a3f0d7ae4e5df1cd9c3def55e6eed..ee1ae198fe272c48b7d45decffb7dfa48a629669 100644 (file)
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -48,7 +48,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
   NodeManager* nm = NodeManager::currentNM();
   SmtEngine* smtCurr = smt::currentSmtEngine();
   // must copy the options
-  smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions()));
+  smte.reset(new SmtEngine(nm, &smtCurr->getOptions()));
   smte->setIsInternalSubsolver();
   smte->setLogic(smtCurr->getLogicInfo());
   // set the options

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index f1b782be26830a8bd17242ff6515b644f65c23a2..de179526468501ea1ebee073d29705a43e582429 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -66,7 +66,7 @@ class AttributeWhite : public CxxTest::TestSuite {
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smtEngine = new SmtEngine(d_em);
+    d_smtEngine = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smtEngine);
     d_booleanType = new TypeNode(d_nm->booleanType());
   }

diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 22d3f0d84ef3e171ce64625b85e34805bba669d6..8ac17bbbdc0d3e7d6ef995b5f294d7c3c21adaef 100644 (file)
--- a/test/unit/expr/type_node_white.h
+++ b/test/unit/expr/type_node_white.h
@@ -42,7 +42,7 @@ class TypeNodeWhite : public CxxTest::TestSuite {
   {
     d_em = new ExprManager();
     d_nm = d_em->getNodeManager();
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new NodeManagerScope(d_nm);
   }
 

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h
index 0ff00a7d5a6fdbfc4835cb09641f0de195df56ac..a0a708c5bdb1fdf1510b72e9f9d31a3b9dda79c8 100644 (file)
--- a/test/unit/preprocessing/pass_bv_gauss_white.h
+++ b/test/unit/preprocessing/pass_bv_gauss_white.h
@@ -174,7 +174,7 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
 

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index ae79e1517857575763cc7daa7f2ca9ae66bb97e9..495097a790a76a914316d0f2aa5bf34038400a3f 100644 (file)
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -131,9 +131,9 @@ class CnfStreamWhite : public CxxTest::TestSuite {
   void setUp() override
   {
     d_exprManager = new ExprManager();
-    d_smt = new SmtEngine(d_exprManager);
-    d_smt->d_logic.lock();
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
+    d_smt = new SmtEngine(d_nodeManager);
+    d_smt->d_logic.lock();
     d_scope = new SmtScope(d_smt);
 
     // Notice that this unit test uses the theory engine of a created SMT

diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h
index 421987e3cadfc7de34be79a0deaa9cfda18aeafe..1f33d0fbff29f6b03fa7d642c2b46d7129e9bdb2 100644 (file)
--- a/test/unit/theory/evaluator_white.h
+++ b/test/unit/theory/evaluator_white.h
@@ -50,7 +50,7 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em, &opts);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
   }

diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h
index 1215b4a31700d4ac8775c31be088654f84bb3322..09cb925a305f7d2015f3a2e5f0d2e4b2ab47972e 100644 (file)
--- a/test/unit/theory/sequences_rewriter_white.h
+++ b/test/unit/theory/sequences_rewriter_white.h
@@ -47,12 +47,11 @@ class SequencesRewriterWhite : public CxxTest::TestSuite
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
-    d_smt = new SmtEngine(d_em, &opts);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
     d_rewriter = new ExtendedRewriter(true);
-
-    d_nm = NodeManager::currentNM();
   }
 
   void tearDown() override

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index f0b3f18fe87af2c8e8449836d35eca8e485c2aa3..3475b1dc8cffa1504da263e8f0332828fa93cbce 100644 (file)
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -101,7 +101,7 @@ public:
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_smt->setOption("incremental", CVC4::SExpr(false));
     d_ctxt = d_smt->getContext();
     d_uctxt = d_smt->getUserContext();

diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h
index 4e19ba90e4fb47c674fbf1b67ad851cbdd851246..72fc4284e4004dde2ca30d29699a3a60914a34f0 100644 (file)
--- a/test/unit/theory/theory_bags_normal_form_white.h
+++ b/test/unit/theory/theory_bags_normal_form_white.h
@@ -35,8 +35,8 @@ class BagsNormalFormWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
     d_rewriter.reset(new BagsRewriter(nullptr));
   }

diff --git a/test/unit/theory/theory_bags_rewriter_white.h b/test/unit/theory/theory_bags_rewriter_white.h
index e47e3278455da4e6847a547ab2cdc641c2cb7216..a58e2cdada71dc1b4a10f31fdbaf778cdb683ed7 100644 (file)
--- a/test/unit/theory/theory_bags_rewriter_white.h
+++ b/test/unit/theory/theory_bags_rewriter_white.h
@@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
     d_rewriter.reset(new BagsRewriter(nullptr));
   }

diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h
index e454dfa280011ee8ba2bee9fcbe24f8ada9b1204..8d1db858d6d9ff5827dd5c3d1e7c5c54c2b270fb 100644 (file)
--- a/test/unit/theory/theory_bags_type_rules_white.h
+++ b/test/unit/theory/theory_bags_type_rules_white.h
@@ -34,8 +34,8 @@ class BagsTypeRuleWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
   }
 

diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h
index fae90918a94ba30d2d1fd84388598d95af91eb98..738a51831cdc8cc959c0f6c66a576ca020ddb49d 100644 (file)
--- a/test/unit/theory/theory_bv_rewriter_white.h
+++ b/test/unit/theory/theory_bv_rewriter_white.h
@@ -41,11 +41,10 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
-    d_smt = new SmtEngine(d_em, &opts);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
-
-    d_nm = NodeManager::currentNM();
   }
 
   void tearDown() override

diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
index bfde7866ed19077234162124255a265f33feb77b..f568dc779eb86f5f92050f0b09f1d8f1443e89e5 100644 (file)
--- a/test/unit/theory/theory_bv_white.h
+++ b/test/unit/theory/theory_bv_white.h
@@ -54,7 +54,7 @@ public:
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
   }
 

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 8a99946e59ccf357149d572c274233bc874d7b28..97da7eb8bb3a7d475c157cc367902769f4a837a6 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -192,8 +192,8 @@ public:
 
   void setUp() override {
     d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
 
     d_ctxt = d_smt->getContext();

diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
index f2c5f0e1db5848ee68a97544c91809248a128a73..e19459f15ee78d5b1b6c725553f989a88d118249 100644 (file)
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.h
@@ -63,7 +63,7 @@ void BvInstantiatorWhite::setUp()
 {
   d_em = new ExprManager();
   d_nm = NodeManager::fromExprManager(d_em);
-  d_smt = new SmtEngine(d_em);
+  d_smt = new SmtEngine(d_nm);
   d_scope = new SmtScope(d_smt);
   d_smt->finishInit();
 }

diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index bb44656bc901cb129721cec405e8c74de2e599e9..ac25f60a976eb5951cb66cda5e09dfcd15d7b7f0 100644 (file)
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -222,7 +222,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_smt->setOption("cegqi-full", CVC4::SExpr(true));
     d_smt->setOption("produce-models", CVC4::SExpr(true));
     d_scope = new SmtScope(d_smt);

diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index 965e5926759b9265f999ea57fce3624ec76a4105..1b5ba1dcb317d66f09c82456ac00d4c4634482d9 100644 (file)
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -36,8 +36,8 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
   void setUp() override
   {
     d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
   }

diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index 66c8dc123fee77254f42a4edb2f63c001f3ac33b..00b012745f1e0abb284e02be4c8927fc422da111 100644 (file)
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -28,8 +28,8 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
   {
     d_slv.reset(new Solver());
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
     d_nm.reset(NodeManager::fromExprManager(d_em.get()));
+    d_smt.reset(new SmtEngine(d_nm.get()));
     d_smt->finishInit();
   }
 

diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index 4135adb0c6831ca9c1ec4675a0d125c71c9c7677..dd70dd5b903f74fb3691928c6306a97c95948152 100644 (file)
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -35,13 +35,13 @@ class TheoryStringsSkolemCacheBlack : public CxxTest::TestSuite
   void setUp() override
   {
     d_em.reset(new ExprManager());
-    d_smt.reset(new SmtEngine(d_em.get()));
+    d_nm = NodeManager::fromExprManager(d_em.get());
+    d_smt.reset(new SmtEngine(d_nm));
     d_scope.reset(new SmtScope(d_smt.get()));
     // Ensure that the SMT engine is fully initialized (required for the
     // rewriter)
     d_smt->push();
 
-    d_nm = NodeManager::fromExprManager(d_em.get());
   }
 
   void tearDown() override {}

diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h
index 69143a69c63dd5b5bacd4032941f644e3d55da2b..ce432d3850c3f0eaaf2df00f21d04b08f305c239 100644 (file)
--- a/test/unit/theory/theory_strings_word_white.h
+++ b/test/unit/theory/theory_strings_word_white.h
@@ -38,10 +38,10 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
     d_em = new ExprManager;
-    d_smt = new SmtEngine(d_em, &opts);
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
     d_scope = new SmtScope(d_smt);
 
-    d_nm = NodeManager::currentNM();
   }
 
   void tearDown() override

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 552aeb3c688f13e7f9120e20315897deb6cbefcb..f69830fd888acb2c0715eecb21484415cb312f9d 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -175,7 +175,7 @@ class TheoryBlack : public CxxTest::TestSuite {
   {
     d_em = new ExprManager();
     d_nm = NodeManager::fromExprManager(d_em);
-    d_smt = new SmtEngine(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_ctxt = d_smt->getContext();
     d_uctxt = d_smt->getUserContext();
     d_scope = new SmtScope(d_smt);

diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index ea5a389139ef75fa58e55f8bdda32b71c1b124ab..24bf9922ea2bc8d17edf2eb7f66165e77148debd 100644 (file)
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -42,8 +42,8 @@ class TypeEnumeratorWhite : public CxxTest::TestSuite {
   void setUp() override
   {
     d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
     d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm);
     d_scope = new SmtScope(d_smt);
     d_smt->finishInit();
   }