Remove a few miscellaneous references to the expr layer (#5661)

Leftover from a development branch.

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 28e979b257c06860f5c5e6a9af44cbbe018833dd..4dd43d414a07457aa1c141e2cc204234200994df 100644 (file)
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -27,8 +27,6 @@
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/context.h"
-#include "expr/dtype.h"
-#include "expr/type.h"
 
 namespace CVC4 {
 

diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index b2ca745f78f1a8e32231fd45051200ec6e306ba5..ff8906b2cfbc09e8c3b1cd740238b61b865ff235 100644 (file)
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -24,7 +24,6 @@
 #include <vector>
 
 #include "base/exception.h"
-#include "expr/type.h"
 
 namespace CVC4 {
 

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 46913ded1cb4eb95d73693ea577ad7bc0960febe..d4dbad5c49cbf125f86764c08b9c2207813ad9e2 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -37,11 +37,6 @@
 #include "util/rational.h"
 
 namespace CVC4 {
-
-class Command;
-class Type;
-class FunctionType;
-
 namespace parser {
 
 /** Wrapper around an ANTLR3 input stream. */

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 6c9009e584ffd8a4274bff4e63f44e9eee1f8d92..173e67fd9e33d82ab58385e216d9ac646b7f45bc 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -25,7 +25,6 @@
 #include <vector>
 
 #include "expr/dtype.h"
-#include "expr/expr.h"  // for ExprSetDepth etc..
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "expr/node_visitor.h"
 #include "expr/sequence.h"

diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 1c37c3edc5c62ffc8582fce3ba1ac07e66b9f20d..bb2ab47bd554472b0a572da849ae0b2b48267396 100644 (file)
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -20,7 +20,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include "expr/expr.h"            // for ExprSetDepth etc..
 #include "expr/node_manager.h"    // for VarNameAttr
 #include "options/language.h"     // for LANG_AST
 #include "options/smt_options.h"  // for unsat cores

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 27c98d62a31e20b678c23d4a45d23807f487153d..a3ce3aa4d07fe252d31cd5cec9310b137e0341dd 100644 (file)
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -27,7 +27,7 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdmaybe.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 #include "util/statistics_registry.h"

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6a4990c2b42d7cdaee3cb6317ceb32370162b9c0..ac0c7819a69651207774216b4e81df7ce6beed30 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -21,7 +21,6 @@
 
 #include "base/check.h"
 #include "base/output.h"
-#include "expr/expr.h"
 #include "expr/node.h"
 #include "options/bv_options.h"
 #include "proof/clause_id.h"

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 81fadb709b38cd2a1f7f33dce2edf25225961234..8ea3507f093a04fe0fa3b4eaaa59934e5ede96ea 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -23,7 +23,6 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "decision/decision_engine.h"
-#include "expr/expr.h"
 #include "options/base_options.h"
 #include "options/decision_options.h"
 #include "options/main_options.h"

diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 9dd162e483b18124fd8fb3538ce0d9dd56d53355..0555e7ba7874f63792f80ae57562fdf90d7dee1e 100644 (file)
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -19,7 +19,6 @@
 
 #include "context/cdhashset.h"
 #include "expr/buffered_proof_generator.h"
-#include "expr/expr.h"
 #include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
 #include "expr/proof.h"

diff --git a/src/smt/model.h b/src/smt/model.h
index 18675040a1501a865a31631fee6c09e88465410e..e7c2434a652624ea52165a3a044e5b5e30f13c37 100644 (file)
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -20,7 +20,7 @@
 #include <iosfwd>
 #include <vector>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "theory/theory_model.h"
 #include "util/cardinality.h"