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.

1 files changed, 11 insertions, 2 deletions

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();