Delete Expr layer. (#6117)

15 files changed, 18 insertions, 35 deletions

diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index 442a57e34..7b42d6a76 100644
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -29,8 +29,6 @@
 #include <string>
 
 #include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/expr_iomanip.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index c008018b2..223028d4c 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -19,7 +19,6 @@
 #include <sstream>
 
 #include "api/cvc4cpp.h"
-#include "expr/expr_manager.h"
 #include "options/options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp
index b536fb932..3c1651155 100644
--- a/test/unit/expr/node_black.cpp
+++ b/test/unit/expr/node_black.cpp
@@ -22,7 +22,6 @@
 #include "api/cvc4cpp.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
-#include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
diff --git a/test/unit/expr/node_traversal_black.cpp b/test/unit/expr/node_traversal_black.cpp
index 1c18abdb5..e443ff685 100644
--- a/test/unit/expr/node_traversal_black.cpp
+++ b/test/unit/expr/node_traversal_black.cpp
@@ -19,7 +19,6 @@
 #include <string>
 #include <vector>
 
-#include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
diff --git a/test/unit/expr/symbol_table_black.cpp b/test/unit/expr/symbol_table_black.cpp
index 68b822bac..10fb52f6d 100644
--- a/test/unit/expr/symbol_table_black.cpp
+++ b/test/unit/expr/symbol_table_black.cpp
@@ -20,10 +20,8 @@
 #include "base/check.h"
 #include "base/exception.h"
 #include "context/context.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/kind.h"
 #include "expr/symbol_table.h"
-#include "expr/type.h"
 #include "test_api.h"
 
 namespace CVC4 {
diff --git a/test/unit/expr/type_cardinality_black.cpp b/test/unit/expr/type_cardinality_black.cpp
index 08e863bc4..58024fa53 100644
--- a/test/unit/expr/type_cardinality_black.cpp
+++ b/test/unit/expr/type_cardinality_black.cpp
@@ -18,7 +18,6 @@
 
 #include "expr/kind.h"
 #include "expr/node_manager.h"
-#include "expr/type.h"
 #include "test_node.h"
 #include "util/cardinality.h"
 
diff --git a/test/unit/expr/type_node_white.cpp b/test/unit/expr/type_node_white.cpp
index 4412ec95a..f364e40fc 100644
--- a/test/unit/expr/type_node_white.cpp
+++ b/test/unit/expr/type_node_white.cpp
@@ -18,8 +18,6 @@
 #include <sstream>
 #include <string>
 
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
 #include "expr/node_manager.h"
 #include "expr/type_node.h"
 #include "smt/smt_engine.h"
diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp
index b35f07f18..c600e3477 100644
--- a/test/unit/main/interactive_shell_black.cpp
+++ b/test/unit/main/interactive_shell_black.cpp
@@ -18,7 +18,6 @@
 #include <vector>
 
 #include "api/cvc4cpp.h"
-#include "expr/expr_manager.h"
 #include "expr/symbol_manager.h"
 #include "main/interactive_shell.h"
 #include "options/base_options.h"
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index ece6168e9..87556d53d 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -19,8 +19,6 @@
 
 #include "api/cvc4cpp.h"
 #include "base/output.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
 #include "expr/symbol_manager.h"
 #include "options/base_options.h"
 #include "options/language.h"
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index 978914d3e..cf343f006 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -28,7 +28,7 @@ class TestNode : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager(nullptr));
+    d_nodeManager.reset(new NodeManager());
     d_scope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_boolTypeNode.reset(new TypeNode(d_nodeManager->booleanType()));
     d_bvTypeNode.reset(new TypeNode(d_nodeManager->mkBitVectorType(2)));
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 718a9d2b6..e55c00e65 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -41,7 +41,7 @@ class TestSmt : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager(nullptr));
+    d_nodeManager.reset(new NodeManager());
     d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
     d_smtEngine->finishInit();
@@ -57,7 +57,7 @@ class TestSmtNoFinishInit : public TestInternal
  protected:
   void SetUp() override
   {
-    d_nodeManager.reset(new NodeManager(nullptr));
+    d_nodeManager.reset(new NodeManager());
     d_nmScope.reset(new NodeManagerScope(d_nodeManager.get()));
     d_smtEngine.reset(new SmtEngine(d_nodeManager.get()));
   }
diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index 6952fb320..1447670f3 100644
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -86,7 +86,7 @@ TEST_F(TestTheoryWhiteBv, mkUmulo)
         kind::DISTINCT, mkExtract(mul, 2 * w - 1, w), mkZero(w));
     Node rhs = mkUmulo(x, y);
     Node eq = d_nodeManager->mkNode(kind::DISTINCT, lhs, rhs);
