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.

5 files changed, 57 insertions, 64 deletions

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_solvers.cpp
index 71676482e..c5bea4860 100644
--- a/test/system/two_smt_engines.cpp
+++ b/test/system/two_solvers.cpp
@@ -17,20 +17,16 @@
 #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);
-  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;
+  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;
 }