From a026f19e6472a252286f2c5cde9e9d71b835fc95 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 5 Jan 2021 10:07:07 -0600
Subject: [PATCH] Remove a few miscellaneous references to the expr layer
 (#5661)

Leftover from a development branch.
---
 src/expr/symbol_table.cpp         | 2 --
 src/expr/symbol_table.h           | 1 -
 src/parser/antlr_input.h          | 5 -----
 src/printer/cvc/cvc_printer.cpp   | 1 -
 src/printer/tptp/tptp_printer.cpp | 1 -
 src/proof/sat_proof.h             | 2 +-
 src/prop/cnf_stream.cpp           | 1 -
 src/prop/prop_engine.cpp          | 1 -
 src/prop/sat_proof_manager.h      | 1 -
 src/smt/model.h                   | 2 +-
 10 files changed, 2 insertions(+), 15 deletions(-)

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 28e979b25..4dd43d414 100644
--- 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 b2ca745f7..ff8906b2c 100644
--- 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 46913ded1..d4dbad5c4 100644
--- 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 6c9009e58..173e67fd9 100644
--- 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 1c37c3edc..bb2ab47bd 100644
--- 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 27c98d62a..a3ce3aa4d 100644
--- 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 6a4990c2b..ac0c7819a 100644
--- 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 81fadb709..8ea3507f0 100644
--- 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 9dd162e48..0555e7ba7 100644
--- 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 18675040a..e7c2434a6 100644
--- 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"
 
-- 
2.30.2