summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/expr/symbol_table.cpp2
-rw-r--r--src/expr/symbol_table.h1
-rw-r--r--src/parser/antlr_input.h5
-rw-r--r--src/printer/cvc/cvc_printer.cpp1
-rw-r--r--src/printer/tptp/tptp_printer.cpp1
-rw-r--r--src/proof/sat_proof.h2
-rw-r--r--src/prop/cnf_stream.cpp1
-rw-r--r--src/prop/prop_engine.cpp1
-rw-r--r--src/prop/sat_proof_manager.h1
-rw-r--r--src/smt/model.h2
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback