Clean up includes to reduce compile times (#6031)

This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0c94320c3b0bbd65018936c8d08e9b242f4aeba1..7a191cd8ab8a3c984c7453ab311ebfa384103226 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -39,6 +39,8 @@
 #include "base/check.h"
 #include "base/configuration.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
+#include "expr/dtype_selector.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "expr/expr_manager_scope.h"

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index 2a8dc8d1005ca205fbbb3fe768da964652fda76b..cddef79fd1f10a3136029aac6c3584f814da71ae 100644 (file)
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -28,24 +28,24 @@ using namespace std;
 
 namespace CVC4 {
 
-thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL;
+thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr;
 
-LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {}
+LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {}
 
 LastExceptionBuffer::~LastExceptionBuffer() {
-  if(d_contents != NULL){
+  if(d_contents != nullptr){
     free(d_contents);
-    d_contents = NULL;
+    d_contents = nullptr;
   }
 }
 
 void LastExceptionBuffer::setContents(const char* string) {
-  if(d_contents != NULL){
+  if(d_contents != nullptr){
     free(d_contents);
-    d_contents = NULL;
+    d_contents = nullptr;
   }
 
-  if(string != NULL){
+  if(string != nullptr){
     d_contents = strdup(string);
   }
 }
@@ -61,7 +61,7 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
   va_start(args, format);
 
   int n = 512;
-  char* buf = NULL;
+  char* buf = nullptr;
 
   for (int i = 0; i < 2; ++i){
     Assert(n > 0);
@@ -80,9 +80,9 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
       break;
     }
   }
-  // buf is not NULL is an invariant.
+  // buf is not nullptr is an invariant.
   // buf is also 0 terminated.
-  Assert(buf != NULL);
+  Assert(buf != nullptr);
   std::string result(buf);
   delete [] buf;
   va_end(args);
@@ -107,7 +107,7 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
     buf = new char[n];
 
     int size;
-    if(extra == NULL) {
+    if(extra == nullptr) {
       size = snprintf(buf, n, "%s\n%s\n%s",
                       header, function, tail);
     } else {
@@ -129,8 +129,8 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
 #ifdef CVC4_DEBUG
   LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
-  if(buffer != NULL){
-    if(buffer->getContents() == NULL) {
+  if(buffer != nullptr){
+    if(buffer->getContents() == nullptr) {
       buffer->setContents(buf);
     }
   }
@@ -149,7 +149,7 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
     buf = new char[n];
 
     int size;
-    if(extra == NULL) {
+    if(extra == nullptr) {
       size = snprintf(buf, n, "%s.\n%s\n",
                       header, function);
     } else {
@@ -170,8 +170,8 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
 #ifdef CVC4_DEBUG
   LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent();
-  if(buffer != NULL){
-    if(buffer->getContents() == NULL) {
+  if(buffer != nullptr){
+    if(buffer->getContents() == nullptr) {
       buffer->setContents(buf);
     }
   }

diff --git a/src/base/exception.h b/src/base/exception.h
index 1d49d94cce0602b6b054c123cb22c0512a809f75..8a89c99fcf9755fdbfc2aeb016c773f320c60b70 100644 (file)
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -151,7 +151,7 @@ public:
   static void setCurrent(LastExceptionBuffer* buffer) { s_currentBuffer = buffer; }
 
   static const char* currentContents() {
-    return (getCurrent() == NULL) ? NULL : getCurrent()->getContents();
+    return (getCurrent() == nullptr) ? nullptr : getCurrent()->getContents();
   }
 
 private:

diff --git a/src/base/listener.h b/src/base/listener.h
index 15256ab014a90f6a215a7fdd970000b8965da213..5c5a58128e3b7770478a69211deeac0aa8b5cfff 100644 (file)
--- a/src/base/listener.h
+++ b/src/base/listener.h
@@ -20,8 +20,6 @@
 #ifndef CVC4__LISTENER_H
 #define CVC4__LISTENER_H
 
-#include <list>
-
 namespace CVC4 {
 
 /**

diff --git a/src/base/output.h b/src/base/output.h
index 96cb9f8acb32e296af9b91bf5a668920e329cc2b..9de1d9b09adf3adc94ab9fa0cad6a40125415365 100644 (file)
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -21,10 +21,8 @@
 
 #include <ios>
 #include <iostream>
-#include <streambuf>
 #include <string>
 #include <cstdio>
-#include <cstdarg>
 #include <set>
 #include <utility>
 

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index cb5e552acf05554ca00b555f84fcc898fedbe857..0515d7126327bc2934359aee217b972b8018e4c3 100644 (file)
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -20,6 +20,7 @@
 #ifndef CVC4__CONTEXT__CDLIST_H
 #define CVC4__CONTEXT__CDLIST_H
 
+#include <cstring>
 #include <iterator>
 #include <memory>
 #include <string>

diff --git a/src/context/context.cpp b/src/context/context.cpp
index 19be126f8948d2a9d9c7d902ed32dce2a4e930b1..1313daa9ab776f916e71aea8fc7cca5f288e2d3e 100644 (file)
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -16,6 +16,7 @@
 
 
 #include <iostream>
+#include <string>
 #include <vector>
 
 #include "base/check.h"

diff --git a/src/context/context.h b/src/context/context.h
index 15b4307b985cabb80662bda6a484f4ee202cdb5c..afec597478a39c15983853eb31786d54cf32c84a 100644 (file)
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -20,10 +20,8 @@
 #define CVC4__CONTEXT__CONTEXT_H
 
 #include <cstdlib>
-#include <cstring>
 #include <iostream>
 #include <memory>
-#include <new>
 #include <typeinfo>
 #include <vector>
 

diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
index f6753a60142cfa45d80e8aba3d2542ae7887027b..266cfb18a901344a28319fe261083e020ccea563 100644 (file)
--- a/src/expr/buffered_proof_generator.cpp
+++ b/src/expr/buffered_proof_generator.cpp
@@ -15,6 +15,7 @@
 #include "expr/buffered_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 

diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index f774e383dd2e658b0677f60c1d0a476801ffb7ca..da80891a299cff992c7d7d37e66bfea9b90db545 100644 (file)
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -17,17 +17,14 @@
 #ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
 #define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
 
-#include <map>
-#include <vector>
-
 #include "context/cdhashmap.h"
-#include "context/cdhashset.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * The proof generator for buffered steps. This class is a context-dependent
  * mapping from formulas to proof steps. It does not generate ProofNodes until it

diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp
index 694d75db6e569e32661e6437e6370aaddf148ba3..23d6b3ca1dd207cf4f75431f5b9545da909816e9 100644 (file)
--- a/src/expr/datatype_index.cpp
+++ b/src/expr/datatype_index.cpp
@@ -15,6 +15,7 @@
 
 #include <sstream>
 #include <string>
+#include "util/hash.h"
 #include "util/integer.h"
 
 using namespace std;

diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
index c7f170ff6e0c28cd562a494fe6d0a9b0c3ff8e4d..08640e1d582d359719ed98f1e5a1289526f405a9 100644 (file)
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -18,7 +18,6 @@
 #define CVC4__DATATYPE_INDEX_H
 
 #include <iosfwd>
-#include "util/hash.h"
 
 namespace CVC4 {
 

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 5cb76858aa68a2a32b2c9bddf6f2567e98d4e871..f94f0063a185792a27feacc16610b8aa7fe36bd1 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -13,6 +13,7 @@
  **/
 #include "expr/dtype.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/type_matcher.h"
 

diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index e4bae29b87a9614dd41df645b63e5ea4e558ffd4..c68a7d44a45b8ac85b60f4f3645ba208112873ea 100644 (file)
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -20,10 +20,8 @@
 #include <map>
 #include <string>
 #include <vector>
-#include "expr/dtype_cons.h"
-#include "expr/dtype_selector.h"
+#include "expr/attribute.h"
 #include "expr/node.h"
-#include "expr/node_manager_attributes.h"
 #include "expr/type_node.h"
 
 namespace CVC4 {
@@ -76,7 +74,7 @@ struct DTypeUFiniteComputedTag
 typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr;
 // ----------------------- end datatype attributes
 
-class NodeManager;
+class DTypeConstructor;
 
 /**
  * The Node-level representation of an inductive datatype, which currently

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 0c209f3934be77e127520b6c4e56384e76dd91f5..8d8d2741f5ba9fd6a07425ee1de4788938d6219f 100644 (file)
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -15,6 +15,7 @@
 #include "expr/lazy_proof.h"
 
 #include "expr/proof_ensure_closed.h"
+#include "expr/proof_node_manager.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index e2bba30158ba69b2a504c12d1f6ef2693c05ed2f..83dc90e4d90ce4f21dc837be60727f4db827ce57 100644 (file)
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -22,10 +22,11 @@
 
 #include "expr/proof.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) lazy proof. This class is an extension of CDProof
  * that additionally maps facts to proof generators in a context-dependent

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 2edad1647778b3956ad1b10d52a8d357d225814d..f80ab099c91b49bd87e5a677a3ad117b7114d639 100644 (file)
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -17,6 +17,7 @@
 #include "expr/proof.h"
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/proof_options.h"
 
 namespace CVC4 {

diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 59cab72c98dbe7da591d76c52d074a6c39ec4b0e..1604bf18223bac2307687371352d8cef9e5a716a 100644 (file)
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -22,10 +22,11 @@
 
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) lazy generator for proof chains. This class is an
  * extension of ProofGenerator that additionally that maps facts to proof

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index c4529562275eeba0c09fa23972dc105c8054585d..1aca73d2eab83ea944873a5ebf63a74353a6037e 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -21,6 +21,7 @@
 #include "base/exception.h"
 #include "base/output.h"
 #include "expr/attribute.h"
+#include "expr/type_checker.h"
 
 using namespace std;
 

diff --git a/src/expr/node.h b/src/expr/node.h
index 559ce5ddbb858eb3a50104642d6c4ab56f11ebd4..06c327018f6fe04b973db391ceb93735c7fcc472 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -22,8 +22,6 @@
 #ifndef CVC4__NODE_H
 #define CVC4__NODE_H
 
-#include <algorithm>
-#include <functional>
 #include <iostream>
 #include <string>
 #include <unordered_map>
@@ -32,14 +30,12 @@
 #include <vector>
 
 #include "base/check.h"
-#include "base/configuration.h"
 #include "base/exception.h"
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
-#include "expr/type.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "util/hash.h"
@@ -980,7 +976,6 @@ std::ostream& operator<<(
 
 //#include "expr/attribute.h"
 #include "expr/node_manager.h"
-#include "expr/type_checker.h"
 
 namespace CVC4 {
 

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 883febd6f03a094adece3fe6a45cdbe3a7061f4c..4404e3445f7e9960eeff5286e2af00f8a02aa262 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -26,6 +26,7 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/skolem_manager.h"
 #include "expr/type_checker.h"

diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp
index 75a11eac713107b479fb1c622dd3e76dc037c930..0b778ebef7430fe49c514dbfcbbe3ede19c928b1 100644 (file)
--- a/src/expr/node_traversal.cpp
+++ b/src/expr/node_traversal.cpp
@@ -14,6 +14,8 @@
 
 #include "node_traversal.h"
 
+#include <functional>
+
 namespace CVC4 {
 
 NodeDfsIterator::NodeDfsIterator(TNode n,

diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index e7e49db45556da276d75949d6cb47c7fef73664e..124372f790e5a262e84919b400538953ce9c78e9 100644 (file)
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__EXPR__NODE_TRAVERSAL_H
 #define CVC4__EXPR__NODE_TRAVERSAL_H
 
-#include <functional>
 #include <iterator>
 #include <unordered_map>
 #include <vector>

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 0635e983b200e837a8e0fbd03f45cda7e1f01a0f..1ad498ecd0454be7b975a85d0472cb1d040ba319 100644 (file)
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -399,7 +399,6 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
 }/* CVC4 namespace */
 
 #include "expr/node_manager.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {
@@ -501,7 +500,6 @@ inline NodeValue* NodeValue::getChild(int i) const {
 }/* CVC4 namespace */
 
 #include "expr/node.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace expr {

diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 1c21a59e7681023000b908000d9107399b60dba4..b512b586953250efa31dfc66a519b0fb45bea336 100644 (file)
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof.h"
 
+#include "expr/proof_node_manager.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {

diff --git a/src/expr/proof.h b/src/expr/proof.h
index 8350b49544bad53df83931d95f4aa34ec4de9525..3a26f097532a088b7e3d47e0818838c3faea92a7 100644 (file)
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -24,11 +24,12 @@
 #include "expr/node.h"
 #include "expr/proof_generator.h"
 #include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * A (context-dependent) proof.
  *

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 840cb4c6601a483fb7bae9938afb423dd1b8004b..ea73b7958aa6c0d3e1053f1e822877cec1ee2475 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
 

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 707d1314c4e73ed6538a250a4c1763628d72cc6e..7e6371aa975641a6746d324bc116ffefda4f95d1 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -17,6 +17,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 
 #include "expr/node_algorithm.h"
+#include "smt/logic_request.h"
 
 namespace CVC4 {
 namespace preprocessing {

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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c7962417a3dd310ecbf101dbd894e71ea867d45b..fd9d20e4bcbe71a0e7d29e833da4bcf9f91c799a 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -17,12 +17,14 @@
 #include "printer/smt2/smt2_printer.h"
 
 #include <iostream>
+#include <list>
 #include <string>
 #include <typeinfo>
 #include <vector>
 
 #include "api/cvc4cpp.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/node_visitor.h"
 #include "expr/sequence.h"

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index ac90d0c367008c428f1ebadc7b3add79feb7ae56..d0c75a924ace73c424d5324757aaaf3209e0b633 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -33,6 +33,7 @@
 #include "prop/prop_proof_manager.h"
 #include "prop/sat_solver_types.h"
 #include "theory/trust_node.h"
+#include "theory/theory_inference_manager.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cdaaa05582c1dabe1f0ece47a3b6471bfcd5500d..f10191c7521c981154723c899b575e80d38479d0 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -39,6 +39,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "util/sexpr.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
 using namespace std;

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index b1fb0589c328e7bf47a67b628c8b0a3daa473407..aedd946c153b4110ebe302e011d427f24be3c769 100644 (file)
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -16,6 +16,7 @@
 
 #include "smt/dump.h"
 
+#include "base/configuration.h"
 #include "base/output.h"
 #include "lib/strtok_r.h"
 #include "preprocessing/preprocessing_pass_registry.h"

diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 0347a24efbd83ed89b13b06e294ffe8c01364954..f0fad93fefc7c1453632babb02310a8d832baf39 100644 (file)
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/listeners.h"
 
+#include "base/configuration.h"
 #include "expr/attribute.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"

diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 3210de7b168145d2a00893bb86dbc6443d86058a..4e8dcce6c8cc4856a3af728cd82fcdf6984818b1 100644 (file)
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -26,7 +26,7 @@
 #ifndef CVC4__LOGIC_REQUEST_H
 #define CVC4__LOGIC_REQUEST_H
 
-#include "expr/kind.h"
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 98fbfe1b3009b8b154109e1580b28aee0c6ec637..3d306a7a209feb5d4830fcf75bae64365886d32a 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -35,6 +35,7 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory.h"
 
 using namespace CVC4::theory;

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 941fd111a4a68c5dceb204cf649be805b0d897b6..ed5e73d5d81ba1551b6ceae3dc06e8fcbe6e3946 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -42,7 +42,6 @@
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
-#include "smt/logic_request.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
 #include "smt/node_command.h"

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index eb8eb6ca011bb20daa8e79f083d3f9a615ef3aef..53a5b7f2f78b25585d97286bb2d2f9012e374b76 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -23,20 +23,15 @@
 #include <vector>
 #include <map>
 
-#include "base/modal_exception.h"
 #include "context/cdhashmap_forward.h"
-#include "context/cdhashset_forward.h"
 #include "context/cdlist_forward.h"
 #include "options/options.h"
-#include "smt/logic_exception.h"
 #include "smt/output_manager.h"
 #include "smt/smt_mode.h"
 #include "theory/logic_info.h"
-#include "util/hash.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/statistics.h"
-#include "util/unsafe_interrupt_exception.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -51,7 +46,6 @@ class TypeNode;
 struct NodeHashFunction;
 
 class NodeManager;
-class DecisionEngine;
 class TheoryEngine;
 class ProofManager;
 class UnsatCore;

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 31eb8bb8f1227dd508c17c724088da1372e23966..26f51c8b87b6581f6124be3c85016697b9bd55ee 100644 (file)
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/arith/arith_preprocess.h"
 
+#include "theory/arith/inference_manager.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 6c858d1ebc6c8e0984fd6e8a4e45728170612c45..396395e1f034c358b19991453e41731f68b27305 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -21,7 +21,6 @@
 #define CVC4__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/arith/rewrites.h"
-#include "theory/theory.h"
 #include "theory/theory_rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 72f8e49fffca8944acb53b9c1bc9fcdfc0245f5e..61715df9b2f783d60dbbc742c6a5960fb28f70d5 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 
 using namespace std;
 

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 374b17d887b7f1969deeb384c9d17e248dbe4faa..5d4bc9b1ef3cb3c58e99161c11b1b2ea25ad06b4 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 
 
 using namespace std;

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 85af862fad47c38e9f0eb8368934b4c2b0eaec5a..8cb249c46c752a4e964a0c7ca00660bb9ad0845d 100644 (file)
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "util/statistics_registry.h"
 
 using namespace std;

diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 1bd4416e03f22de965871d67fcd58b1247660295..e001d98d4e9ee9ea5e4b4b8082b43823757d8b87 100644 (file)
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -52,6 +52,7 @@
 
 #pragma once
 
+#include "theory/arith/error_set.h"
 #include "theory/arith/simplex.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index df3ba37f3077aa9ba618233335991fdea4bbc746..04165c2897e3df68c9877168a7f13990459cdf21 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "theory/arith/nl/cad/projections.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
+#include "theory/arith/nl/nl_model.h"
 
 namespace std {
 /** Generic streaming operator for std::vector. */

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 4511d0c55e88d02e999a03ba23bf00564f949955..8736b7a086078fee4fd39701348c06dc6458bfa6 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -32,12 +32,14 @@
 #include "theory/arith/nl/cad/constraints.h"
 #include "theory/arith/nl/cad/proof_generator.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
+
+class NlModel;
+
 namespace cad {
 
 /**

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 74c0457a85fe9ae4a80af26dc8b7c30074874538..efc5c465af8e4f157402f48165fdccfaef0c89bf 100644 (file)
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -14,15 +14,11 @@
 
 #include "theory/arith/nl/cad_solver.h"
 
-#ifdef CVC4_POLY_IMP
-#include <poly/polyxx.h>
-#endif
-
-#include "options/arith_options.h"
 #include "theory/inference_id.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/poly_conversion.h"
-#include "util/poly_util.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 21fbbab2e7489d37e46340aa1390642c3b509b48..b67d78f0d0c863ab5bee3bed9378e3ab283db4a0 100644 (file)
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -17,17 +17,22 @@
 
 #include <vector>
 
+#include "context/context.h"
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/cad/proof_checker.h"
-#include "theory/arith/nl/nl_model.h"
+#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 /**
  * A solver for nonlinear arithmetic that implements the CAD-based method
  * described in https://arxiv.org/pdf/2003.05633.pdf.

diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 5da5319a1e91df7897dc1a2d33c683b08e0b8e26..7e77efb16bd5dd64f2c476222af7fcbbf4254b37 100644 (file)
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -17,6 +17,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_model.h"

diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 863b3f87917381bc3577bc2aa07fb461bc7c07d8..285189cccf29fdd71345c8613745de001baae234 100644 (file)
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -19,15 +19,21 @@
 
 #include "expr/node.h"
 #include "expr/proof_set.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
+
+class CDProof;
+
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 struct ExtState
 {
   ExtState(InferenceManager& im,

diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 7b4d98037b9efe8c96ea0de5503d9ec074f690f1..09cfd74103c994ac824b03069fa0572ccb972439 100644 (file)
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -15,10 +15,12 @@
 #include "theory/arith/nl/ext/factoring_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "expr/skolem_manager.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 5ae898bd221ff31ef7ee8b71cf7eed9a35eec1f2..ad6fd36b84a01e6b547406ac827962867ab5f425 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -15,11 +15,13 @@
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index a3e56358b29af823f5ffb2d07d8e07db6d16bb54..d970bd95d2acdd012ff2d969c6fa22655298c63f 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/ext/monomial_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"

diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index 51179826a3befbd97e483da46f95cf43b3708d01..05908ecc762bc37e8eb918881cddbd2920fee710 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -16,6 +16,7 @@
 #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
+#include "theory/theory_inference.h"
 #include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 1e9b444e32f47c64fe0cdfcbee3ad4e2b3a8ff9d..5bcdb801dc99924a33208806bdd0c8f799140840 100644 (file)
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -15,9 +15,11 @@
 #include "theory/arith/nl/ext/split_zero_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index e8730e496dd941300f36233d475d65fe92654b87..0e7ad09998b5c48c8c2ce27adb31be10ca3e058c 100644 (file)
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -16,6 +16,7 @@
 #define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
 
 #include "expr/node.h"
+#include "context/cdhashset.h"
 #include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 3d646a684084f64b58bf7e778742f088aaf278d6..2d04c2b5ca3dd0372370bc8f5db724ad538c2e96 100644 (file)
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -15,9 +15,11 @@
 #include "theory/arith/nl/ext/tangent_plane_check.h"
 
 #include "expr/node.h"
+#include "expr/proof.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp
index 62e1fa904e8299e6068d3eae736d662b6ea8caa1..ee12d17d6f7b978513ea3aeb32d5e108208578a8 100644 (file)
--- a/src/theory/arith/nl/ext_theory_callback.cpp
+++ b/src/theory/arith/nl/ext_theory_callback.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/ext_theory_callback.h"
 
 #include "theory/arith/arith_utilities.h"
+#include "theory/uf/equality_engine.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index a5b4e87bda5ae27c12cba2f84dac10d1e3f29b00..6487b48eccea8e0913a5c815a6e140e4cd7042e0 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -18,7 +18,10 @@
 #include "options/smt_options.h"
 #include "preprocessing/passes/bv_to_int.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
 #include "util/iand.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index c854f3ab7f7424542cd575d3b893088b33bb31c8..044a37abcfb046f83308efc21960dd1ae9210f97 100644 (file)
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -20,17 +20,20 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/iand_utils.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class ArithState;
+class InferenceManager;
+
 namespace nl {
 
+class NlModel;
+
 /** Integer and solver class
  *
  */

diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 17eb518a2f137a9781fa2996fa498036dd05e8ff..652f0eec72bac84aa6e53ae10d3add8d24bed6c4 100644 (file)
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -19,6 +19,8 @@
 
 #include "cvc4_private.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {

diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index a05defc0a93f8141d30472caa174c8dddf10d02b..4c1de019629810a85c3e9e9443b22d9cdebac974 100644 (file)
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -16,7 +16,7 @@
 #ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
 #define CVC4__THEORY__ARITH__IAND_TABLE_H
 
-#include <tuple>
+#include <map>
 #include <vector>
 
 #include "expr/node.h"

diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index af86d69fd9a4f3d72280af9dc8c980c653c13cf4..7d698a221d96e196cffc11c24b990b34dc0dc864 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/output.h"
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/poly_conversion.h"
 #include "theory/arith/normal_form.h"
 #include "theory/rewriter.h"

diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 176549d8b92c1b281f80385865d3692bbb774a8e..b9ecfc437cbf201654185f77672c2c21aace4f4e 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -23,7 +23,6 @@
 
 #include "expr/node.h"
 #include "theory/arith/bound_inference.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/icp/candidate.h"
 #include "theory/arith/nl/icp/contraction_origins.h"
 #include "theory/arith/nl/icp/intersection.h"
@@ -32,6 +31,9 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 namespace icp {
 

diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp
index aa8fcf543bb8760036c05cadb6f722a0f4640e27..b5fedb7ebc099dc9af258af83eef92e96ab0c07f 100644 (file)
--- a/src/theory/arith/nl/icp/intersection.cpp
+++ b/src/theory/arith/nl/icp/intersection.cpp
@@ -18,6 +18,8 @@
 
 #include <iostream>
 
+#include <poly/polyxx.h>
+
 #include "base/check.h"
 #include "base/output.h"
 #include "theory/arith/nl/poly_conversion.h"

diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index 0df6caf34b0fb00456cbabc72e31fffb0946e2eb..cdc166139c3c20bb19a748eeb8ded7d8f7893cc1 100644 (file)
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -18,7 +18,9 @@
 #include "util/real_algebraic_number.h"
 
 #ifdef CVC4_POLY_IMP
-#include <poly/polyxx.h>
+namespace poly {
+  class Interval;
+}
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 5c4140430bf856755d95d8ff4177c4868f6b8bee..9255d3349b475dfd89361839583aa7a7c5f30468 100644 (file)
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -20,6 +20,7 @@
 #include "options/theory_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/theory_model.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index cd2d15563d8cb7db5a189ca84cd40d34ab69a670..4d55855457347e3bb2fa9ce52b707cf7fd1abbf4 100644 (file)
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -19,15 +19,20 @@
 #include <unordered_map>
 #include <vector>
 
-#include "context/cdo.h"
-#include "context/context.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
+
+namespace context {
+class Context;
+}
+
 namespace theory {
+
+class TheoryModel;
+
 namespace arith {
 namespace nl {
 

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index c46781e76ef1fed6f94f6ed651260efd2d94619a..f269f1d69ac5ca23b62f5ba8dd74098bb26b716a 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -18,10 +18,10 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 
 #include "options/arith_options.h"
-#include "options/theory_options.h"
 #include "theory/arith/arith_state.h"
-#include "theory/arith/arith_utilities.h"
 #include "theory/arith/bound_inference.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
 #include "theory/theory_model.h"

diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index fba9e8e87aef4acfc11ce514405eb7980cacfb90..6a38021a0fecbd22005996113392924c3b5af310 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -21,10 +21,7 @@
 #include <map>
 #include <vector>
 
-#include "context/cdlist.h"
-#include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad_solver.h"
 #include "theory/arith/nl/ext/factoring_check.h"
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
@@ -35,19 +32,25 @@
 #include "theory/arith/nl/ext_theory_callback.h"
 #include "theory/arith/nl/iand_solver.h"
 #include "theory/arith/nl/icp/icp_solver.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/stats.h"
 #include "theory/arith/nl/strategy.h"
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
 #include "theory/ext_theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
+namespace eq {
+  class EqualityEngine;
+}
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
 
+class NlLemma;
+
 /** Non-linear extension class
  *
  * This class implements model-based refinement schemes

diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 5b7edb3ef1ac08d44a6ff897fdd0e5278072a3f6..67cfd58071a9657108f8f475695d4fa6456c9b1e 100644 (file)
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -20,9 +20,8 @@
 
 #include "expr/node.h"
 #include "expr/node_manager_attributes.h"
-#include "util/integer.h"
+#include "theory/arith/bound_inference.h"
 #include "util/poly_util.h"
-#include "util/rational.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 37d816179897c98bd7cf5c7099ffd495faa891a6..102d2d6aed4e9453eb74bfb1ac51dac52dcc183a 100644 (file)
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -23,15 +23,18 @@
 
 #include <poly/polyxx.h>
 
-#include <iostream>
+#include <cstddef>
+#include <map>
+#include <utility>
 
 #include "expr/node.h"
-#include "theory/arith/bound_inference.h"
-#include "util/real_algebraic_number.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class BoundInference;
+
 namespace nl {
 
 /** Bijective mapping between CVC4 variables and poly variables. */

diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index f869d83a43c95150211ad04229ef783326dfdd76..fab4de35ae153b3951ce3d891ced5dee2096085c 100644 (file)
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -17,8 +17,6 @@
 #ifndef CVC4__THEORY__ARITH__NL__STATS_H
 #define CVC4__THEORY__ARITH__NL__STATS_H
 
-#include "expr/kind.h"
-#include "theory/inference_id.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index 526ae36f12ccbb3f5c3a1236034132748fb751fd..1f7b85b606c5dedcbbc9f13b2b40621d61567b60 100644 (file)
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -16,7 +16,6 @@
 #define CVC4__THEORY__ARITH__NL__STRATEGY_H
 
 #include <iosfwd>
-#include <map>
 #include <vector>
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 86b17376cbf1a2d0c5a72f79251d2b54e1a62058..74766926b8b1e503d08b4a16530f336827b4aeb5 100644 (file)
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -19,9 +19,11 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index b874e1a4b10c20204893e4c0e326bab791b4518b..ddef4faf72d3a490f632d26e6c6c43742e68a550 100644 (file)
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -21,8 +21,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index f5dc49da804e27d813ec1b015dadf818e88f2259..11852ac3abd37017727cae87d8f58ed20ba213f2 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -19,6 +19,7 @@
 
 #include "expr/node_algorithm.h"
 #include "expr/node_builder.h"
+#include "expr/proof.h"
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"

diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index da4b48fd6a162f7167f0ca34c90d43667200f96c..a009df09b3531bc5af8bee97351fba3dc303ac98 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -21,8 +21,6 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index 375f1757e84f03d202e78ccaaa40f1ed978e26dc..f45b906bca6904d70ab4ee03fd2c56630258986c 100644 (file)
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index ccdc80e0f9abd7c175bff440b8fdbf3734afa520..0e1248f7c7334953d6e07e90ab0ba20218ba547f 100644 (file)
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -16,12 +16,14 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
 
 #include "expr/node.h"
-#include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 class TaylorGenerator

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index e58da1aad43704c2babe348ab3a136853a6eeb68..d1355c746014cc7f66cfd353ec624deff2a79432 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index 8135ba1fb5e834038e28fec9b8ed7dbf97e6efb4..343f303d1d3afdf0de1cc1ab4c80ff94442c0ca8 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -9,37 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-/*********************                                                        */
-/*! \file transcendental_solver.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
  ** \brief Solving for handling transcendental functions.
  **/
 
 #ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
 
-#include <map>
-#include <unordered_map>
-#include <unordered_set>
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/exponential_solver.h"
 #include "theory/arith/nl/transcendental/sine_solver.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
@@ -47,7 +25,13 @@
 namespace CVC4 {
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 /** Transcendental solver class

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 76c3d5357078649a7ed9eb35e57b00eddb2bbad1..ae8c1eea7742038bd745503806bb1b802a25c194 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -14,8 +14,10 @@
 
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
+#include "expr/proof.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 93ac4627a3844e59a4848ceed933667ac694f6f8..d0678fb9a2ca6dbc608de88ec1ba39dd899349fe 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -23,6 +23,7 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
 namespace CVC4 {
+class CDProof;
 namespace theory {
 namespace arith {
 namespace nl {

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 5c1b90663d4d6e939855ef2ba7ed3bf17cb201d1..d0a7f7fc44c50237276371e7bc2638ddced3def1 100644 (file)
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -19,6 +19,7 @@
 #include "base/output.h"
 #include "options/arith_options.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "theory/arith/simplex.h"
 
 

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 6740c8e1c13223f0b38431fe27ae58a4b1de9fc7..e34696cb579b5775265f8389ff26c9cdbfebc430 100644 (file)
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -57,7 +57,6 @@
 
 #include "theory/arith/arithvar.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/arith/error_set.h"
 #include "theory/arith/linear_equality.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
@@ -68,6 +67,8 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class ErrorSet;
+
 class SimplexDecisionProcedure {
 protected:
   typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec;

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 18169474d7901d7ea06ff2738c12dd1867b35d2b..796cd941234b41791c810731ca4fff3693af3c89 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -22,6 +22,7 @@
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/error_set.h"
 #include "util/statistics_registry.h"
 
 using namespace std;

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index eba84e339410cd922f12a48f32a9de92329201ca..f3344cbda205e42a21faded614782a43f73786de 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,13 +22,15 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
+namespace nl {
+class NonlinearExtension;
+}
 
 class TheoryArithPrivate;
 

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 3b5f0dd822f425613f6a7e743fd413ff545f3194..40bd81795113fdcb872d1187f99709fe640c1619 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -65,6 +65,7 @@
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/dense_map.h"
 #include "util/integer.h"

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 56e8fa4b0884f222c4ec7e8b06a51f0011755f70..818393cc7a5c95e9cfd0cb50a81b537a9e4ae877 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -43,6 +43,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/dio_solver.h"
 #include "theory/arith/dual_simplex.h"
+#include "theory/arith/error_set.h"
 #include "theory/arith/fc_simplex.h"
 #include "theory/arith/infer_bounds.h"
 #include "theory/arith/linear_equality.h"

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index 96f2b02c39ec6d45c35218c80715df35e31c8f24..b5bb9be14b2f7cf741bb977b200134020593e842 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "options/smt_options.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4dd7dcafd195fed5e5275da8f106504c31efe6b0..49f530e3262916040ba364d972d7bc2e4dc6b476 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -28,8 +28,10 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arrays/skolem_cache.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/decision_manager.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 
 using namespace std;

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7e4f0e36cb236821b85d7aa912df717043188068..e02c3029615553c5e7ff54e8580d1f0d387d002a 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -29,7 +29,9 @@
 #include "theory/arrays/inference_manager.h"
 #include "theory/arrays/proof_checker.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/decision_strategy.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_equality_engine.h"
 #include "util/statistics_registry.h"

diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 76c001ba299ae6146a0e4e8c71807f1629f6bac5..c39e0198bd63580305993a4a9f126ec5f7c3fc92 100644 (file)
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -17,6 +17,7 @@
 #include "theory/bags/bag_solver.h"
 
 #include "theory/bags/inference_generator.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace std;
 using namespace CVC4::context;

diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 48cd9c419b6f2172cb50dd1d83523dc7288e2a89..d9f736c4f0c3dd8644dd1e4182e712c1c12c296a 100644 (file)
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -19,6 +19,7 @@
 
 #include "theory/bags/rewrites.h"
 #include "theory/rewriter.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 726160d838f14bb3b56cb0b4d9b327551760982b..f00bffb2edad06c56faec8a038287e71eca71776 100644 (file)
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -21,6 +21,7 @@
 #include <vector>
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "theory/booleans/proof_circuit_propagator.h"
 #include "util/utility.h"
 

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 90de1d8dac53b04c3b8bc97cff6fb97d9a0ce35b..b5ad16b1c92538639d1f07eaae209d710d154f85 100644 (file)
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -25,6 +25,7 @@
 #include "theory/booleans/theory_bool_rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory.h"
+#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/hash.h"
 

diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 551c186124d13ea955e16fa5e51bab52ef912818..4c731194595ee8e2495cfcb370d009f49dd0bafa 100644 (file)
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -15,6 +15,7 @@
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 38e4b3aa6451731a49e09364dd1b7140418118a4..d9adf06fbb30b3ed2d5355066d5447e9d3d895d0 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -24,6 +24,7 @@
 #include <unordered_map>
 #include <unordered_set>
 
+#include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
 #include "theory/theory.h"

diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index d8d8dbed7f7467a33c1cf2f9b11a422235d167b4..3cadac62155d0e6f9b84a2d384c86617aaf84604 100644 (file)
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -30,6 +30,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::theory::bv::utils;
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 55a0ff46b54fb5a4cc63a5b13f2c2f02cd0ef6da..47974fc038839352eb07eb79c4a487210f7c9868 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/bv_solver_simple.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/ee_setup_info.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 2aa722e48f025bb561a01587e624430b633ee516..fafde0601d91cd8145a1c52430d052679101e905 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -24,6 +24,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h
index 40553f01b1bd52146be83497798b67687ea22c56..6793d6e90178edf3e0de7dac93fd5a391f4aad98 100644 (file)
--- a/src/theory/care_graph.h
+++ b/src/theory/care_graph.h
@@ -21,8 +21,8 @@
 
 #include <set>
 
-#include "expr/kind.h"  // For TheoryId.
 #include "expr/node.h"
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 4dbf26062120d30f0e3fef8dc8ab05be888aa444..5334e76dfeead155c9bbaedfc397b80e5e51cdbd 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "options/datatypes_options.h"

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 14dc9fbf1b82e38f0833f39b64f08ccc1b983a8f..ea5928a42224822d2636cf0b7118b595afafc974 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/infer_proof_cons.h"
 
+#include "expr/proof.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index 9702a558464dc7a029578f151e62e71fb4890f73..4c7773e29b89ff029b4abb084c1f12ef297bde04 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -17,7 +17,11 @@
 #include "expr/dtype.h"
 #include "options/datatypes_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index ba46d2a423a4b23acf4f66afb1d9adbf03f76f99..610383ff1d532e4a34486a5f9487861714c91233 100644 (file)
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -25,6 +25,9 @@
 
 namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace datatypes {
 
 /**

diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 6bfa2015169b0fb5c9434414123a75e96df51525..9a9f7cb7bfcceed0a8cca4e9e72b8988556d6f24 100644 (file)
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/proof_checker.h"
 
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 60bf36139ce3f845dda961d3007ed31298fd5961..6169d375250ce79601fe8a7c6614b1af47d0befb 100644 (file)
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/sygus_datatype_utils.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"
 #include "smt/smt_engine.h"

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 7efd2a9ac93d309117c92232689a4adb2bd01f24..8622ec483c387ccb070a42d7fb9d8d0866673003 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -15,6 +15,7 @@
 #include "theory/datatypes/sygus_extension.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_manager.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"

diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp
index b7ab9b4f7fc959e8e4a4c0a428c84319778e3fbf..a2530f4ace1f16b609e158dd882831414b2474a1 100644 (file)
--- a/src/theory/datatypes/sygus_simple_sym.cpp
+++ b/src/theory/datatypes/sygus_simple_sym.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/datatypes/sygus_simple_sym.h"
 
+#include "expr/dtype_cons.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 45787ee04c34ffc9b4dcef82f74ea3ab287927a5..9105cdfd6c1dd1b106034b84ee768a0c7d07f576 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -19,7 +19,9 @@
 
 #include "base/check.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/kind.h"
+#include "expr/proof_node_manager.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 2834b86ba730a5275fed94cf9ef13d484532afbc..73aef4dd79819b6b9105a8b60103f2e17acedca0 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/type_matcher.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 

diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index c55b4a14f3b91695d76bb3f56bb7e3330ab18360..1247ecca5885eeab9e6faf42c8e95ffc71b88c14 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;

diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 07943034248272b5e5a5c712f3b90256c2dfd336..25bdd2f94579038adbe747b8d3286624e77a3070 100644 (file)
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -14,6 +14,7 @@
  ** Enumerators for datatypes.
  **/
 
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/type_enumerator.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_utils.h"

diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 7b4936a536c047f70ae390ac1342018d48ad83c7..030d9a497198cbcfa5880381b9f82046853e4af1 100644 (file)
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -20,7 +20,9 @@
 
 #include "base/check.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/substitutions.h"
 
 using namespace std;

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 6df991ef932017a4f2c97060ab6a9cfcac91863a..e9b59fdae667953f47349d90776abab17e80b33a 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -22,9 +22,12 @@
 #include <unordered_set>
 #include <vector>
 
+#include "base/configuration.h"
 #include "options/fp_options.h"
+#include "smt/logic_exception.h"
 #include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
+#include "theory/output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 

diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 1a745b3a33e6b687fbac943decd6f5eb957730fe..bd6e70ff11c1ac141a48a854c20f70d8697603d6 100644 (file)
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -23,9 +23,11 @@
 #include <string>
 #include <utility>
 
+#include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {

diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp
index 0c143f265fbcbe7ae560de9f46a865f52bb5cadd..3e4b921dbebb3084fdc00b963ffe5556883adbba 100644 (file)
--- a/src/theory/inference_manager_buffered.cpp
+++ b/src/theory/inference_manager_buffered.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index bb2bf937aa14131449eaa2f94a4d1c60e68c0c11..24570f9a656af30e18f48516c8bbd01a07d7da90 100644 (file)
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -18,6 +18,7 @@
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {

diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 16f0f39579de10e44235459b6c048ad4ec133799..7a584c14677ef53e885414b507aa754c45ea35d9 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 0d1a51a306261703f52b068e2ad666abca50eabb..bda4e31fc6224f265de2ac4f24c9ec5384d06017 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -18,6 +18,8 @@
 #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h"
 #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h"
 
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index e782a1b6f37c3ab252b2d501f43d9aec53b91fed..0c416fdf413b53b490fcc59fbe9b8b9f89d18225 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -17,6 +17,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index eb02eb19e2d1fb35ff0264d163e344087f0dfe77..c553a123907856e4388fc2087c0b2ced6d5aa382 100644 (file)
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -14,11 +14,13 @@
 
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 5df350fe5aacd1b1b35b6524bb6301b3078ba2cc..1875dc631284093afa1a736b1d126fcd0931b6a6 100644 (file)
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -16,7 +16,10 @@
 
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"

diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index ce535d5e89d81dbb803d512dab42c535888510fb..07cb74a839b3a5f92ec547ffaca354602e27a49e 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"

diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 5c5dcfef195af54b676e1519f4c14a3ff9e39599..dfe2e3ae996ed143d315e1a95c622fd423635c87 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -15,7 +15,9 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi.h"
 
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index 66433ba7835b96c03fe14986c1a6e38465ca7822..00a233d6abffb4abb0b7a1760562fda368a9fd1e 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -14,6 +14,8 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 6b2f1b7f83e9aab2502b72b8c47f9b005dce839b..f9692bd760e45d6aca9e71e580f8a327d4bfa410 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -14,6 +14,11 @@
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 
 #include "theory/quantifiers/ematching/trigger_term_info.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index e7635f2006a553f1dc632c6a45506cb239d47dae..9768e7f2c932a3e575c49c91ff2354eb1065643a 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
 #include "theory/quantifiers/quant_relevance.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 #include "util/random.h"
 

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index 14913bdc1653d0c49a9f907661989a9b0198eed5..c2b5f78ae026f69b14b392ebdd4c2efa373758bf 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index a64dc4424af81d1bb2c89cce9a9d556c266c027e..6564f407e4d6d8cdf836c14fb896e5caf1b4bea0 100644 (file)
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 79bd5c1ddc1bdec51b471085232292fd442833b2..9d8b64e257bc5bdd7a4ccc0eedee75faf80ec677 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -22,10 +22,12 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index 8448fe8102391c85cd8dbef303cf6d8ee939ec57..17baf50005364e3a4f290a4376ee9ac5f27a0242 100644 (file)
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -13,7 +13,9 @@
  **/
 #include "theory/quantifiers/ematching/var_match_generator.h"
 
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 759d3e69f3318fb6e8fe6d160e678a8601f6107b..6ce561b2dc922c0587ec1afd8249549407a1e986 100644 (file)
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 700ae2c6497bb61cb77c2be36efd08e48dd24e66..fb0505bae4f9ce7ddf089ee2206683e9e135edad 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -16,10 +16,12 @@
 
 #include "theory/quantifiers/fmf/bounded_integers.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/term_enumeration.h"

diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index 9d4a414e980a83087f62d408e8d3fad6af0d4870..3e7466ed2e5aefdfdc61538e73e885db1e24bd16 100644 (file)
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -23,6 +23,7 @@
 #include "context/cdhashmap.h"
 #include "context/context.h"
 #include "expr/attribute.h"
+#include "theory/decision_strategy.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 96e8a40bedeb94cfa4e938e3bf4ec0cc8ff3bfdd..c248167cb7afb38d69edfe15cd63a393ab974320 100644 (file)
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/inst_match.h"
 
 #include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 

diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 993fad90a72063833a5189ea5de051734f554f38..ab5dcb16662faf91dc65ec86fa04c76d7a64176a 100644 (file)
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 using namespace CVC4::context;
 

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 2eb99a7743ac3e909d184dab25c9e02760fcfb01..3164ff5ce9b446db39fea97a5d8c51860754d8eb 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/instantiate.h"
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index a0b776819c4c1e5309accdd34ee9f54b0dd49250..37cc49f172061dca8c7e73b7a780569c49a20435 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -19,6 +19,8 @@
 
 #include <map>
 
+#include "context/cdhashset.h"
+#include "expr/lazy_proof.h"
 #include "expr/node.h"
 #include "expr/proof.h"
 #include "theory/quantifiers/inst_match_trie.h"

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f89f9f0ea4cc23febbf9d94cfa9aadc9bcfc31bd..cf37bc746469a0038e2b8e5a473c9cf387bd3800 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/quant_conflict_find.h"
 
+#include "base/configuration.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "options/theory_options.h"

diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp
index 5bb50c926d643a232d2db0300d8cf2e686232e9a..58716f80998b40703c0a2d909507beaa0ce05027 100644 (file)
--- a/src/theory/quantifiers/quant_rep_bound_ext.cpp
+++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/quant_rep_bound_ext.h"
 
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index a0b7808363c5e66a7f72a41eaf34f59616da7973..e3bd2072f7055065ae5d92e27b5ecee4e9906d91 100644 (file)
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -13,6 +13,9 @@
  **/
 
 #include "theory/quantifiers/quant_split.h"
+
+#include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/first_order_model.h"

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2126bf1f0e14c7c43d106b42a53fb24ebac33fe4..ec7e7fd2c54bfae5cbc28499fe422458ba19d642 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/arith/arith_msum.h"
@@ -27,6 +28,7 @@
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 
 using namespace std;

diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 0bcca266e1928b3abbdd71bab2d058c5f2f3e14d..55f680897d6c5fa95769e259c33876e1dee075bc 100644 (file)
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/quantifiers_state.h"
 
 #include "options/quantifiers_options.h"
+#include "theory/uf/equality_engine_iterator.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 3cef2884fa7d10f688a7c1e9567acb18e66bbcd5..b97a8e539fd37aac3a6373d5eae02e57268090bf 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index a9ac7d0d253822271668eb01b1b4c3d8f7467375..42729ef5b636121eba2be1b48409a91965245b34 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/skolemize.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index b296a442131ea335e7ebddcb44f99f373abd4e40..77714f87d53f9624418114f3771b44e600cbb5ef 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "smt/command.h"

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index db2a972d58c8f3c30a34248f7aa6c2c3308f58a6..a58ce894deda974538e090bef024b20c8b6aa515 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/cegis_core_connective.h"
 
+#include "expr/dtype_cons.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
 #include "proof/unsat_core.h"

diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 9db77fd95a93936028dc699cabf4d26239667cb6..5da6f212125ba48b1b04fad1025a7bdc6b3bcc08 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -19,6 +19,7 @@
 #include <map>
 #include <vector>
 
+#include "theory/decision_strategy.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 

diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 360476399fe2af239097dc37e74f1295f9341bbd..f6e34e8a10482da533197eacd887739886829191 100644 (file)
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
 
+#include "expr/dtype_cons.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index e0159049b47096cbde463e48ca36d1113f1fd8d7..2fa6009d3b6fd9b7fc9c454003e61b63778e67f5 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"

diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 882c9ca7703dbda793bc3d5e788fec321d6ac081..90765284aae09b837f2c5d843a7edb6c30ec05bc 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -14,10 +14,12 @@
 
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 0f9d2ccd1e242326eda02a75b1f36b3a40e3a8a2..5965e94305964c2064b41c65e208bdd2ccaa2a8d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_explain.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 538d80e44e5f4ee9a8c1a12acdd2e36d14a30d3d..98a177f8695256053b3b7455afacd8b0eed18e14 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -16,6 +16,7 @@
 
 #include <stack>
 
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index 7d757ca984c4a82c9f827f91dfa9f1cbcfb98812..953eac7b05a35a5aec2c25b44bbc5f72acd84d6d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 
+#include "expr/dtype_cons.h"
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6e36222b608efbbf856c68267a4be5d54b3bfe9b..cc29e7b0aa72cb842cdb75a2b78a19ecb4df13c7 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"

diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 1e67bb8cc4310725c7a0ac96fad0ecfea76e1aad..a2675dd96cc23da350a11e33e0f15776ed41931d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -19,6 +19,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 81120da28feb697f477e50658cc57cc65f57c1cd..8b741b6d7ec94a59db1c7632a02327ce2f8a8cc8 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
 #include "api/cvc4cpp.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"

diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index f0d3e47b630d6ea562e827ec23f1c747d14bac0f..1c0cfcc5518682161cb3e409c132afb5caee7a7d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -15,12 +15,14 @@
 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_unif.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 0fcba916b876463e3c1c2e1f9f4012ec3e4d256a..56691c7c19df123858ceeaf9d512c198862da401 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -14,6 +14,7 @@
  **/
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
+#include "base/configuration.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index bc5cd1fda2a3c7e4234fc5b51cdf8a33fe3222ae..f393601ad91a9f61d89b64ad77c8b8d5cc5dcd8c 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 #include "base/check.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/datatypes_options.h"
@@ -23,6 +24,8 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"

diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index d44d2eda84b6eb0a6405002fe2647616c1c1e7db..8e29ab9d6bc7df00ed03cf9f93b18f6998cf2646 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -16,6 +16,7 @@
 
 #include "base/check.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/sygus_datatype.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 9fdf0aa7f9a65ec15e1f1284fecf22247a757f35..a46d4e445330d9729d97d09e0f5c119037e60319 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -18,11 +18,14 @@
 #include <unordered_set>
 
 #include "expr/node_algorithm.h"
+#include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {

diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 3116f35e60a96f120fa6b06f707f003f2dd79fb5..17cb1c9a12965685cac42d6e04f790fdb418c396 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -21,6 +21,7 @@
 #include <unordered_set>
 
 #include "context/cdhashset.h"
+#include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_module.h"
 
 namespace CVC4 {

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 62eef124a7846d3f01cf84ce4d48e1fa27ab5e5a..a72054f6d53594ac4bdcf42cff79e752dc10bfd0 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus_sampler.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cb5c7dfec0d510d145e4c5ed9d2a06a24166e290..281d5c844b3fa23fb46ff6e2dc3b014e68af2f88 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -21,6 +21,8 @@
 #include "options/uf_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 9a031f99c94503583a036d4b28ef5fc35e537f03..b121b2c46a16550770e9f44055b40b952a915f44 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -20,6 +20,8 @@
 #include <map>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
+#include "context/cdhashset.h"
 #include "expr/attribute.h"
 #include "expr/node_trie.h"
 #include "theory/quantifiers/quant_util.h"

diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 9cbf2cf5386189d3ea2fb9516f5f6a3b643177b3..33f74c7c4f1af4dc02646655c51799b6cedea954 100644 (file)
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/strings/word.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 036b63b273b012a137f2bbd2816ec76fd9281f58..98bb9bec37e25df06fc52cb3a7db203174716948 100644 (file)
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
 
 #include <map>
-#include <unordered_set>
 
 #include "expr/attribute.h"
 #include "expr/node.h"
@@ -55,8 +54,6 @@ typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute;
 
 namespace quantifiers {
 
-class TermDatabase;
-
 // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
 class TermUtil
 {

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7046a8ef05eee92c1ac28dbf59ecffd94b47892a..79422b41808539974342cb39ab61bcf99c134dbe 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -20,10 +20,22 @@
 #include "options/uf_options.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+#include "theory/quantifiers/equality_query.h"
+#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/full_model_check.h"
+#include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_modules.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/skolemize.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_enumeration.h"
 #include "theory/theory_engine.h"
 #include "theory/uf/equality_engine.h"
 

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f464b24d4e83f9bff23110f5381941c98f6b451c..d08e32f6eb59655f5c3a05046f81b79faade9477 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -20,23 +20,11 @@
 #include <map>
 #include <unordered_map>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
-#include "expr/attribute.h"
-#include "theory/quantifiers/ematching/trigger_trie.h"
-#include "theory/quantifiers/equality_query.h"
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/quantifiers_inference_manager.h"
-#include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/sygus/term_database_sygus.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
-#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers/quantifiers_registry.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -46,9 +34,24 @@ class TheoryEngine;
 namespace theory {
 
 class DecisionManager;
+class QuantifiersModule;
+class RepSetIterator;
 
+namespace inst {
+class TriggerTrie;
+}
 namespace quantifiers {
+class EqualityQueryQuantifiersEngine;
+class FirstOrderModel;
+class Instantiate;
+class QModelBuilder;
+class QuantifiersInferenceManager;
 class QuantifiersModules;
+class QuantifiersState;
+class Skolemize;
+class TermDb;
+class TermDbSygus;
+class TermEnumeration;
 }
 
 // TODO: organize this more/review this, github issue #1163

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index be26510c61a0cc615ac8cb993a8df86c717fc15b..fc98e61987bf6bc58886a21e34da3c65c046218d 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/rewriter.h"
 
+#include "expr/term_conversion_proof_generator.h"
 #include "options/theory_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index 572662483d19aa38280070961802ff31fa1fb181..f5c1348ad802de1839e35dad81a238a48e5df700 100644 (file)
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,20 +19,21 @@
 #pragma once
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
 #include "theory/theory_rewriter.h"
-#include "theory/trust_node.h"
-#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
+
+class TConvProofGenerator;
+class ProofNodeManager;
+
 namespace theory {
 
+class TrustNode;
+
 namespace builtin {
 class BuiltinProofRuleChecker;
 }
 
-class RewriterInitializer;
-
 /**
  * The rewrite environment holds everything that the individual rewrites have
  * access to.

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 2a409a304e4a12dbd29e0df29f8ab70ede105ef6..0a8039ed10437ca548bc46b6ba707c4d2ab20914 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -24,6 +24,7 @@
 #include "options/sep_options.h"
 #include "options/smt_options.h"
 #include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"

diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index b2cd6bf45e98e1fcdb65d7976769a273c2770da5..198273993a97b58d461a4ac02991839a0ad49310 100644 (file)
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -23,9 +23,11 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
+#include "theory/decision_strategy.h"
 #include "theory/inference_manager_buffered.h"
 #include "theory/sep/theory_sep_rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "util/statistics_registry.h"
 

diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 13ee672db885a6442d9f603d163e2d1741122665..0d832b64632b88610198a7d08021291070e87ab9 100644 (file)
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -18,6 +18,7 @@
 #define SRC_THEORY_SETS_RELS_UTILS_H_
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/node.h"
 
 namespace CVC4 {

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index e06a8cb528a717cd91f306a0ab6442c846726e8b..5c6300059bceb201fc5bae1f15955a259740901c 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -20,6 +20,7 @@
 #include "theory/sets/theory_sets_private.h"
 #include "theory/sets/theory_sets_rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 1e4473d6f553c528abb9fcd997d3ea41c78aef19..eb802af4a4b2fa71a8df974e50ababdb60785bbf 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -17,6 +17,7 @@
 #include "theory/sets/theory_sets_rewriter.h"
 
 #include "expr/attribute.h"
+#include "expr/dtype_cons.h"
 #include "options/sets_options.h"
 #include "theory/sets/normal_form.h"
 #include "theory/sets/rels_utils.h"

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 5446f67be7883c5ef9ae9081ee0dc4be7be8d0d5..642a4d4ae14fcdc02c88ec143d0b8a253e9b048e 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/strings/core_solver.h"
 
+#include "base/configuration.h"
 #include "options/strings_options.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/strings_entail.h"

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 770991286d30298e20c609829869d69d97da57a8..620cca185e50809b0640eba5b9d31e5056fb095e 100644 (file)
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/strings/regexp_elim.h"
 
+#include "expr/proof_node_manager.h"
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_entail.h"

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 0157a47f042b47b50fa2fc66102a3c989cd2ac29..bd95933a5be77e1a15df7749fa2dbaf535f6a728 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -19,6 +19,7 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/ext_theory.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 82463367e7f2e48893b6bcf331fdd437a18f3803..a725f4d88dec8e8a3cca46fe330d8f80e59cafd2 100644 (file)
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/term_registration_visitor.h"
 
+#include "base/configuration.h"
 #include "options/quantifiers_options.h"
 #include "theory/theory_engine.h"
 

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index fef3fdc67704151ad41fa049e52dd9c869d32588..19fc913120aa4dc1aa739b0654f2e91635b27435 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -26,10 +26,16 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/ee_setup_info.h"
 #include "theory/ext_theory.h"
+#include "theory/output_channel.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/substitutions.h"
+#include "theory/theory_inference_manager.h"
+#include "theory/theory_model.h"
 #include "theory/theory_rewriter.h"
+#include "theory/theory_state.h"
+#include "theory/trust_substitutions.h"
 
 using namespace std;
 

diff --git a/src/theory/theory.h b/src/theory/theory.h
index fa26ab65e9ccb9b7d49d570e6386d94b8002486f..5f4698e563229c6743f5c36c5465069bbff36804 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -20,49 +20,39 @@
 #define CVC4__THEORY__THEORY_H
 
 #include <iosfwd>
-#include <map>
 #include <set>
 #include <string>
 #include <unordered_set>
 
-#include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "options/options.h"
 #include "options/theory_options.h"
-#include "smt/logic_request.h"
 #include "theory/assertion.h"
 #include "theory/care_graph.h"
-#include "theory/decision_manager.h"
-#include "theory/ee_setup_info.h"
 #include "theory/logic_info.h"
-#include "theory/output_channel.h"
 #include "theory/theory_id.h"
-#include "theory/theory_inference_manager.h"
-#include "theory/theory_rewriter.h"
-#include "theory/theory_state.h"
 #include "theory/trust_node.h"
-#include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 
-class TheoryEngine;
 class ProofNodeManager;
+class TheoryEngine;
 
 namespace theory {
 
+class DecisionManager;
+struct EeSetupInfo;
+class OutputChannel;
 class QuantifiersEngine;
+class TheoryInferenceManager;
 class TheoryModel;
-class SubstitutionMap;
 class TheoryRewriter;
-
-namespace rrinst {
-  class CandidateGenerator;
-}/* CVC4::theory::rrinst namespace */
+class TheoryState;
+class TrustSubstitutionMap;
 
 namespace eq {
   class EqualityEngine;

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 53a812653d02cc6bd7e9f5c54fcc38a592dbc4c2..810f31ce53690204b681681aa8f31d20b5bf783f 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -15,8 +15,11 @@
 #include "theory/theory_inference_manager.h"
 
 #include "smt/smt_statistics_registry.h"
+#include "theory/output_channel.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index d3a317cbcf2b1c06b84ac1ea39c52b0e81f0e8d9..61b105dac59d2a63679c8313081ff2dbe26ed147 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -23,9 +23,8 @@
 #include "expr/node.h"
 #include "theory/inference_id.h"
 #include "theory/output_channel.h"
-#include "theory/theory_state.h"
 #include "theory/trust_node.h"
-#include "theory/uf/proof_equality_engine.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -34,8 +33,10 @@ class ProofNodeManager;
 namespace theory {
 
 class Theory;
+class TheoryState;
 namespace eq {
 class EqualityEngine;
+class ProofEqEngine;
 }
 
 /**

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 9604dc72b348373ca7f35a3e87af380c0d6ef0c9..89f53acb8d8bcb3821c79991602e55d9dc593908 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -14,6 +14,7 @@
 #include "theory/theory_model_builder.h"
 
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"

diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h
index a0586bd0c9b73efee4b4ec735e0e5709a2fb0cea..d4d2a78a5cb88366c72972c8c3f5d66524cbaf4f 100644 (file)
--- a/src/theory/trust_node.h
+++ b/src/theory/trust_node.h
@@ -18,11 +18,11 @@
 #define CVC4__THEORY__TRUST_NODE_H
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 
 class ProofGenerator;
+class ProofNode;
 
 namespace theory {
 

diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
index 7ab43091a0ab77b248f5a289edbd670342e00a0b..58d5f4924d3e32a1dd2d06dfe9567330e1f3b93e 100644 (file)
--- a/src/theory/uf/eq_proof.cpp
+++ b/src/theory/uf/eq_proof.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/uf/eq_proof.h"
 
+#include "base/configuration.h"
 #include "expr/proof.h"
 #include "options/uf_options.h"
 

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 497e394c77154db6afa3e767c5e04d33fe44585c..49e19c15f1f7f85b3e916b3506b31434486eebe9 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -25,6 +25,7 @@
 #include "expr/node_trie.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 #include "theory/uf/proof_equality_engine.h"

diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 9233bde530219acc38a1e62f9a8881dfeaa12f74..5d017cb0f3025d4f2a0a3229c2dd7470848c7781 100644 (file)
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -18,6 +18,8 @@
 
 #include "util/bitvector.h"
 
+#include "base/exception.h"
+
 namespace CVC4 {
 
 unsigned BitVector::getSize() const { return d_size; }

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 997293639ce3fc223b652455637d4e2102d0175b..b1a27929ac8f50a407b6e52cd28865d756586591 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -21,7 +21,6 @@
 
 #include <iosfwd>
 
-#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {

diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 585512138a0bf9e7361785fd0fc725da6cf53566..f78b076deeddb205cff0f323318140e08ce87728 100644 (file)
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -16,7 +16,10 @@
 
 #include "util/cardinality.h"
 
+#include <ostream>
+
 #include "base/check.h"
+#include "base/exception.h"
 
 namespace CVC4 {
 

diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 8ad3edbe24cffd1f42d43e0b372f8e28a8c718af..9218095a8780ee9c052f533bedb2b476d4759441 100644 (file)
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -20,10 +20,8 @@
 #ifndef CVC4__CARDINALITY_H
 #define CVC4__CARDINALITY_H
 
-#include <iostream>
-#include <utility>
+#include <iosfwd>
 
-#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {

diff --git a/src/util/divisible.h b/src/util/divisible.h
index 36bb37db0937319a89dcb5d5bf586312025c18bb..b2682b0556fed5013e077dcd86dacbc641485630 100644 (file)
--- a/src/util/divisible.h
+++ b/src/util/divisible.h
@@ -21,8 +21,9 @@
 #define CVC4__DIVISIBLE_H
 
 #include <iosfwd>
+#include <ostream>
+#include <stddef.h>
 
-#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {

diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp
index c972388921868812bdf87a77d12fbd9f27b5084e..ce8b50bc893fe2e86c0db671c0a19636a24f1417 100644 (file)
--- a/src/util/ostream_util.cpp
+++ b/src/util/ostream_util.cpp
@@ -15,6 +15,8 @@
  **/
 #include "util/ostream_util.h"
 
+#include <ostream>
+
 namespace CVC4 {
 
 StreamFormatScope::StreamFormatScope(std::ostream& out)

diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h
index b27c22819dbb1bd0daea992c7ccc40977c0ef63b..6e2a291a3739c6a696c696a0448fb118f1168ad2 100644 (file)
--- a/src/util/ostream_util.h
+++ b/src/util/ostream_util.h
@@ -20,7 +20,7 @@
 #define CVC4__UTIL__OSTREAM_UTIL_H
 
 #include <ios>
-#include <ostream>
+#include <iosfwd>
 
 namespace CVC4 {
 

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 17dac50b3ca9dc11db699b0ca365d1e00d728022..0534be1b74ad948e6d03d2d3ad5a0212bef6795e 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -16,8 +16,13 @@
 **/
 #include "util/resource_manager.h"
 
+#include <algorithm>
+#include <ostream>
+
 #include "base/check.h"
+#include "base/listener.h"
 #include "base/output.h"
+#include "options/options.h"
 #include "options/smt_options.h"
 #include "util/statistics_registry.h"
 

diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 3be99021b8fae6eb58d8bd98382e599da22d1225..a4a9b7f4e44824fbbaf4702bd450c203c2cf19ab 100644 (file)
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -21,18 +21,15 @@
 #ifndef CVC4__RESOURCE_MANAGER_H
 #define CVC4__RESOURCE_MANAGER_H
 
-#include <sys/time.h>
-
+#include <stdint.h>
 #include <chrono>
 #include <memory>
-
-#include "base/exception.h"
-#include "base/listener.h"
-#include "options/options.h"
-#include "util/unsafe_interrupt_exception.h"
+#include <vector>
 
 namespace CVC4 {
 
+class Listener;
+class Options;
 class StatisticsRegistry;
 
 /**

diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index 73e6afb9655bfe3e257f0b63621c5361c3d62337..781c73aec8f98b33e59f15aa4e6c52f3fadd6637 100644 (file)
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -17,8 +17,6 @@
 
 #include "util/statistics.h"
 
-#include <typeinfo>
-
 #include "util/safe_print.h"
 #include "util/statistics_registry.h" // for details about class Stat
 

diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index d2f7244f97a703c87c12dd4b6ee1fab537b2f849..efa1de1c05ee04790330f8c18551b525ecf0f4ef 100644 (file)
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -43,7 +43,6 @@
 #include <vector>
 
 #include "base/exception.h"
-#include "lib/clock_gettime.h"
 #include "util/safe_print.h"
 #include "util/statistics.h"
 

diff --git a/src/util/tuple.h b/src/util/tuple.h
index 240e4179203eb803f1ebec8d44caa27ca26a1870..109d4640b238af806b0bd877492b53b5e52e51be 100644 (file)
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -20,7 +20,6 @@
 #define CVC4__TUPLE_H
 
 #include <iostream>
-#include <string>
 #include <vector>
 #include <utility>
 

diff --git a/src/util/utility.cpp b/src/util/utility.cpp
index 7a50eb7fd16b9855bc7985e9db881ee63ad6278e..2b848d9249657e83e0c91f8d90a5cfb8ede26e6f 100644 (file)
--- a/src/util/utility.cpp
+++ b/src/util/utility.cpp
@@ -19,7 +19,6 @@
 #include <unistd.h>
 
 #include <cstdlib>
-#include <iostream>
 
 #include "base/check.h"
 

diff --git a/src/util/utility.h b/src/util/utility.h
index 549b98d669bd30d38359615b355d825e94a96786..06155788f8c02729f6d6eb9cb31a18338c8d7675 100644 (file)
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -21,10 +21,8 @@
 
 #include <algorithm>
 #include <fstream>
-#include <functional>
 #include <memory>
 #include <string>
-#include <utility>
 
 namespace CVC4 {
 

diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp
index ddbdcde6b9674412657a4e1a525386aea8cc18bb..f50d529d55ec1efcf072ca38db955bc560b0a1a7 100644 (file)
--- a/test/unit/expr/node_black.cpp
+++ b/test/unit/expr/node_black.cpp
@@ -21,6 +21,7 @@
 
 #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"

diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 7aecdd3b261363d68d7160c86cd6e5fc42a93c16..cd77f355db3e64bea71688c2d9a402d3271588c6 100644 (file)
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -15,12 +15,16 @@
 #ifndef CVC4__TEST__UNIT__TEST_SMT_H
 #define CVC4__TEST__UNIT__TEST_SMT_H
 
+#include "expr/dtype_cons.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "test.h"
+#include "theory/output_channel.h"
+#include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_state.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 #include "util/unsafe_interrupt_exception.h"

diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp
index 8bdf82622fe45e56a8cd322c69d3c5fb7747811b..5e5b52d3e0e071595213689b5898d9c655b6634a 100644 (file)
--- a/test/unit/theory/theory_arith_white.cpp
+++ b/test/unit/theory/theory_arith_white.cpp
@@ -12,6 +12,7 @@
  ** \brief Whitebox tests for theory Arithmetic.
  **/
 
+#include <list>
 #include <vector>
 
 #include "context/context.h"

diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index 0ef095fd9fdce07ac90274937e270d0e45a5a46e..0120dda760c945270d3885efa4f28f205a5e87cb 100644 (file)
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -18,6 +18,7 @@
 
 #include "api/cvc4cpp.h"
 #include "expr/dtype.h"
+#include "expr/dtype_cons.h"
 #include "expr/expr.h"
 #include "expr/type_node.h"
 #include "test_expr.h"