-    d_smtEngine->assertFormula(eq.toExpr());
+    d_smtEngine->assertFormula(eq);
     Result res = d_smtEngine->checkSat();
     ASSERT_EQ(res.isSat(), Result::UNSAT);
     d_smtEngine->pop();
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
index 54b4ce55b..7b6a73d2c 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
@@ -88,7 +88,7 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
     }
     Node body = d_nodeManager->mkNode(k, x, d_t);
     Node scr = d_nodeManager->mkNode(EXISTS, d_bvarlist, body);
-    Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr();
+    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
     Result res = d_smtEngine->checkSat(a);
     ASSERT_EQ(res.d_sat, Result::UNSAT);
   }
@@ -117,14 +117,14 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
                              litk, d_nodeManager->mkNode(k, d_s, d_x), d_t);
     Node scr =
         d_nodeManager->mkNode(EXISTS, d_bvarlist, pol ? body : body.notNode());
-    Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr();
+    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
     Result res = d_smtEngine->checkSat(a);
     if (res.d_sat == Result::SAT)
     {
       std::cout << std::endl;
-      std::cout << "s " << d_smtEngine->getValue(d_s.toExpr()) << std::endl;
-      std::cout << "t " << d_smtEngine->getValue(d_t.toExpr()) << std::endl;
-      std::cout << "x " << d_smtEngine->getValue(d_x.toExpr()) << std::endl;
+      std::cout << "s " << d_smtEngine->getValue(d_s) << std::endl;
+      std::cout << "t " << d_smtEngine->getValue(d_t) << std::endl;
+      std::cout << "x " << d_smtEngine->getValue(d_x) << std::endl;
     }
     ASSERT_EQ(res.d_sat, Result::UNSAT);
   }
@@ -173,17 +173,17 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
     Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x});
     Node scr =
         d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
-    Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr();
+    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
     Result res = d_smtEngine->checkSat(a);
     if (res.d_sat == Result::SAT)
     {
       std::cout << std::endl;
       if (!s1.isNull())
-        std::cout << "s1 " << d_smtEngine->getValue(s1.toExpr()) << std::endl;
+        std::cout << "s1 " << d_smtEngine->getValue(s1) << std::endl;
       if (!s2.isNull())
-        std::cout << "s2 " << d_smtEngine->getValue(s2.toExpr()) << std::endl;
-      std::cout << "t " << d_smtEngine->getValue(t.toExpr()) << std::endl;
-      std::cout << "x " << d_smtEngine->getValue(x.toExpr()) << std::endl;
+        std::cout << "s2 " << d_smtEngine->getValue(s2) << std::endl;
+      std::cout << "t " << d_smtEngine->getValue(t) << std::endl;
+      std::cout << "x " << d_smtEngine->getValue(x) << std::endl;
     }
     ASSERT_TRUE(res.d_sat == Result::UNSAT);
   }
@@ -213,13 +213,13 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
     Node bvarlist = d_nodeManager->mkNode(BOUND_VAR_LIST, {x});
     Node scr =
         d_nodeManager->mkNode(EXISTS, bvarlist, pol ? body : body.notNode());
-    Expr a = d_nodeManager->mkNode(DISTINCT, scl, scr).toExpr();
+    Node a = d_nodeManager->mkNode(DISTINCT, scl, scr);
     Result res = d_smtEngine->checkSat(a);
     if (res.d_sat == Result::SAT)
     {
       std::cout << std::endl;
-      std::cout << "t " << d_smtEngine->getValue(t.toExpr()) << std::endl;
-      std::cout << "x " << d_smtEngine->getValue(x.toExpr()) << std::endl;
+      std::cout << "t " << d_smtEngine->getValue(t) << std::endl;
+      std::cout << "x " << d_smtEngine->getValue(x) << std::endl;
     }
     ASSERT_TRUE(res.d_sat == Result::UNSAT);
   }
diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
index 693bc0423..540fca6f2 100644
--- a/test/unit/util/array_store_all_white.cpp
+++ b/test/unit/util/array_store_all_white.cpp
@@ -15,8 +15,6 @@
  **/
 
 #include "expr/array_store_all.h"
-#include "expr/expr.h"
-#include "expr/type.h"
 #include "test_smt.h"
 
 namespace CVC4 {
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index 18dc479be..ef24d870d 100644
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -16,10 +16,8 @@
 
 #include <sstream>
 
-#include "api/cvc4cpp.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
-#include "expr/expr.h"
 #include "expr/type_node.h"
 #include "test_smt.h"