Some more cleanup of includes (#6083)

This PR does some more cleanup of the includes.

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index e259452911df0291ea50fa85eba275fb5f975951..4ab552001b42d17ba9abbd2dab3d3519a60b9af9 100644 (file)
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -86,7 +86,6 @@
 #include <functional>
 #include <iterator>
 #include <unordered_map>
-#include <vector>
 
 #include "base/check.h"
 #include "context/cdhashmap_forward.h"

diff --git a/src/context/cdlist.h b/src/context/cdlist.h
index 2abd0b82494d92ff1598ad723fb10c93a80fd632..b1c8229f0d520bb39392720c0a2331d7dab83d22 100644 (file)
--- a/src/context/cdlist.h
+++ b/src/context/cdlist.h
@@ -22,9 +22,7 @@
 
 #include <cstring>
 #include <iterator>
-#include <memory>
 #include <string>
-#include <sstream>
 
 #include "base/check.h"
 #include "context/cdlist_forward.h"

diff --git a/src/context/cdtrail_queue.h b/src/context/cdtrail_queue.h
index cf36156cf97d313228728fef2bfc4b75307f68fe..f505004cb486b311ec2e1618b2a3b3ce3fe5da13 100644 (file)
--- a/src/context/cdtrail_queue.h
+++ b/src/context/cdtrail_queue.h
@@ -22,12 +22,13 @@
 #ifndef CVC4__CONTEXT__CDTRAIL_QUEUE_H
 #define CVC4__CONTEXT__CDTRAIL_QUEUE_H
 
-#include "context/context.h"
 #include "context/cdlist.h"
+#include "context/cdo.h"
 
 namespace CVC4 {
 namespace context {
 
+class Context;
 
 template <class T>
 class CDTrailQueue {

diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index db9d89dd15d9a03c9fa1319e445cc02a5487c952..4d941332001ab5a333524bc672368ac9fed1989c 100644 (file)
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -15,9 +15,11 @@
  **/
 
 #include <cstdlib>
-#include <vector>
 #include <deque>
+#include <limits>
 #include <new>
+#include <ostream>
+#include <vector>
 
 #ifdef CVC4_VALGRIND
 #include <valgrind/memcheck.h>
@@ -166,6 +168,12 @@ void ContextMemoryManager::pop() {
     d_freeChunks.pop_front();
   }
 }
+#else
+
+unsigned ContextMemoryManager::getMaxAllocationSize()
+{
+  return std::numeric_limits<unsigned>::max();
+}
 
 #endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */
 

diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index 43e0e1f949875d876d391817b2d3aaef37f02d9c..e20b9fdb94ebc500b800e67b8b1e82fb4ab3ccd5 100644 (file)
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -20,8 +20,9 @@
 #ifndef CVC4__CONTEXT__CONTEXT_MM_H
 #define CVC4__CONTEXT__CONTEXT_MM_H
 
+#ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
 #include <deque>
-#include <limits>
+#endif
 #include <vector>
 
 namespace CVC4 {
@@ -161,10 +162,7 @@ class ContextMemoryManager {
 class ContextMemoryManager
 {
  public:
-  static unsigned getMaxAllocationSize()
-  {
-    return std::numeric_limits<unsigned>::max();
-  }
+  static unsigned getMaxAllocationSize();
 
   ContextMemoryManager() { d_allocations.push_back(std::vector<char*>()); }
   ~ContextMemoryManager()

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 99e0bd96954bf9e0509ecbb7204b40fc39dd9d61..7eba1b2ea404660d8a9635325ebcef2d14131382 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -36,7 +36,6 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
-#include "options/options.h"
 
 namespace CVC4 {
 

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 5bea85b0052db9ff91b3dd4fb582a0c0d5f8c1d9..42c3862201c452916810b4a98cce688fa3c687f2 100644 (file)
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/node_manager.h"
 #include "options/smt_options.h"
+#include "expr/lazy_proof.h"
 #include "proof/proof_manager.h"
 #include "smt/preprocess_proof_generator.h"
 #include "theory/builtin/proof_checker.h"

diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp
index 82c1a14d4eed40977bd2f7339768a17ada28f51a..9f26d38000c034bd268d1e0b5f325c9c5e07bc1b 100644 (file)
--- a/src/printer/let_binding.cpp
+++ b/src/printer/let_binding.cpp
@@ -14,6 +14,8 @@
 
 #include "printer/let_binding.h"
 
+#include <sstream>
+
 namespace CVC4 {
 
 LetBinding::LetBinding(uint32_t thresh)

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 26bab2e5c7b040e50963d6775012d491ed0478ad..17d2f4d2f5695fb0f3f65b08b44375fecb8f6460 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -32,6 +32,7 @@ namespace CVC4 {
 class ResourceManager;
 class DecisionEngine;
 class OutputManager;
+class ProofNodeManager;
 class TheoryEngine;
 
 namespace prop {

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 6ad0562abfddc52194b383d04343ec033abd5928..5fcb57beb04d139e15ea1adaefd9dc4a09a3c9f5 100644 (file)
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/assertions.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "options/base_options.h"
 #include "options/language.h"

diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 167caf3792539ec9cc10067cbdad3d0c247efd30..1a8a6e3d0123248cdd7c15afcad3dee5ca028316 100644 (file)
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -20,7 +20,6 @@
 #include <memory>
 #include <vector>
 
-#include "context/context.h"
 #include "expr/node.h"
 
 namespace CVC4 {

diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 84c4acfac7f3d16b26911da8ae09560c863d6e13..ed19549c931774cdb3e8fb85c0fe74dbb0b4f639 100644 (file)
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -17,16 +17,18 @@
 #ifndef CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
 #define CVC4__SMT__PREPROCESS_PROOF_GENERATOR_H
 
-#include <map>
-
 #include "context/cdhashmap.h"
 #include "expr/lazy_proof.h"
+#include "expr/proof.h"
 #include "expr/proof_set.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class LazyCDProof;
+class ProofNodeManager;
+
 namespace smt {
 
 /**

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index a3c3a5ae2a6ef8325f9549dce096735a7ab666ee..e5dd7869c092134117e8900562baf02c1ebc6cd0 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -15,6 +15,7 @@
 #include "smt/preprocessor.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "printer/printer.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"

diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 0191d17e5f89e2aad7714b041b472a5b49756a25..eadbbedc537d978c8ca84797ea9899fcb28138fb 100644 (file)
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -30,6 +30,7 @@ class PreprocessingPassContext;
 namespace smt {
 
 class AbstractValues;
+class PreprocessProofGenerator;
 
 /**
  * The preprocessor module of an SMT engine.

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 45cd8284de629065993f6fbd1afeb73187523117..9a6486dedd6a98e7b90cce6e6c3362a567658f2b 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -14,7 +14,6 @@
 
 #include "smt/process_assertions.h"
 
-#include <stack>
 #include <utility>
 
 #include "expr/node_manager_attributes.h"
@@ -27,8 +26,10 @@
 #include "options/strings_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
+#include "smt/assertions.h"
 #include "smt/defined_function.h"
 #include "smt/dump.h"
 #include "smt/expand_definitions.h"

diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index b0577978032826efdf1169c54a39d353cd0dc765..f1c0aed3b0ad24a3bc3508a7a4694440523acda3 100644 (file)
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -21,18 +21,21 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/type_node.h"
-#include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "smt/assertions.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 
+namespace preprocessing {
+class AssertionPipeline;
+class PreprocessingPass;
+class PreprocessingPassContext;
+}
+
 namespace smt {
 
+class Assertions;
 class ExpandDefs;
 struct SmtEngineStatistics;
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 79678a5c0d1b4b03763287ff9f61df2d669abde0..7e8a4fb862a6db7770532ed641804f67cf55bcb4 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -44,6 +44,7 @@
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
+#include "smt/logic_exception.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 50f7ddfc7b1a5acd31435ccb40215a61210e7a48..4f10b6bc507483ee4c2264dbfbd5b30938c4d9e1 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -19,12 +19,12 @@
 #ifndef CVC4__SMT_ENGINE_H
 #define CVC4__SMT_ENGINE_H
 
+#include <map>
+#include <memory>
 #include <string>
 #include <vector>
-#include <map>
 
 #include "context/cdhashmap_forward.h"
-#include "context/cdlist_forward.h"
 #include "options/options.h"
 #include "smt/output_manager.h"
 #include "smt/smt_mode.h"
@@ -87,7 +87,6 @@ class Model;
 class SmtEngineState;
 class AbstractValues;
 class Assertions;
-class ExprNames;
 class DumpManager;
 class ResourceOutListener;
 class SmtNodeManagerListener;
@@ -110,7 +109,6 @@ class DefinedFunction;
 
 struct SmtEngineStatistics;
 class SmtScope;
-class ProcessAssertions;
 class PfManager;
 class UnsatCoreManager;
 
@@ -120,7 +118,6 @@ ProofManager* currentProofManager();
 /* -------------------------------------------------------------------------- */
 
 namespace theory {
-  class TheoryModel;
   class Rewriter;
   class QuantifiersEngine;
 }/* CVC4::theory namespace */

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ab251503b7ffab335c784b2f6073b6cdf010cfba..89e75d89218144d5a5ccee7d89aba19e36435c35 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_state.h"
 #include "smt/smt_engine_stats.h"
+#include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
 

diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h
index ba02b5746d0a924680fa0f49939eccae6c2cd8a0..daa83ed54fde86fd09b108ecd3479d4da41031e3 100644 (file)
--- a/src/smt/unsat_core_manager.h
+++ b/src/smt/unsat_core_manager.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__SMT__UNSAT_CORE_MANAGER_H
 #define CVC4__SMT__UNSAT_CORE_MANAGER_H
 
-#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/proof_node.h"

diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 66e35bd52e6593347a231ea03a3fa2580d0dd504..c48948ade075182f8346cfb568635a314017ed34 100644 (file)
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -19,7 +19,6 @@
 
 #include <unordered_set>
 
-#include "expr/node_manager.h"
 #include "expr/proof.h"
 #include "expr/proof_generator.h"
 #include "expr/term_conversion_proof_generator.h"

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 152146cdfcf03b9f3af0f2741a7ec7c90a82c964..80690f39cada8bc688c13c1d255e446abdb612b9 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -28,6 +28,7 @@
 #include "theory/arith/cut_log.h"
 #include "theory/arith/matrix.h"
 #include "theory/arith/normal_form.h"
+#include "theory/eager_proof_generator.h"
 
 using namespace std;
 

diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 58e115b819d0ae6441527ad2258bab040d6e245b..46e252ec703bcd9c5a486c00c49a77e57b9dd22c 100644 (file)
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -66,7 +66,6 @@ class NodeLog;
 class TreeLog;
 class ArithVariables;
 class CutInfo;
-class RowsDeleted;
 
 class ApproximateSimplex{
  public:

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 0c19234482075d875a97c79198ca23f0b7681116..a075c87fe1d9bf8e217aaa7b14cb27f26e9d73cc 100644 (file)
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/arith/arith_preprocess.h"
 
+#include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 69cc02bb97962ca40edd5d86381bf9a4d2e52ed5..db0fd7d5e30735c46dc2f4a9500a79388934d6b7 100644 (file)
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -18,16 +18,19 @@
 #define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
 
 #include "context/cdhashmap.h"
-#include "theory/arith/arith_state.h"
-#include "theory/arith/inference_manager.h"
 #include "theory/arith/operator_elim.h"
 #include "theory/logic_info.h"
-#include "theory/skolem_lemma.h"
 
 namespace CVC4 {
 namespace theory {
+
+class SkolemLemma;
+
 namespace arith {
 
+class ArithState;
+class InferenceManager;
+
 /**
  * This module can be used for (on demand) elimination of extended arithmetic
  * operators like div, mod, to_int, is_int, sqrt, and so on. It uses the

diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index 2b74e600548cae2c0d887190f47e30267e129100..799d0bcee074396e961d5648f8560ad27ff9cfcc 100644 (file)
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -20,14 +20,15 @@
 #ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 #define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 
-#include <set>
-
 #include "context/cdhashmap.h"
-#include "context/context.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/delta_rational.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 

diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index f9051328cfd2cb3fe495776893dce5319336d657..4f1f50b7a5a8d35602e593d3d0a9f21f2dab51ac 100644 (file)
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -14,6 +14,8 @@
 
 #include "arith_utilities.h"
 
+#include <cmath>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -114,7 +116,7 @@ Node getApproximateConstant(Node c, bool isLower, unsigned prec)
   Rational cr = c.getConst<Rational>();
 
   unsigned lower = 0;
-  unsigned upper = pow(10, prec);
+  unsigned upper = std::pow(10, prec);
 
   Rational den = Rational(upper);
   if (cr.getDenominator() < den.getNumerator())

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index e4d6bd0ee474039b0de898e6144c1750fac42ce5..40ca7b8f63e394dc098ca4e660e760f1fa8e3fc9 100644 (file)
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 #define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
-#include <math.h>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>
@@ -25,7 +24,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
 #include "util/dense_map.h"
 #include "util/integer.h"
 #include "util/rational.h"

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index efcb9632569e5818aa2013a812a5cbc21fb3ee0f..e5c99597184a358517c6f258585c70b6f4412da2 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -21,6 +21,8 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/tableau.h"
 
 using namespace std;
 

diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 84bfafcc8785b40f27e4a049eec13358bbcedad9..ee412483bf6cd894bd0803966c8b78b64bacbae4 100644 (file)
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/arith/callbacks.h"
 
+#include "expr/proof_node.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/arith/theory_arith_private.h"
 

diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 9fbe3b90fe20953f67c3b41ce3b0768c1664b590..574d289b0df2e60b242b4395f444c757d390f449 100644 (file)
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -18,13 +18,15 @@
 #pragma once
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/rational.h"
 
 namespace CVC4 {
+
+class ProofNode;
+
 namespace theory {
 namespace arith {
 

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 636cebe5fd161c7485e9af9bea2d765e1e1ce41f..f2210574bccba536c93a0a1e3b979d0ee21225df 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -18,9 +18,16 @@
 #include "theory/arith/congruence_manager.h"
 
 #include "base/output.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/constraint.h"
+#include "theory/arith/partial_model.h"
+#include "theory/ee_setup_info.h"
+#include "theory/rewriter.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
 #include "options/arith_options.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index f2aef815f2048ccb81d4953b9603dd7fa31e9878..9815ad9c84c460867e181cc87d67ac2b19c6f42a 100644 (file)
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -19,27 +19,42 @@
 
 #pragma once
 
+#include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
-#include "context/cdo.h"
 #include "context/cdtrail_queue.h"
-#include "context/context.h"
-#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/callbacks.h"
 #include "theory/arith/constraint_forward.h"
-#include "theory/arith/partial_model.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/ee_setup_info.h"
 #include "theory/trust_node.h"
-#include "theory/uf/equality_engine.h"
-#include "theory/uf/proof_equality_engine.h"
+#include "theory/uf/equality_engine_notify.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
+namespace context {
+class Context;
+class UserContext;
+}
+
 namespace theory {
+
+class EagerProofGenerator;
+struct EeSetupInfo;
+
+namespace eq {
+class ProofEqEngine;
+class EqualityEngine;
+}
+
 namespace arith {
 
+class ArithVariables;
+
 class ArithCongruenceManager {
 private:
   context::CDRaised d_inConflict;

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 70106b14c51166c9e075616dd830dbdf9b11bad9..bafd4d6827abebe231cb6ab049d38055c4fecd01 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -21,9 +21,14 @@
 #include <unordered_set>
 
 #include "base/output.h"
+#include "expr/proof_node_manager.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/congruence_manager.h"
 #include "theory/arith/normal_form.h"
+#include "theory/arith/partial_model.h"
+#include "theory/rewriter.h"
 
 
 using namespace std;

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 6a73d69d206de05c08196c8ee13369348377464c..6ac03bb82fda7143b216f8c3d105c3a946a3d916 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -78,36 +78,38 @@
 #ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
 #define CVC4__THEORY__ARITH__CONSTRAINT_H
 
-#include <list>
-#include <set>
 #include <unordered_map>
 #include <vector>
 
 #include "base/configuration_private.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "expr/node.h"
-#include "expr/proof_node_manager.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/callbacks.h"
-#include "theory/arith/congruence_manager.h"
 #include "theory/arith/constraint_forward.h"
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/proof_macros.h"
 #include "theory/trust_node.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
-namespace theory {
-namespace arith {
-class Comparison;
-}
-}
+
+class ProofNodeManager;
+
+namespace context {
+class Context;
 }
-namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace arith {
 
+class Comparison;
+class ArithCongruenceManager;
+class ArithVariables;
+
 /**
  * Logs the types of different proofs.
  * Current, proof types:

diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index f6f974fcadad1f6697a0444a361def9b9fecc5b9..2b67026dc469ac9e2dd9779bf53610d60d4d5fe4 100644 (file)
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -22,13 +22,11 @@
 #include <unordered_map>
 #include <map>
 #include <set>
-#include <vector>
 
 #include "expr/kind.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/constraint_forward.h"
 #include "util/dense_map.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
@@ -230,7 +228,6 @@ public:
 };
 std::ostream& operator<<(std::ostream& os, const NodeLog& nl);
 
-class ApproximateSimplex;
 class TreeLog {
 private:
   int next_exec_ord;

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 2c06967c43a19933b22001f6ccfdc53fd4d72d88..a232464e56e8b1b071156a0d4bc5906c47a7837b 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -20,6 +20,7 @@
 #include "base/output.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/arith/partial_model.h"
 
 using namespace std;
 

diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 571c64a783c5de3f5df59bbdc6bd15c5629cab54..3ce7199c0a31429fa7f926ccec39aeba83bf294c 100644 (file)
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -24,18 +24,18 @@
 #include <utility>
 #include <vector>
 
-#include "base/output.h"
 #include "context/cdlist.h"
 #include "context/cdmaybe.h"
 #include "context/cdo.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "theory/arith/normal_form.h"
-#include "theory/arith/partial_model.h"
 #include "util/rational.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 3784ec79b55dd11e10a6b3b594df81887b04fa83..5ad2f16c0b30a09712921ea2a5ae4b0921573017 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -21,6 +21,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
 
 
 using namespace std;

diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 34d695f8aca6f63ecde0745fc865ef8022b3cf13..7400a229ffe5baecb9328168c24d1abf9deee9fa 100644 (file)
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -62,7 +62,6 @@ namespace arith {
 
 
 class ErrorSet;
-class ErrorInfoMap;
 
 class ComparatorPivotRule {
 private:

diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 658f7c23ecf1dad4ffa01ec71f417490dc7b6bb8..45a9b79bb4d63259109130c65bcd4b3194acaad6 100644 (file)
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -55,7 +55,9 @@
 #pragma once
 
 #include "theory/arith/error_set.h"
+#include "theory/arith/linear_equality.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 

diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index e1eb786d0a129a13dcf95982e3e74e3ab3d4f4f1..03ab8e53b5e1d986912f6efc26597d4ce2af5fd8 100644 (file)
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -23,7 +23,6 @@
 
 #include "expr/node.h"
 #include "theory/arith/delta_rational.h"
-#include "theory/theory.h"
 #include "util/integer.h"
 #include "util/maybe.h"
 #include "util/rational.h"

diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index c4281f0bde9bce996ed16239e7d322a06f718aea..a281c825befaf65fef28a5453c225a3dffde2ab7 100644 (file)
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -15,6 +15,7 @@
 #include "theory/arith/inference_manager.h"
 
 #include "options/arith_options.h"
+#include "theory/arith/arith_state.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index 80cb62201575c76f0cd6f504c965e35e90229dde..dd617f4a3e30c8f3ac94c4c2432d0e7a44c65cdb 100644 (file)
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -17,18 +17,16 @@
 #ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
 #define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
 
-#include <map>
 #include <vector>
 
-#include "theory/arith/arith_state.h"
 #include "theory/inference_id.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
+class ArithState;
 class TheoryArith;
 
 /**

diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index f0a3fbe25d61d103a52652f706229d4f32e57692..42f8920c8cf56aee49d521b7effe84685e31f556 100644 (file)
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -23,12 +23,9 @@
 
 #include <poly/polyxx.h>
 
-#include <map>
 #include <tuple>
 #include <vector>
 
-#include "expr/kind.h"
-#include "expr/node_manager_attributes.h"
 #include "theory/arith/nl/poly_conversion.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 9302cb7f21e16ec88143744793e51cc55b7322ad..33267cb7aedc1f8f7de15d187ed0764142166138 100644 (file)
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -23,8 +23,6 @@
 
 #include <poly/polyxx.h>
 
-#include <algorithm>
-#include <iostream>
 #include <vector>
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index f13e6f4a331db93afe9c0214f4794dbc2ece857f..5ebe0c6b7a885831499b8eef8de2c272317730ae 100644 (file)
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 62d3c03ff5937878f50912a597751461f1bf2fe0..9f0799e7cfe9797783c690c33df500d17e7d5976 100644 (file)
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -16,6 +16,9 @@
 
 #ifdef CVC4_POLY_IMP
 
+#include "theory/lazy_tree_proof_generator.h"
+#include "theory/arith/nl/poly_conversion.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {

diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 72f0f766b8a7ecb8b8686dc0026630afb46f367c..4709b8e5970fab95f31a1b565f2d710dfaa7d7ea 100644 (file)
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -23,18 +23,21 @@
 
 #include <vector>
 
-#include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/proof_generator.h"
 #include "expr/proof_set.h"
 #include "theory/arith/nl/cad/cdcac_utils.h"
-#include "theory/arith/nl/poly_conversion.h"
 #include "theory/lazy_tree_proof_generator.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+
 namespace theory {
 namespace arith {
 namespace nl {
+
+struct VariableMapper;
+
 namespace cad {
 
 /**

diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 3a7d5159ad5ea35c015bd317b159c83444d4b309..b83398cd6fd630b27f138cd1a78cbd021df9c953 100644 (file)
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -23,6 +23,9 @@
 #include "theory/arith/nl/cad/proof_checker.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
 namespace theory {
 namespace arith {
 

diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp
index 4523686404094d6e315df3346fc6803d371cf514..9ec3b1fc11bcb72e61a61c74d83c406d78b398d1 100644 (file)
--- a/src/theory/arith/nl/ext/constraint.cpp
+++ b/src/theory/arith/nl/ext/constraint.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/nl/ext/monomial.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h
index 2f439f65e775e58c8ed0df18bfa9eee6703ae7f8..d5ed7ccfd0c80cd1937fba22355a89bf3770fe0f 100644 (file)
--- a/src/theory/arith/nl/ext/constraint.h
+++ b/src/theory/arith/nl/ext/constraint.h
@@ -20,13 +20,14 @@
 
 #include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/nl/ext/monomial.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+class MonomialDb;
+
 /** constraint information
  *
  * The struct ( d_rhs, d_coeff, d_type ) represents that a literal is of the

diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index c7841748fb2c4e16536a92a4ddd68b727dc56819..28373223b0cb79e41f1e80a9c10c395caba4b11b 100644 (file)
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -21,6 +21,8 @@
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index f64fc8feb1704f7724d549248b08774c315e87e5..7a0da42aac6436eb61350dcaa2284e1877a13afe 100644 (file)
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h
index c8d27ec2764dbbec6b71c827fbfa20f1be8cd7b3..4c017d1982c2ece8761b4f24ec3f1283f07227fb 100644 (file)
--- a/src/theory/arith/nl/ext/factoring_check.h
+++ b/src/theory/arith/nl/ext/factoring_check.h
@@ -18,13 +18,17 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
+
+class CDProof;
+
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class FactoringCheck
 {
  public:

diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index 2c25a6e294cd16da7b4d161f82a68756d390732a..47cb5daecf0783e41cd8ae84e3fddc682e5c0050 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -20,6 +20,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h
index 103e2725fd5b771f6c6d24947ef41b60c341b08a..e7ba4d861558669d5e0726f2cb975c01ca1f542e 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_bounds_check.h
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.h
@@ -17,13 +17,14 @@
 
 #include "expr/node.h"
 #include "theory/arith/nl/ext/constraint.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class MonomialBoundsCheck
 {
  public:

diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index 3f62d0afb70ae8bafe0b22940bf3c3f2fb4761af..7f99b876df687a3c8e75c54ff6ba08960b299e85 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -19,6 +19,8 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
+#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index b964f00a4cc65c4ec213a738ae7630306b986e01..a085544764019de8a4e055d8d4dee791d140fd73 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -16,14 +16,16 @@
 #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
+#include "theory/arith/nl/ext/monomial.h"
 #include "theory/theory_inference.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class MonomialCheck
 {
  public:

diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 09954bf192f550f3eb9be404aec14370364c5c15..45f4160a0feaf8649afa456cee5c264c890b2def 100644 (file)
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index bee2fe40529dbf27c4f6ffc3ec937d4840f0c235..0304457371a2c43fa1a222f3926b58abbf6be937 100644 (file)
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -17,13 +17,14 @@
 
 #include "expr/node.h"
 #include "context/cdhashset.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class SplitZeroCheck
 {
  public:

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 25415128377fd79c5852dcb4b612dd890bf7ab50..64ea19f3c3cdd967895a977964a4a62a18d70740 100644 (file)
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -19,6 +19,7 @@
 #include "theory/arith/arith_msum.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h
index e0656789b0f4497dd23315e0cd8ace23301a82ed..a771ae543d59be882b3dcf9c1d9c8ace3854d6c1 100644 (file)
--- a/src/theory/arith/nl/ext/tangent_plane_check.h
+++ b/src/theory/arith/nl/ext/tangent_plane_check.h
@@ -15,14 +15,17 @@
 #ifndef CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
 #define CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
 
+#include <map>
+
 #include "expr/node.h"
-#include "theory/arith/nl/ext/ext_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 namespace nl {
 
+struct ExtState;
+
 class TangentPlaneCheck
 {
  public:

diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h
index f1ad3df20d0f050a5b2bf7210bedf6627815c6bb..a3dc74ec8f46d45dd66f58ccacaebf9fc7ddca70 100644 (file)
--- a/src/theory/arith/nl/ext_theory_callback.h
+++ b/src/theory/arith/nl/ext_theory_callback.h
@@ -20,6 +20,9 @@
 
 namespace CVC4 {
 namespace theory {
+namespace eq {
+class EqualityEngine;
+}
 namespace arith {
 namespace nl {
 

diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index e484252f29dd6220fbbabf2d7b0f3b5ba7cff046..137d430c008100bbcfe1216fffd891e61f3703bb 100644 (file)
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -21,7 +21,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "theory/arith/nl/iand_utils.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index 15ccab231c2bf5a6a5c8c704f1b437ff5536d130..a84fcf9784b34797ad759998c4d987f811fc3bf5 100644 (file)
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -17,7 +17,6 @@
 #define CVC4__THEORY__ARITH__IAND_TABLE_H
 
 #include <map>
-#include <vector>
 
 #include "expr/node.h"
 

diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index dae13318c777bf91080c94e30a923a237cbbd7c2..5467c64cecc0fdc867a593c700866f190471e246 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/arith/nl/nl_lemma_utils.h"
 #include "theory/theory_model.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index f907963c116b056c47cf61836ae77fd6ad9bf0bb..cd52cb1592afe31cf32ecac312bdffc70ff38fcd 100644 (file)
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -21,7 +21,6 @@
 
 #include "expr/kind.h"
 #include "expr/node.h"
-#include "theory/arith/nl/nl_lemma_utils.h"
 
 namespace CVC4 {
 
@@ -36,6 +35,7 @@ class TheoryModel;
 namespace arith {
 namespace nl {
 
+class NlLemma;
 class NonlinearExtension;
 
 /** Non-linear model finder

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 38243823b237cae258d71e9d2599b4c7288ef350..3f32e7075090ed802b2d8399ee5dd3e722881342 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -24,6 +24,7 @@
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 47d62e6079e08b1c4b51a4c529e84e5a567fe4e1..baa0f886cd49d784921088a40a1ee0230ecc42e9 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -23,6 +23,7 @@
 
 #include "expr/node.h"
 #include "theory/arith/nl/cad_solver.h"
+#include "theory/arith/nl/ext/ext_state.h"
 #include "theory/arith/nl/ext/factoring_check.h"
 #include "theory/arith/nl/ext/monomial_bounds_check.h"
 #include "theory/arith/nl/ext/monomial_check.h"
@@ -37,6 +38,7 @@
 #include "theory/arith/nl/strategy.h"
 #include "theory/arith/nl/transcendental/transcendental_solver.h"
 #include "theory/ext_theory.h"
+#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
@@ -46,6 +48,7 @@ namespace eq {
 namespace arith {
 
 class InferenceManager;
+class TheoryArith;
 
 namespace nl {
 

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 68d5a5f31f2accb5dd6ae0042aa4ab2e00af2e97..8b6f4484deb5ce992410d026e2d635a70e8f00cc 100644 (file)
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -24,6 +24,8 @@
 #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/arith/nl/transcendental/transcendental_state.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 76b14022f60ce5fe6dbc9add12679bcfba501905..484174d5fbf6332477809ea188acc3c827344963 100644 (file)
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -16,12 +16,8 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
 
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
 
 #include "expr/node.h"
-#include "theory/arith/nl/transcendental/transcendental_state.h"
 
 namespace CVC4 {
 namespace theory {
@@ -29,6 +25,8 @@ namespace arith {
 namespace nl {
 namespace transcendental {
 
+struct TranscendentalState;
+
 /** Transcendental solver class
  *
  * This class implements model-based refinement schemes

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 0e5c09a2f45e4a5b05eeb994b38385a5f2f0dd71..528e0bea26f2019a8e16414b6117de0626e6b9e7 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -23,6 +23,9 @@
 #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/arith/nl/transcendental/transcendental_state.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 0b2e9d920572cef0ac3ddd30f1da05e26dd3abbd..c628559fc1f69e028a63927b56612fecb824e64c 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -16,9 +16,6 @@
 #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
 
 #include <map>
-#include <unordered_map>
-#include <unordered_set>
-#include <vector>
 
 #include "expr/node.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index c6b929fec04e82adbe7577d309fcfdf5ee5199ab..f236b472a58d5593eeadfe29d2929634ff65f562 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -23,6 +23,7 @@
 #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/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 438cc7047370ba9ea939c468ed5c876bdd39b1d6..593354794cd79e28592220ea48676a23fd17119d 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -16,6 +16,8 @@
 
 #include "expr/proof.h"
 #include "theory/arith/arith_utilities.h"
+#include "theory/arith/inference_manager.h"
+#include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 33994fa3a1f5bd757082876f3add98793ee9e7f4..cd5466e89f0db80d4e6b9fa24074004c991e70ef 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -17,8 +17,7 @@
 
 #include "expr/node.h"
 #include "expr/proof_set.h"
-#include "theory/arith/inference_manager.h"
-#include "theory/arith/nl/nl_model.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/transcendental/proof_checker.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
@@ -26,7 +25,13 @@ namespace CVC4 {
 class CDProof;
 namespace theory {
 namespace arith {
+
+class InferenceManager;
+
 namespace nl {
+
+class NlModel;
+
 namespace transcendental {
 
 /**

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index bf8ec6c588228c6633ffbba91950b66e602d64a3..c3500e6990b1025a0a47a48293a3657611b219d9 100644 (file)
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -21,7 +21,6 @@
 #define CVC4__THEORY__ARITH__NORMAL_FORM_H
 
 #include <algorithm>
-#include <list>
 
 #include "base/output.h"
 #include "expr/node.h"

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 6a9a130ca32db52f01d232fcb10bc4c03c5cd0a2..c6f9611296eb48bdb0011a213dc71b2887b77db3 100644 (file)
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -17,6 +17,7 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "options/arith_options.h"
 #include "smt/logic_exception.h"
 #include "theory/arith/arith_utilities.h"

diff --git a/src/theory/arith/operator_elim.h b/src/theory/arith/operator_elim.h
index 6dc5354449195e195202febcfdf1ba9f1b7fce30..489974eac4930dd1d83de56922234dcd9f4a0168 100644 (file)
--- a/src/theory/arith/operator_elim.h
+++ b/src/theory/arith/operator_elim.h
@@ -17,12 +17,14 @@
 #include <map>
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
 #include "theory/eager_proof_generator.h"
 #include "theory/logic_info.h"
 #include "theory/skolem_lemma.h"
 
 namespace CVC4 {
+
+class TConvProofGenerator;
+
 namespace theory {
 namespace arith {
 

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index ec682b948b46c5aaadd6ee8ff33a9cf7ff731188..af0fe37ec2f94f659d9ad9fe6dd6cf34e22f8fcb 100644 (file)
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -21,11 +21,9 @@
 #ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 #define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 
-#include <list>
 #include <vector>
 
 #include "context/cdlist.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
@@ -35,6 +33,9 @@
 #include "theory/arith/delta_rational.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace theory {
 namespace arith {
 

diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h
index 8d2a94215c6e7253a3ee6598a2e732a93760d02b..0745bdd615729006af72ca507ded2482afa4d868 100644 (file)
--- a/src/theory/arith/proof_checker.h
+++ b/src/theory/arith/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index c383c3a855a67c483de3022334f5dddd5409e580..fc3d919c3ceb2a73a40d2050f3e90651b3b2eabe 100644 (file)
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -15,12 +15,14 @@
  ** \todo document this file
  **/
 
+#include "theory/arith/simplex.h"
+
 #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"
-
+#include "theory/arith/linear_equality.h"
+#include "theory/arith/tableau.h"
 
 using namespace std;
 

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index d1f891676f8c5e3b0477ab8bfc0c5f0cf285eb7e..1100930686d73a4efda170a8612f41b8899c4916 100644 (file)
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -56,19 +56,20 @@
 
 #include <unordered_map>
 
+#include "options/arith_options.h"
 #include "theory/arith/arithvar.h"
-#include "theory/arith/delta_rational.h"
-#include "theory/arith/linear_equality.h"
 #include "theory/arith/partial_model.h"
-#include "theory/arith/tableau.h"
 #include "util/dense_map.h"
 #include "util/result.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
 class ErrorSet;
+class LinearEqualityModule;
+class Tableau;
 
 class SimplexDecisionProcedure {
 protected:

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index d47dba70f4ccee323d88c8d5f2aec82d0a887523..79136e77c1b1b12cb4fd0ec541e202d708ff746d 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/arith/constraint.h"
 #include "theory/arith/error_set.h"
+#include "theory/arith/tableau.h"
 #include "util/statistics_registry.h"
 
 using namespace std;

diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 5febe1bb079131edbd28b812ce09629b00823c7e..d9d11dcc550797f8c0675e34a4627dbf4a97a92b 100644 (file)
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -54,7 +54,9 @@
 
 #pragma once
 
+#include "theory/arith/linear_equality.h"
 #include "theory/arith/simplex.h"
+#include "theory/arith/simplex_update.h"
 #include "util/dense_map.h"
 #include "util/statistics_registry.h"
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 42cd16efc46d729d2ea242aef49c198d893e2084..937901c5716fc6e4cfe8c30be60783958a5def6a 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -25,6 +25,8 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/ext_theory.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1a41c9301e4018d57db90a963ef425619b02ac6d..a208c9b10d2b768112ec0ca27b9d05a472cdf11b 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,7 +22,6 @@
 #include "theory/arith/arith_rewriter.h"
 #include "theory/arith/arith_state.h"
 #include "theory/arith/inference_manager.h"
-#include "theory/arith/operator_elim.h"
 #include "theory/theory.h"
 
 namespace CVC4 {

diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 583ff8dee36aabd566984cdd2e277288f02f50f4..55a2472b33ff1bf1dbd044f0a46686c6a0468516 100644 (file)
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -18,22 +18,15 @@
 #pragma once
 
 #include <map>
-#include <queue>
 #include <vector>
 
 #include "context/cdhashset.h"
 #include "context/cdinsert_hashmap.h"
 #include "context/cdlist.h"
 #include "context/cdqueue.h"
-#include "context/context.h"
 #include "expr/kind.h"
-#include "expr/metakind.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/proof_generator.h"
-#include "options/arith_options.h"
-#include "smt/logic_exception.h"
-#include "smt_util/boolean_simplification.h"
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arithvar.h"
@@ -51,12 +44,8 @@
 #include "theory/arith/normal_form.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/proof_checker.h"
-#include "theory/arith/simplex.h"
 #include "theory/arith/soi_simplex.h"
 #include "theory/arith/theory_arith.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/rewriter.h"
-#include "theory/theory_model.h"
 #include "theory/trust_node.h"
 #include "theory/valuation.h"
 #include "util/dense_map.h"
@@ -67,6 +56,10 @@
 
 namespace CVC4 {
 namespace theory {
+
+class EagerProofGenerator;
+class TheoryModel;
+
 namespace arith {
 
 class BranchCutInfo;

diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 5adb0e7835750b31ae3055b02e4f9be23032d423..499f96bfb0c92a9aed165d8a25e4ef3a957a1ed2 100644 (file)
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -18,14 +18,11 @@
 #ifndef CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 #define CVC4__THEORY__ARRAYS__ARRAY_INFO_H
 
-#include <iostream>
-#include <map>
 #include <tuple>
 #include <unordered_map>
 
 #include "context/backtrackable.h"
 #include "context/cdlist.h"
-#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "util/statistics_registry.h"
 

diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h
index a8d1407a86187ee2ac561d5f92aad7732465ad9c..053502788e59621ad3527e69795fac5808951152 100644 (file)
--- a/src/theory/arrays/proof_checker.h
+++ b/src/theory/arrays/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 34a7a71b959f2a4d61a2badb41b98a066e82a152..689e72a44a3dfc34cd13618705cd095a177a1976 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -33,7 +33,6 @@
 #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"
 
 namespace CVC4 {

diff --git a/src/theory/atom_requests.h b/src/theory/atom_requests.h
index 05c159b4b1e0310461c58f0fc325b96b65698552..b8a653bc371c35d12cba99ecf2c2432e72f2c680 100644 (file)
--- a/src/theory/atom_requests.h
+++ b/src/theory/atom_requests.h
@@ -20,7 +20,7 @@
 #pragma once
 
 #include "expr/node.h"
-#include "theory/theory.h"
+#include "theory/theory_id.h"
 #include "context/cdlist.h"
 #include "context/cdhashset.h"
 #include "context/cdhashmap.h"

diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index 869b229ea0de85687325cc609bc704be153f234c..a7a0f8796804ac6126b046404332c00314df0d5f 100644 (file)
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -17,6 +17,10 @@
 #include "theory/bags/bag_solver.h"
 
 #include "theory/bags/inference_generator.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/normal_form.h"
+#include "theory/bags/solver_state.h"
+#include "theory/bags/term_registry.h"
 #include "theory/uf/equality_engine_iterator.h"
 
 using namespace std;

diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h
index e524f742270135555121fa23147dd59ba04418ed..914a12ae2e49e8f04f817643df8509108cb73ab6 100644 (file)
--- a/src/theory/bags/bag_solver.h
+++ b/src/theory/bags/bag_solver.h
@@ -17,19 +17,16 @@
 #ifndef CVC4__THEORY__BAG__SOLVER_H
 #define CVC4__THEORY__BAG__SOLVER_H
 
-#include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "theory/bags/infer_info.h"
 #include "theory/bags/inference_generator.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/normal_form.h"
-#include "theory/bags/solver_state.h"
-#include "theory/bags/term_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+class TermRegistry;
+
 /** The solver for the theory of bags
  *
  */

diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 3718aedb71c2629d2e672b70d9a228166b92c0d9..51b2e543825357e7b1ea90124dbbf9d2b9e71bc7 100644 (file)
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H
 
 #include "theory/bags/rewrites.h"
-#include "theory/rewriter.h"
+#include "theory/theory_rewriter.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {

diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index caf4070ec11283e95bd66f4e3c432973312a0ff5..f59c43cb6b2a88c270980f63d3f29e9a2a5fce6c 100644 (file)
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__BAGS_STATISTICS_H
 #define CVC4__THEORY__BAGS_STATISTICS_H
 
-#include "expr/kind.h"
 #include "theory/bags/rewrites.h"
 #include "util/statistics_registry.h"
 

diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index c61075f51cc1f822a8be0ea6e7e85004c59056ac..0d56080c47cf7701f207d5235a3726ee9a83a3bb 100644 (file)
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -17,6 +17,8 @@
 #include "expr/attribute.h"
 #include "expr/bound_var_manager.h"
 #include "expr/skolem_manager.h"
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
 #include "theory/uf/equality_engine.h"
 
 namespace CVC4 {

diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index d6fc184c780a01e4cb5d2bde6e65194adbd03615..bfaf5d0fc910be1274f3b5e66063b92ba3be9af7 100644 (file)
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -17,18 +17,16 @@
 #ifndef CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
 #define CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H
 
-#include <map>
-#include <vector>
-
 #include "expr/node.h"
 #include "infer_info.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/solver_state.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+
 /**
  * An inference generator class. This class is used by the core solver to
  * generate lemmas

diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 44a18bcc4b26f953c982b2b0b7dea80a13030355..dcc5387e9abbb20882b22a42cfaf0f3b99a6d535 100644 (file)
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/bags/inference_manager.h"
 
+#include "theory/bags/solver_state.h"
+
 using namespace std;
 using namespace CVC4::kind;
 

diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index 8b0fe05909b34a022563ed354a42ef60a5ac1ef0..d74d3c189d88dec7460c5c97478fa0d93b54d75a 100644 (file)
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -17,14 +17,14 @@
 #ifndef CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
 #define CVC4__THEORY__BAGS__INFERENCE_MANAGER_H
 
-#include "theory/bags/infer_info.h"
-#include "theory/bags/solver_state.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class SolverState;
+
 /** Inference manager
  *
  * This class manages inferences produced by the theory of bags. It manages

diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index 93f1af11d0c9b7f1a3fb34c4de9b07e8a3f30a5f..d8820d8c4a733f2931d32edf1a7c85821a54c85c 100644 (file)
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -18,7 +18,6 @@
 #define CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H
 
 #include <map>
-#include <vector>
 
 #include "theory/theory_state.h"
 

diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 38c49421942a836b79da67687f32c133e53aa68f..192fd6809e304938adddbfb8c3e26e021c51a7a9 100644 (file)
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -14,6 +14,9 @@
 
 #include "theory/bags/term_registry.h"
 
+#include "theory/bags/inference_manager.h"
+#include "theory/bags/solver_state.h"
+
 using namespace std;
 using namespace CVC4::kind;
 

diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index fcd822e168224fceb902e92b605481e9b6419040..87e61a026eb26594255733c957f3cf73b08f9f82 100644 (file)
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -18,16 +18,17 @@
 #define CVC4__THEORY__BAGS__TERM_REGISTRY_H
 
 #include <map>
-#include <vector>
 
 #include "context/cdhashmap.h"
-#include "theory/bags/inference_manager.h"
-#include "theory/bags/solver_state.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bags {
 
+class InferenceManager;
+class SolverState;
+
 /**
  * Term registry, the purpose of this class is to maintain a database of
  * commonly used terms, and mappings from bags to their "proxy variables".

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 253fe2b7f4a6dceaf6050c22e86de227b11744ac..2950739e420a02abcf2df17cdfcfe5514ac03266 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -14,6 +14,9 @@
 
 #include "theory/bags/theory_bags.h"
 
+#include "smt/logic_exception.h"
+#include "theory/bags/normal_form.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 3839629d4d9822ddc582c2680eab73a31b5c1c3b..df64c3f1c98aae7d249cd9dc190793620ff8e560 100644 (file)
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -17,17 +17,15 @@
 #ifndef CVC4__THEORY__BAGS__THEORY_BAGS_H
 #define CVC4__THEORY__BAGS__THEORY_BAGS_H
 
-#include <memory>
-
 #include "theory/bags/bag_solver.h"
 #include "theory/bags/bags_rewriter.h"
 #include "theory/bags/bags_statistics.h"
 #include "theory/bags/inference_generator.h"
 #include "theory/bags/inference_manager.h"
 #include "theory/bags/solver_state.h"
+#include "theory/bags/term_registry.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 1912d1ba6fbc65571c427ee9197c206308ba7ab5..b50ec34c71bb6d3d9bd3feeb7e019d4dc6e2ed64 100644 (file)
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -21,8 +21,12 @@
 #include <vector>
 
 #include "expr/node_algorithm.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 #include "theory/booleans/proof_circuit_propagator.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/theory.h"
+#include "util/hash.h"
 #include "util/utility.h"
 
 using namespace std;

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index a2e4febad965cedba2850d8a1df719aee9292a26..ba8c5782d49905a0febe3cfb624eaf23acb54d27 100644 (file)
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 
-#include <functional>
 #include <memory>
 #include <unordered_map>
 #include <vector>
@@ -30,15 +29,17 @@
 #include "context/context.h"
 #include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
-#include "theory/eager_proof_generator.h"
-#include "theory/theory.h"
 #include "theory/trust_node.h"
-#include "util/hash.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+class ProofNode;
+
 namespace theory {
+
+class EagerProofGenerator;
+
 namespace booleans {
 
 /**

diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h
index b3d7c0f646a5177a2009306e6ea30b3b4775e34e..1d807fd904b67533a3c9df11e89c61d887393952 100644 (file)
--- a/src/theory/booleans/proof_checker.h
+++ b/src/theory/booleans/proof_checker.h
@@ -19,7 +19,6 @@
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index a7ae4ac18771b2e6ba62cf3b819e932f5695826b..aaff8293363b04c68451d7a8dca3f63be29b646f 100644 (file)
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -18,6 +18,7 @@
 
 #include <sstream>
 
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {

diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h
index f9a51e0678332d83c395178509eccc0426f0f43f..fa472b602810ec180284f133a60aa4ba6cdd2f99 100644 (file)
--- a/src/theory/booleans/proof_circuit_propagator.h
+++ b/src/theory/booleans/proof_circuit_propagator.h
@@ -22,9 +22,13 @@
 #include <memory>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 namespace booleans {
 

diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 5878a4da5fec7116ebf9e30b1fa1c155dd1c4ba0..bf84d543b17bc3cf760831a2d467264205185408 100644 (file)
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -20,7 +20,6 @@
 #ifndef CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
 #define CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
 
-#include "theory/theory.h"
 #include "theory/theory_rewriter.h"
 
 namespace CVC4 {

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index aef88b539210d6a6519c3e1e934c461f8b08e44f..84e64baa407e121550984dfa587d735b4f47916a 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -21,7 +21,6 @@
 
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "theory/rewriter.h"
 #include "theory/builtin/theory_builtin_rewriter.h" // for array and lambda representation
 
 #include <sstream>

diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp
index faafacfc51b08b679c70cd00e16860a46293ca68..6f70821916fb3f93ae66a1875ea396f5d0baa88b 100644 (file)
--- a/src/theory/builtin/type_enumerator.cpp
+++ b/src/theory/builtin/type_enumerator.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/builtin/type_enumerator.h"
 
+#include "theory/builtin/theory_builtin_rewriter.h"
+
 namespace CVC4 {
 namespace theory {
 namespace builtin {

diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 25f750cf957aab91d95e5f2d62e696e9141fe5de..7b4b09f84cfc64f4d6afbe9f0eb706ebe5263437 100644 (file)
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -22,7 +22,6 @@
 #include "expr/kind.h"
 #include "expr/type_node.h"
 #include "expr/uninterpreted_constant.h"
-#include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/type_enumerator.h"
 #include "util/integer.h"
 

diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index b4d4960ed4aa90ad32bdef2cc663fd39c9a4df7a..465a8eb65543c8131cb91e6c656f64295780ed81 100644 (file)
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -20,6 +20,7 @@
 #include "cvc4_private.h"
 #include "options/bv_options.h"
 #include "prop/cnf_stream.h"
+#include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "smt/smt_statistics_registry.h"
 

diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 8f9deb2dacdc80715a7fb04f99a4f465e1b2d74a..d3326f85308a30ad49e6174aa363199344c60809 100644 (file)
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -20,7 +20,6 @@
 #define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
-#include "prop/sat_solver.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -35,6 +34,9 @@ class Cnf_Dat_t_;
 typedef Cnf_Dat_t_ Cnf_Dat_t;
 
 namespace CVC4 {
+namespace prop {
+class SatSolver;
+}
 namespace theory {
 namespace bv {
 

diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index f2b462b6b7f5e4a34ca11ec32a2778f06b144220..d66b46505fe053fe90d03f8d155607df3d24742d 100644 (file)
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -19,11 +19,11 @@
 #ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 #define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 
+#include <memory>
 #include <unordered_set>
 
 #include "theory/bv/bitblast/bitblaster.h"
 
-#include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 
 namespace CVC4 {

diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 053ca637389a35e35b1eea231c2e52405957524d..622369043c9554ffbe92248fb7a06f59e1430ae9 100644 (file)
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -23,12 +23,14 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
-#include "prop/cnf_stream.h"
-#include "prop/registrar.h"
 #include "prop/bv_sat_solver_notify.h"
 #include "theory/bv/abstraction.h"
 
 namespace CVC4 {
+namespace prop {
+class CnfStream;
+class NullRegistrat;
+}
 namespace theory {
 namespace bv {
 

diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 28624a949da13e3826323c4135f20a34a19891d4..6a1d61a3b191e430b899fdd96fed33167176f1c0 100644 (file)
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -19,9 +19,6 @@
 #ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 #define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
 
-#include <unordered_set>
-#include <vector>
-
 #include "expr/node.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/theory_model.h"

diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 39728c2ec9fdc795466ed516e181c1ac574605ea..be5da70b2b5d3aba3a20ab4253f21c9c9c4c53f0 100644 (file)
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -19,16 +19,15 @@
 #ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 #define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
 
-#include <list>
 #include <queue>
 #include <unordered_map>
 #include <unordered_set>
 
+#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdo.h"
 #include "context/cdqueue.h"
 #include "context/context.h"
-#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index dd1e7c9f77b03c7cf4efec9affb72b4d63b7c27d..a34ec98ada2ffeb6a384483cd7e5b252c06fa140 100644 (file)
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
 #define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
 
-#include <unordered_map>
-
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
 #include "theory/bv/proof_checker.h"

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 43fd9003019e511216a4c1ec18a6c1949cd319b2..38d94ea27c8f615edc700f8035a64a21c7c0b462 100644 (file)
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -28,6 +28,7 @@
 #include "theory/bv/bv_quick_check.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4::context;

diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 9af95fa20df8de281c07f7fa48d367ff49523430..969ded528057f5c9c6c9061be1f0fcfa0f529df1 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -21,7 +21,6 @@
 #include <unordered_map>
 #include <unordered_set>
 
-#include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "theory/bv/bv_subtheory.h"
 #include "theory/ext_theory.h"

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 1b471dd68ab28bc49f130f2d2563835087d64d4c..aa3607a66627eae523227f9f0cba6a79aed85d30 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -20,6 +20,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace std;

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index ab3c8d774855a703213b4de46866e128f18a2cad..a19c18df8dfa06eeb8afcc25fd9120c38658b0f0 100644 (file)
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -15,6 +15,8 @@
  **/
 #include "theory/bv/slicer.h"
 
+#include <sstream>
+
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0151791b7458ac745f515fc2f0f8be0ebd7ad5f2..4e7cfdd2a6d5f2ec4f6335a9108d27c27a773537 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -19,8 +19,6 @@
 #ifndef CVC4__THEORY__BV__THEORY_BV_H
 #define CVC4__THEORY__BV__THEORY_BV_H
 
-#include <unordered_map>
-
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"

diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index ee153a695f8d80d227d59b862631337c1a455ed2..9ecc2597354b39750910e59664090d338a02eee8 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -21,13 +21,11 @@
 #define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
 
 #include "theory/theory_rewriter.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
-struct AllRewriteRules;
 typedef RewriteResponse (*RewriteFunction) (TNode, bool);
 
 class TheoryBVRewriter : public TheoryRewriter

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 2a2639505cfe10100c62463a817d86987f51f7a0..c6c03e56193aa39eba944dbc1390f6862605320b 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -19,7 +19,6 @@
 #pragma once
 
 #include <set>
-#include <sstream>
 #include <unordered_map>
 #include <unordered_set>
 #include <vector>

diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp
index 4290ff989f0eb367114675aeb6c42f44c143c6e0..567a16636af96111809228123b8bbcdebac8b736 100644 (file)
--- a/src/theory/combination_care_graph.cpp
+++ b/src/theory/combination_care_graph.cpp
@@ -17,6 +17,7 @@
 #include "expr/node_visitor.h"
 #include "prop/prop_engine.h"
 #include "theory/care_graph.h"
+#include "theory/model_manager.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {

diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index ec2f7e336221d1463e72cf117ffa887982161a9a..160b56625f4fb2f53c246ab34546a4b2e52d0686 100644 (file)
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -16,8 +16,11 @@
 
 #include "expr/node_visitor.h"
 #include "theory/care_graph.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/ee_manager_distributed.h"
+#include "theory/model_manager.h"
 #include "theory/model_manager_distributed.h"
+#include "theory/shared_solver.h"
 #include "theory/shared_solver_distributed.h"
 #include "theory/theory_engine.h"
 

diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h
index 1e18ee5584eb7042ff8ad0268838c76d4347b176..a6331b4067e8439d34e3e80d1178576f0f9207ce 100644 (file)
--- a/src/theory/combination_engine.h
+++ b/src/theory/combination_engine.h
@@ -20,10 +20,7 @@
 #include <vector>
 #include <memory>
 
-#include "theory/eager_proof_generator.h"
 #include "theory/ee_manager.h"
-#include "theory/model_manager.h"
-#include "theory/shared_solver.h"
 #include "theory/valuation.h"
 
 namespace CVC4 {
@@ -32,6 +29,10 @@ class TheoryEngine;
 
 namespace theory {
 
+class EagerProofGenerator;
+class ModelManager;
+class SharedSolver;
+
 /**
  * Manager for doing theory combination. This class is responsible for:
  * (1) Initializing the various components of theory combination (equality

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index ad1947700af39a6e248cfd8e05a8c7f5e13be7cb..8ad927ce4dd33f499ef90dcf52bb5b0ba56c6e99 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -19,9 +19,7 @@
 #ifndef CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
 #define CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H
 
-#include "expr/node_manager_attributes.h"
 #include "theory/theory_rewriter.h"
-#include "theory/type_enumerator.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 0c8db3eaf8df5b19c8ba4a00607f59f016b7976f..b231e8fd4d1723435979108c1f10a8855196aba0 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -15,7 +15,9 @@
 #include "theory/datatypes/infer_proof_cons.h"
 
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/model_manager.h"
 #include "theory/rewriter.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h
index 11bc6409567231ebfd32c03bb129512d0a1b6b27..eeb8214e2deeb195b29200fc85c7efb522f72a81 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.h
+++ b/src/theory/datatypes/infer_proof_cons.h
@@ -17,14 +17,15 @@
 #ifndef CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
 #define CVC4__THEORY__DATATYPES__INFER_PROOF_CONS_H
 
-#include <vector>
-
+#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
 #include "theory/datatypes/inference.h"
-#include "theory/theory_proof_step_buffer.h"
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
 namespace theory {
 namespace datatypes {
 

diff --git a/src/theory/datatypes/inference.h b/src/theory/datatypes/inference.h
index aed58fa2d8bfcb1fe39ca2a3010a2964e8a0437e..9c19608c19833db47c0e44d3002afe0f27eb00cd 100644 (file)
--- a/src/theory/datatypes/inference.h
+++ b/src/theory/datatypes/inference.h
@@ -17,10 +17,10 @@
 #ifndef CVC4__THEORY__DATATYPES__INFERENCE_H
 #define CVC4__THEORY__DATATYPES__INFERENCE_H
 
-#include "context/cdhashmap.h"
 #include "expr/node.h"
-#include "theory/inference_manager_buffered.h"
 #include "theory/inference_id.h"
+#include "theory/theory_inference.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h
index 643ae669b94a2dfb0273a3cd9bee85909511cb1b..1107470430106a8b79dc434a4e24b708bf8b5e6c 100644 (file)
--- a/src/theory/datatypes/inference_manager.h
+++ b/src/theory/datatypes/inference_manager.h
@@ -17,10 +17,8 @@
 #ifndef CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
 #define CVC4__THEORY__DATATYPES__INFERENCE_MANAGER_H
 
-#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "theory/datatypes/infer_proof_cons.h"
-#include "theory/datatypes/inference.h"
 #include "theory/inference_manager_buffered.h"
 
 namespace CVC4 {

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 206e97846567f58870a0888f840129656a72bcab..e75d1005fb1b28520b57a007fac033f34018df6d 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -22,11 +22,14 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_explain.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
 using namespace CVC4;

diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h
index 16cd00cae5f0d02f35803df90ad50c403aeb9cce..c35fc86ff35b7e1c4a216080a07efec3aeda9bbd 100644 (file)
--- a/src/theory/datatypes/sygus_extension.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -22,20 +22,18 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
-#include "context/cdlist.h"
-#include "context/cdo.h"
 #include "context/context.h"
-#include "expr/dtype.h"
 #include "expr/node.h"
 #include "theory/datatypes/sygus_simple_sym.h"
 #include "theory/decision_manager.h"
-#include "theory/quantifiers/sygus/sygus_explain.h"
-#include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers/term_database.h"
 
 namespace CVC4 {
 namespace theory {
+namespace quantifiers {
+class SynthConjecture;
+}
 namespace datatypes {
 
 class InferenceManager;

diff --git a/src/theory/datatypes/sygus_simple_sym.h b/src/theory/datatypes/sygus_simple_sym.h
index f1a77910f3deb188992d26222827094b1f04b999..713d1bdc2b17585fb4cfc10c2e8229d7e2ed4c33 100644 (file)
--- a/src/theory/datatypes/sygus_simple_sym.h
+++ b/src/theory/datatypes/sygus_simple_sym.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
 #define CVC4__THEORY__DATATYPES__SIMPLE_SYM_BREAK_H
 
-#include <map>
 #include "expr/dtype.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index bb6a8479219978b2f3a76feaa975ac716866c8e2..e20e3db9bb4e8c4372bb57e488a20f47de3905a5 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -27,11 +27,15 @@
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/logic_info.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/theory_model.h"
+#include "theory/theory_state.h"
 #include "theory/type_enumerator.h"
 #include "theory/valuation.h"
 

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 27caad03c79bce0aa78d95426e0939a0df43ede8..95dccf2e5f09f3d4987cc8b23bf33f7eacf3690b 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -31,6 +31,7 @@
 #include "theory/datatypes/sygus_extension.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
+#include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"
 #include "util/hash.h"
 

diff --git a/src/theory/decision_strategy.h b/src/theory/decision_strategy.h
index ef0b6f09dd045f44404fcdc01a1a3e661d839ac0..74edde7f9da51be0d9883ade05e6160e01e092c1 100644 (file)
--- a/src/theory/decision_strategy.h
+++ b/src/theory/decision_strategy.h
@@ -18,7 +18,6 @@
 #ifndef CVC4__THEORY__DECISION_STRATEGY__H
 #define CVC4__THEORY__DECISION_STRATEGY__H
 
-#include <map>
 #include "context/cdo.h"
 #include "expr/node.h"
 #include "theory/valuation.h"

diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index 2a6d28d563fcf2e9ad6c836b7cdf06f8850e2b77..7bbdc91d3c7efd3f1ab56b57d3dbb5140fb9d5d0 100644 (file)
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -15,6 +15,7 @@
 #include "theory/eager_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {

diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h
index 3fd8118ede27ecfecab3fbacee1f7d838f4207ea..256dfeee94e38e4beeb29a155840f8f11251b614 100644 (file)
--- a/src/theory/eager_proof_generator.h
+++ b/src/theory/eager_proof_generator.h
@@ -20,10 +20,14 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 
 /**

diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp
index 0ba62065b339ed33b9079eb809d8bca05c3a5fa8..3757f153a2d8e738a1757cb24ee6aaf92f0560c8 100644 (file)
--- a/src/theory/ee_manager_distributed.cpp
+++ b/src/theory/ee_manager_distributed.cpp
@@ -17,6 +17,7 @@
 #include "theory/quantifiers_engine.h"
 #include "theory/shared_solver.h"
 #include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h
index 3ae1a90de5745f6656ffe5264def890128d5e629..26f3d943036ec0b4541b0a7dba4fcda8f30f756f 100644 (file)
--- a/src/theory/ee_manager_distributed.h
+++ b/src/theory/ee_manager_distributed.h
@@ -18,15 +18,17 @@
 #ifndef CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
 #define CVC4__THEORY__EE_MANAGER_DISTRIBUTED__H
 
-#include <map>
 #include <memory>
 
 #include "theory/ee_manager.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
+namespace eq {
+class EqualityEngine;
+}
+
 /**
  * The (distributed) equality engine manager. This encapsulates an architecture
  * in which all theories maintain their own copy of an equality engine.

diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index 3240ec77b8ace6f95ac550ced9f2e81a0752a9c3..0bdccab1b26b6e7f0b6536b71c987665e2efd344 100644 (file)
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 #include "theory/output_channel.h"
-#include "theory/theory.h"
+#include "theory/theory_id.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -28,6 +28,8 @@ class TheoryEngine;
 
 namespace theory {
 
+class Theory;
+
 /**
  * An output channel for Theory that passes messages back to a TheoryEngine
  * for a given Theory.

diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
index ae54a8d3b7ff257016ac7e91e3fe1db37ef4cd95..f2235c6bf414dece10e35d3fa834a15d4afd3b18 100644 (file)
--- a/src/theory/ext_theory.h
+++ b/src/theory/ext_theory.h
@@ -34,17 +34,18 @@
 #define CVC4__THEORY__EXT_THEORY_H
 
 #include <map>
-#include <set>
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
+#include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "theory/theory.h"
 
 namespace CVC4 {
 namespace theory {
 
+class OutputChannel;
+
 /**
  * A callback class for ExtTheory below. This class is responsible for
  * determining how to apply context-dependent simplification.

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 60d229215d017c3c62b5d551066120c378d93452..3590799483e61bad2068726b9538cad0b04c1fe1 100644 (file)
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -16,6 +16,8 @@
 
 #include <vector>
 
+#include "base/check.h"
+#include "expr/node_builder.h"
 #include "theory/theory.h"  // theory.h Only needed for the leaf test
 #include "util/floatingpoint.h"
 #include "util/floatingpoint_literal_symfpu.h"

diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 8f02cc115a24cb5575a857ee67337173b5fa2715..6623f308ca77fe39ac60d549c9103210e299da52 100644 (file)
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -23,11 +23,9 @@
 #ifndef CVC4__THEORY__FP__FP_CONVERTER_H
 #define CVC4__THEORY__FP__FP_CONVERTER_H
 
-#include "base/check.h"
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/node_builder.h"
 #include "expr/type_node.h"
 #include "theory/valuation.h"
 #include "util/bitvector.h"

diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h
index 5f6b9cf4d8248c3314dbf2e6f94c0256c62ed466..73f7a240493aab7c69c7a1843cf0a9820968935e 100644 (file)
--- a/src/theory/inference_id.h
+++ b/src/theory/inference_id.h
@@ -14,14 +14,11 @@
 
 #include "cvc4_private.h"
 
+#include <iosfwd>
+
 #ifndef CVC4__THEORY__INFERENCE_ID_H
 #define CVC4__THEORY__INFERENCE_ID_H
 
-#include <map>
-#include <vector>
-
-#include "util/safe_print.h"
-
 namespace CVC4 {
 namespace theory {
 

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index f1ef4e0966f0ba1d9cd4a7135772cd2b4f2d6604..2772385d2147f1d0329444338b40da9adf0f05a8 100644 (file)
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
 #define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
 
-#include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "theory/theory_inference.h"
 #include "theory/theory_inference_manager.h"

diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index f048e9e90c1d9def8310b0e76241eedbd3ae7709..fe6d1cf623a5346703c7ac37cec88b5ae079f541 100644 (file)
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -23,7 +23,8 @@
 
 #include <string>
 #include <vector>
-#include "expr/kind.h"
+
+#include "theory/theory_id.h"
 
 namespace CVC4 {
 

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index cecb4ccc55d835652666b44ee6f8547630cf660a..b9057604e92711df7a38c9c504e81ed35f45818a 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/first_order_model.h"
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/theory_engine.h"
 

diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h
index 69efe6e5fc5c0e71d2d413e615169cfa782b924a..1e4c390661eb82525be1f292308403b97f68313f 100644 (file)
--- a/src/theory/model_manager.h
+++ b/src/theory/model_manager.h
@@ -21,8 +21,6 @@
 
 #include "theory/ee_manager.h"
 #include "theory/logic_info.h"
-#include "theory/theory_model.h"
-#include "theory/theory_model_builder.h"
 
 namespace CVC4 {
 
@@ -30,6 +28,9 @@ class TheoryEngine;
 
 namespace theory {
 
+class TheoryEngineModelBuilder;
+class TheoryModel;
+
 /**
  * A base class for managing models. Its main feature is to implement a
  * buildModel command. Overall, its behavior is specific to the kind of equality

diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp
index 3177e16ffaebc2c3eb3caf5f0da1494355ef0e36..838cf0ad6b2d227843039157d193fb4ef3f38d50 100644 (file)
--- a/src/theory/model_manager_distributed.cpp
+++ b/src/theory/model_manager_distributed.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
+#include "theory/theory_model_builder.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h
index f8cbf23223b6473e48578dd8fe0951b4a20b7dd8..d41b6fa3b9047da9920a1ab04d8385816d641c50 100644 (file)
--- a/src/theory/model_manager_distributed.h
+++ b/src/theory/model_manager_distributed.h
@@ -17,8 +17,6 @@
 #ifndef CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
 #define CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
 
-#include <memory>
-
 #include "theory/ee_manager.h"
 #include "theory/model_manager.h"
 

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 0441b1126a57efee4d15648dac3cbf26d871f098..8c10a1348711d5d962e75e0f0c8fb8f15782c075 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -19,11 +19,6 @@
 #ifndef CVC4__THEORY__OUTPUT_CHANNEL_H
 #define CVC4__THEORY__OUTPUT_CHANNEL_H
 
-#include <memory>
-
-#include "expr/proof_node.h"
-#include "smt/logic_exception.h"
-#include "theory/interrupted.h"
 #include "theory/trust_node.h"
 #include "util/resource_manager.h"
 

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 7da13adcdb96da220663c4168d101b702965b3f3..ca1d43b2fd045aeb2cf41a54e48c4d7528b6ad0e 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -23,6 +23,7 @@
 #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/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index 5260b46904c169e24f6e4959db80d02118a05c45..a5fb33a1fcd104a06b3325e30158880e660e7493 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -17,10 +17,8 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
 #define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
 
-#include <map>
-#include <memory>
-#include <unordered_set>
 #include <vector>
+
 #include "theory/quantifiers/candidate_rewrite_filter.h"
 #include "theory/quantifiers/expr_miner.h"
 #include "theory/quantifiers/sygus_sampler.h"

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 7926116db9e8120820a6c7d2760679c7f1f7163f..94c8b87e627c283a8ee0add030e99b7084a113c1 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -22,6 +22,7 @@
 #include "theory/arith/theory_arith_private.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 using namespace std;

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 6f529ea831d1bef17be8b039e71082f45d416231..56bd14b333f590ee204b5ea267d8d7022444e349 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/term_database.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/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index dfc79d5a773a33cb2046eb67ecb7cd1cea88ecee..f1ed9fe00c06444ec0135be11070a5414804b672 100644 (file)
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 using namespace CVC4;

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 c6675745d1f43ed6695f94fa531a8bfa90b0b551..41f83269c29f54bdb9eb72e898d5daddfeac4daa 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/term_util.h"

diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 68f8e2e0db38c991b9f8ec97dccfa01f5dbbacde..91cb6e929dfa243938e7baf915fc570a9aa16950 100644 (file)
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -13,6 +13,7 @@
  **/
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/instantiate.h"

diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 153f2e6ba243d80796904ec405f0189330412bfa..ef9b8063f2ad82a0da812491b90bf6428ef26ef6 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 
 #include "expr/skolem_manager.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
@@ -23,12 +24,14 @@
 #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/inst_match.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"
+#include "theory/valuation.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 4211816b73fbf543f106455e969c0226bb8c20b1..892f453eac071ddd44b2cb9663aa0c3905069095 100644 (file)
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -17,17 +17,13 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 #define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
 
-#include <map>
-
 #include "expr/node.h"
-#include "options/quantifiers_options.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/valuation.h"
 
 namespace CVC4 {
 namespace theory {
 
 class QuantifiersEngine;
+class Valuation;
 
 namespace quantifiers {
 class QuantifiersState;
@@ -38,6 +34,7 @@ class QuantifiersRegistry;
 namespace inst {
 
 class IMGenerator;
+class InstMatch;
 class InstMatchGenerator;
 /** A collection of nodes representing a trigger.
 *

diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
index 57246202db185a635230cabd42f4f8e81e4c7979..910dbc79b140f6688c3cebe08624888b8992a015 100644 (file)
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
 #define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
 
-#include <map>
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 3e70e5e694a94cdbba2a978d7f49ccc67103dd94..2ecf3673f64402c2d78dbb63f8a1ddda0e8e12b8 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4;

diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 8b850302239323e9c59433c8021d106c19b93ef5..878b4ddd3230d3e53e19c92a838973a0fbed7f1d 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -19,6 +19,7 @@
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_rep_bound_ext.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/equality_engine.h"
 

diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 121708a3692e51483f3242ada61a3ff1678ebc81..578554d79b834ea1bd3a1f696c755b7b9f8461f6 100644 (file)
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -18,15 +18,15 @@
 #define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 
 #include "expr/node.h"
-#include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/theory_model_builder.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class FirstOrderModel;
+class QuantifiersState;
 
 class QModelBuilder : public TheoryEngineModelBuilder
 {

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index b91a816419b89daa0740021abfc0814f1b7f7237..92e5ec71b88612649822dd435f419008b246529c 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -17,15 +17,14 @@
 #ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H
 #define CVC4__INST_STRATEGY_ENUMERATIVE_H
 
-#include "context/context.h"
-#include "context/context_mm.h"
 #include "theory/quantifiers/quant_module.h"
-#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class RelevantDomain;
+
 /** Enumerative instantiation
  *
  * This class implements enumerative instantiation described

diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 8fbb58fe0dfb2089b8349ab2e79f4843978d43d4..f6fb9ed75c11fb62cdce1b5a116d8c9d959d7761 100644 (file)
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -14,12 +14,14 @@
 
 #include "theory/quantifiers/instantiate.h"
 
+#include "expr/lazy_proof.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"
 #include "proof/proof_manager.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -29,6 +31,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace CVC4::context;

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index a1e08e274251cc68ba9b678a403a97a70489420d..e55e677dfd04c2c30a65af67b9942ae23da17e7b 100644 (file)
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -20,7 +20,6 @@
 #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"
@@ -28,6 +27,9 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+class LazyCDProof;
+
 namespace theory {
 
 class QuantifiersEngine;

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index d233dac623059d9d435e76080c2d744c67991f13..17081bb7ba7796fcf92b50cdaf103bda3f5a27a7 100644 (file)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -28,6 +28,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;

diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 8b68457bbb7a416e6ed55686d1f51cbe69b9c265..0b1f18f5b74cfd7b9e8f35a6cebf6acaae426a9d 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 4c232ef78876e88d08c83dfc1bd7264532818a97..3e223fd7caeaefd06399bd36fd6980def6e1ed8b 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 
 #include "options/quantifiers_options.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
@@ -27,6 +28,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::kind;

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 5ac93d4369e27aa475f59cce7b17e3d5d42c6f0a..509e4905e0a2fde04ec1a469d842679b5b5d64a6 100644 (file)
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -29,6 +29,7 @@
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 7c1ed40eb5581114b3c3d0b8b32d2bee73f97281..56743e26435e9368a0409c71f2f01102e4dc78c5 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index e2573bb52a962968b1464015d149170054f7ec1f..3c6ab6bc1a59870ae8c58af143c9873f0e9ca27a 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/sygus/transition_inference.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 #include "util/random.h"
 

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 742b3a3d90f47e357d5699b1b066b1d45905b21c..fec15fdc65ee84c4d488f7db4477359cef1f0758 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/cegis_unif.h"
 
+#include "expr/sygus_datatype.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"

diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h
index d9ec52affda55b3ca2cc3dd9c1e1a88d5d436bb2..61c0327b7e84fe4cea2ad21953485e10cff559de 100644 (file)
--- a/src/theory/quantifiers/sygus/example_infer.h
+++ b/src/theory/quantifiers/sygus/example_infer.h
@@ -18,8 +18,6 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
 #define CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
 
-#include "context/cdhashmap.h"
-#include "theory/quantifiers/sygus/sygus_module.h"
 #include "theory/quantifiers/sygus/sygus_unif_io.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index b550c3550cce401c6bb08e065a2de8190f1b3196..4f870830e88473c943083515c7ec47e994e64835 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -18,8 +18,11 @@
 #include "expr/node_algorithm.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 4fe2b8afc945a36a38bcd2987e92983ee153896b..9025b1a519a4d72afb9288ff2d40978eabffc55c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -16,7 +16,9 @@
 
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
+#include "smt/logic_exception.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/sygus_invariance.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index bf6807151d591d7e348385c3f4b3470a57e32b5d..262062f148fa8b1f8d5178b4a7e36260727e226b 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -20,12 +20,14 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/quantifiers/sygus/sygus_invariance.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class SygusInvarianceTest;
+class TermDbSygus;
+
 /** Recursive term builder
  *
  * This is a utility used to generate variants

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 2782336681165db8d31f1bb0b26186d344a7627a..49c0f5f47bac88e8c7d03c29aeab776954712acc 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 #include "theory/strings/word.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 4dd85e0aca418a64dc6e9c3983c0367a3ea5c5e4..bb4bb6384833cd0cba4d4138690fe67af65bf8f8 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -19,7 +19,6 @@
 
 #include <map>
 #include <memory>
-#include <string>
 #include <vector>
 
 #include "expr/node.h"

diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index be6d4c7ebd7da4a46b028bf9700cb983c268f2ed..1740ecc3d7dedf910df567fd7c03e503efbb56b8 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -17,6 +17,7 @@
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 using namespace std;

diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 4ef0f8f08dd8bfbc720174fe3188dcc1ca60777e..86d113edcf79ec87e813169e57c5e5f133b411f0 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
 
-#include <map>
 #include <vector>
 
 #include "expr/node.h"

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index aa2551251f6886ea06cdef9683e3db55cb393bb1..bc9da0c4d32b549b202f7f93254b061c875b8eec 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/example_infer.h"
+#include "theory/quantifiers/sygus/sygus_unif_io.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index 52e574d4975022766f4c16eb81a175b44c28b271..7b20df8de7554ae18b59b4458d30f45a2b73508c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -17,14 +17,13 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
 #define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
 
-#include "context/cdhashmap.h"
 #include "theory/quantifiers/sygus/sygus_module.h"
-#include "theory/quantifiers/sygus/sygus_unif_io.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class SygusUnifIo;
 class SynthConjecture;
 
 /** SygusPbe

diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 1123830f391fc0c4a882e807a12ce226b6258d98..3629164eec4144ee532a5baa7e218cbf4ecd5b2e 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -15,10 +15,7 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
 #define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
 
-#include <string>
-#include <vector>
 #include "expr/node.h"
-#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 1400882ebbe8096aa24798e83a0a1311fc761f33..0911b73c238a81d3a9892a93cf4a8813f4d95c5d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -24,6 +24,7 @@
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/logic_info.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index 30d04c8e2160cd949eb78a0854bc7300d924de84..319497f77e8cb068b6ffb97595e8b2af5717929e 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -19,16 +19,17 @@
 
 #include <unordered_set>
 #include "expr/node.h"
-#include "theory/logic_info.h"
 
 namespace CVC4 {
+
+class LogicInfo;
+
 namespace theory {
 
 class QuantifiersEngine;
 
 namespace quantifiers {
 
-class CegConjecture;
 class TermDbSygus;
 
 /** SygusRepairConst

diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index 2c0ac227b6ff404897afb2aa46d022da7efe7a97..a9891aa72312d50cef5c489c72c16b0d0317e80e 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/strings/word.h"
 #include "util/random.h"
 

diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 732b52bf94941b362b546c3408c746aafdf97f26..a3cf5ed19c6c9d5d172f509cc3e0ca8ee60e437c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -19,6 +19,7 @@
 #include "printer/printer.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 #include <math.h>

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 57043086b692855fd1993f4f8f1bf8c915cd557b..dc864fbd8a5e9659a3af2a8c9bfc37bdcc413d04 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -19,6 +19,7 @@
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -29,9 +30,12 @@
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
 #include "theory/quantifiers/sygus/synth_engine.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 47ebe685318b42bf8b01bde1d1f4db0192562304..27c565795df38d2cbfb894c621247af0377d2310 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -20,7 +20,6 @@
 
 #include <memory>
 
-#include "theory/decision_manager.h"
 #include "theory/quantifiers/expr_miner_manager.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus/cegis.h"
@@ -28,8 +27,6 @@
 #include "theory/quantifiers/sygus/cegis_unif.h"
 #include "theory/quantifiers/sygus/example_eval_cache.h"
 #include "theory/quantifiers/sygus/example_infer.h"
-#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
-#include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 #include "theory/quantifiers/sygus/sygus_stats.h"
@@ -39,6 +36,8 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class CegGrammarConstructor;
+class SygusPbe;
 class SygusStatistics;
 
 /**

diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index 0a50f90c7aee727fdabdf862d1f3bc844cbe00e7..543d5e7f055a880144d4aceb1e223ec359043283 100644 (file)
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index a8f247b58ee017d2b5f6a7a5d6a6123dfd89ee80..9266a3f9d201db9ccb75dbc1936a362b803caf4e 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -20,6 +20,7 @@
 #include "expr/sygus_datatype.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/sygus/type_node_id_trie.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h
index 43a6cd07ab8e6ba97bfba9d05900dd4d3b40c8fa..7b45d115b6d55952d55597a743d44654cb7de333 100644 (file)
--- a/src/theory/quantifiers/sygus/type_info.h
+++ b/src/theory/quantifiers/sygus/type_info.h
@@ -18,10 +18,8 @@
 #define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
 
 #include <map>
-#include <unordered_set>
 
 #include "expr/node.h"
-#include "theory/quantifiers/sygus/type_node_id_trie.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h
index 5625a8d1f8542efba3e937b3d2fb41ae12af1f7a..020c8d08656f4f2b0dc66f0d3dba7139db87c67a 100644 (file)
--- a/src/theory/quantifiers/sygus/type_node_id_trie.h
+++ b/src/theory/quantifiers/sygus/type_node_id_trie.h
@@ -26,8 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class TermDbSygus;
-
 /**
  * A trie indexed by types that assigns unique identifiers to nodes based on
  * a vector of types.

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index eeeb5385ed4bee667e0b2bb61f2ac8b34164a174..fa6d800851419cc314c01d70aa23482878bc230a 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 588201fbfa03ecaec869563cf11d61631066c115..61754ac328b7b3e4c43c2dc503da88056a706466 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -18,7 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
 #include <map>
-#include <unordered_set>
+#include <unordered_map>
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f72c970ba05aa32da6bddfa73709b98cb2f26e37..401857206974d80c69e1217232e698c6904e9f52 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -31,6 +31,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"

diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index 9b26c381794a81cdfcb0359796a503a71e877663..d38170563b910f9349eb49ef2c14f967808425d9 100644 (file)
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/relevance_manager.h"
 
+#include <sstream>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index fc1e7dffa82336784094176ff112dc3cc39e7f4e..5c3e2d38d2154cc8a59d065dd7b9f80a76ef6300 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -19,6 +19,7 @@
 #include "expr/node_algorithm.h"
 #include "options/sets_options.h"
 #include "smt/logic_exception.h"
+#include "theory/rewriter.h"
 #include "theory/sets/normal_form.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"

diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 8997d2b47a625fb74ddc882cb022d34e99382fc7..9e16bfb97f52f774f4c872b6f4fae9f8a7717b41 100644 (file)
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -15,6 +15,7 @@
 #include "theory/sets/inference_manager.h"
 
 #include "options/sets_options.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index e9529d4e01c2281419e7a4b356cd856d7f145d01..3937a32b673ece5f3532d630416b2e32ae503d4b 100644 (file)
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -21,6 +21,7 @@
 
 #include <memory>
 
+#include "smt/logic_exception.h"
 #include "theory/sets/inference_manager.h"
 #include "theory/sets/skolem_cache.h"
 #include "theory/sets/solver_state.h"

diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index fcdb7810f181f0a2e1ec447d08b26e7dde8ce956..91e008f80716ff4eb50f9bc721995c3db273a46c 100644 (file)
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -15,6 +15,8 @@
 #include "theory/shared_solver.h"
 
 #include "expr/node_visitor.h"
+#include "theory/ee_setup_info.h"
+#include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {

diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index d1c6f6c03a0e29a325b8a9f8cf6e7dd553ca3f2a..a4d08bd1bc1ddae1414f3cf02be214bc73bea556 100644 (file)
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -18,19 +18,20 @@
 #define CVC4__THEORY__SHARED_SOLVER__H
 
 #include "expr/node.h"
-#include "expr/proof_node_manager.h"
-#include "theory/ee_setup_info.h"
-#include "theory/logic_info.h"
 #include "theory/shared_terms_database.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
 
 namespace CVC4 {
 
+class LogicInfo;
+class ProofNodeManager;
 class TheoryEngine;
 
 namespace theory {
 
+struct EeSetupInfo;
+
 /**
  * A base class for shared solver. The shared solver is the component of theory
  * engine that behaves like a theory solver, and whose purpose is to ensure the

diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 9ad91ed33b764af284d11cd7a64fe837fe696f9a..cc99e75b47782184f18ab5488ec0c1a6c1247e43 100644 (file)
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -18,7 +18,6 @@
 #ifndef CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
 #define CVC4__THEORY__SMT_ENGINE_SUBSOLVER_H
 
-#include <map>
 #include <memory>
 #include <vector>
 

diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h
index c1e5b1fa802b38c09ba6594a07d440a5f1c51d10..822416da3978cc08e8ca3431faeae07c6c4bdd10 100644 (file)
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -17,10 +17,9 @@
 #ifndef CVC4__SORT_INFERENCE_H
 #define CVC4__SORT_INFERENCE_H
 
-#include <iostream>
-#include <string>
-#include <vector>
 #include <map>
+#include <vector>
+
 #include "expr/node.h"
 #include "expr/type_node.h"
 

diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index c6bdad898cc99d2bc71210560293d682dbfb0b6a..8a8abbf812334033d1d9e4d129c99aaba759bd5a 100644 (file)
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/sequence.h"
 #include "options/strings_options.h"
+#include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 5dab55e6556a13a24deb0e0c3704976812efa1e9..b746f2961b13b1ac374ad3c4def8eb0a9c93b9ba 100644 (file)
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -18,6 +18,8 @@
 
 #include "base/configuration.h"
 #include "options/strings_options.h"
+#include "smt/logic_exception.h"
+#include "theory/rewriter.h"
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/strings/strings_entail.h"
 #include "theory/strings/theory_strings_utils.h"

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index b6db6175fbfff6e03a6fd8bf8ffaddb9eab9fdd5..a02566a41691d38c32dcf8e97e72ce80eb7e4ac3 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/strings/infer_proof_cons.h"
 
+#include "expr/proof_node_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/smt_options.h"
 #include "options/strings_options.h"

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 0a938b23679484734908a922b3caa189e7f94de1..f252196d8c8aa8857e3f24c932df713ad25c54f4 100644 (file)
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -19,6 +19,7 @@
 #include <cmath>
 
 #include "options/strings_options.h"
+#include "smt/logic_exception.h"
 #include "theory/ext_theory.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/theory_model.h"

diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 1fd0169b0edf077e09ac6ce4d3740c034e952b8c..456cd492b2b6e27201965814cdbda5f6b2cc1f49 100644 (file)
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/strings/solver_state.h"
 
+#include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/word.h"
 

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 9ea9042cd30d751e4153d75e8f1962f3a7d25208..3a3003ba9ca0d2c803a284a38e37e146cf5855ec 100644 (file)
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -17,6 +17,7 @@
 
 #include "base/configuration.h"
 #include "options/quantifiers_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::theory;

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8a5c40fd84a96942cd014447a8b611716a976105..f34aebe8bccc263c4927898e9e30955d69d1e49e 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -32,12 +32,14 @@
 #include "prop/prop_engine.h"
 #include "smt/dump.h"
 #include "smt/logic_exception.h"
+#include "smt/output_manager.h"
 #include "theory/combination_care_graph.h"
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/relevance_manager.h"
 #include "theory/rewriter.h"
+#include "theory/shared_solver.h"
 #include "theory/theory.h"
 #include "theory/theory_engine_proof_generator.h"
 #include "theory/theory_id.h"
@@ -48,7 +50,6 @@
 
 using namespace std;
 
-using namespace CVC4::preprocessing;
 using namespace CVC4::theory;
 
 namespace CVC4 {

diff --git a/src/theory/theory_id.h b/src/theory/theory_id.h
index 96ac5bef011f44a2581940ee317356a1cd1e3d54..1833f1cace1a30610930525bdb76d79d91a7a573 100644 (file)
--- a/src/theory/theory_id.h
+++ b/src/theory/theory_id.h
@@ -20,7 +20,7 @@
 #ifndef CVC4__THEORY__THEORY_ID_H
 #define CVC4__THEORY__THEORY_ID_H
 
-#include <iostream>
+#include <iosfwd>
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index f970ce41e1248e9e73f1ff310f9e9fb33ef3aa19..68f70b740f6ebf70fcca0210a078a40eb7a037d3 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -16,6 +16,7 @@
 
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
+#include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_state.h"
 #include "theory/uf/equality_engine.h"

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 6e9622e2397afde5e1681d069a266b083be631e7..a599afa23ca00eac895f2827a70825f227410b88 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -21,6 +21,7 @@
 
 #include "context/cdhashset.h"
 #include "expr/node.h"
+#include "expr/proof_rule.h"
 #include "theory/inference_id.h"
 #include "theory/output_channel.h"
 #include "theory/trust_node.h"

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 10eb789b207f04abe90c5b505b6553b2b7c2c292..0c1ea7a7a5ef614481b65341cbe99d439a2e1a0a 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -19,6 +19,7 @@
 #include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_engine.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 73b1d1d800d133bc70669343d3f02fb61c7af2d1..0d83fa42d569d84c223e4b22987e8fa18f37fdae 100644 (file)
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -19,6 +19,7 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "theory/rewriter.h"
 #include "theory/uf/theory_uf_model.h"
 
 using namespace std;

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index 6d76968adbb42cd6098665bdf31484a227bbd924..51f2155d3e7ac322a2612485849699b4d2e7f21e 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/lazy_proof.h"
 #include "expr/skolem_manager.h"
+#include "smt/logic_exception.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 810987a0cefe8d6052a1c8038fcf2391a94ee0c2..d61f2d15be1c9d8c378aef2dc5b287f17da62571 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -18,6 +18,8 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"

diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h
index 91653785fad24b663ccb504ab2b643de72f90602..d701adfc48f3924cd08d9074393f5a2acdf6e956 100644 (file)
--- a/src/theory/uf/cardinality_extension.h
+++ b/src/theory/uf/cardinality_extension.h
@@ -19,11 +19,10 @@
 
 #include "context/cdhashmap.h"
 #include "context/context.h"
+#include "theory/decision_strategy.h"
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
 
-#include "theory/decision_manager.h"
-
 namespace CVC4 {
 namespace theory {
 namespace uf {

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index bfcb829ff26c06879109b2b785d64df3e05dea47..59dc3943d2f03547ee3d0cd3126bc1cda6fa1007 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -17,9 +17,12 @@
 
 #include "theory/uf/equality_engine.h"
 
+#include "base/output.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/rewriter.h"
+#include "theory/uf/eq_proof.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 7e297134e9ea81741ad7dacda5e52a10954b788c..b81a17dcfd3b7f5525726cc7267390bb50893503 100644 (file)
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -22,18 +22,14 @@
 
 #include <deque>
 #include <queue>
-#include <memory>
 #include <unordered_map>
 #include <vector>
 
-#include "base/output.h"
 #include "context/cdhashmap.h"
 #include "context/cdo.h"
 #include "expr/kind_map.h"
 #include "expr/node.h"
-#include "theory/rewriter.h"
 #include "theory/theory_id.h"
-#include "theory/uf/eq_proof.h"
 #include "theory/uf/equality_engine_iterator.h"
 #include "theory/uf/equality_engine_notify.h"
 #include "theory/uf/equality_engine_types.h"
@@ -45,6 +41,7 @@ namespace eq {
 
 class EqClassesIterator;
 class EqClassIterator;
+class EqProof;
 
 /**
  * Class for keeping an incremental congruence closure over a set of terms. It provides

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 0a7418e8dbfda28227a75ad99a7311eef7008c8d..7db887b56d283cd76f82edd969167adbb8dd2cc7 100644 (file)
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -15,7 +15,11 @@
 #include "theory/uf/proof_equality_engine.h"
 
 #include "expr/lazy_proof_chain.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
 #include "theory/rewriter.h"
+#include "theory/uf/eq_proof.h"
+#include "theory/uf/equality_engine.h"
 #include "theory/uf/proof_checker.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 1ce623683c8ffa1623b0a2ce7849a98ff089807e..adf8d2c18601d1c31380710442a22194fdf8b641 100644 (file)
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
 #define CVC4__THEORY__UF__PROOF_EQUALITY_ENGINE_H
 
-#include <map>
 #include <vector>
 
 #include "context/cdhashmap.h"
@@ -25,15 +24,18 @@
 #include "expr/buffered_proof_generator.h"
 #include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 #include "theory/eager_proof_generator.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
+
+class ProofNode;
+class ProofNodeManager;
+
 namespace theory {
 namespace eq {
 
+class EqualityEngine;
+
 /**
  * A layer on top of an EqualityEngine. The goal of this class is manage the
  * use of an EqualityEngine object in such a way that the proper proofs are

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index caa15e69e35902f439b070ffccaf7fc5b39ff464..273e81740667fca026407dfacd69bdfe39a0b406 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -26,6 +26,7 @@
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "smt/logic_exception.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/uf/cardinality_extension.h"

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 7f136f9c1a554f6e00fe9c5eb2bb1319282864ff..be63be373ba9ee38812b5025fc1e7f63350fdfcd 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -20,15 +20,12 @@
 #ifndef CVC4__THEORY__UF__THEORY_UF_H
 #define CVC4__THEORY__UF__THEORY_UF_H
 
-#include "context/cdo.h"
 #include "expr/node.h"
 #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"
 #include "theory/uf/symmetry_breaker.h"
 #include "theory/uf/theory_uf_rewriter.h"
 

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 3613a9b22bb709a2b00c4eb3458b0b18ed13a102..393f1f705b9311bce5ccc51e292242d5a1d37eac 100644 (file)
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -18,6 +18,8 @@
 
 #include "expr/attribute.h"
 #include "theory/quantifiers/first_order_model.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 3c5cc681b50bb1c96a310aed876bceca24ce8565..62ec8204fe89fb7396dd5858e7818bb284122082 100644 (file)
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -20,10 +20,12 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
 namespace theory {
+
+class TheoryModel;
+
 namespace uf {
 
 class UfModelTreeNode

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 54b71f9f88ae6bdbfece19643a498144c2da8e64..e46f38a28bee79ebb2e53d8893a24cc97c55dbb0 100644 (file)
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -19,6 +19,7 @@
 #include "expr/node.h"
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
+#include "theory/assertion.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 840da860f2294830dc960534902098397fcb7cb2..860517451eb74a5807ca58bdd6671d0812927292 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -24,7 +24,6 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "options/theory_options.h"
-#include "theory/assertion.h"
 
 namespace CVC4 {
 
@@ -32,6 +31,7 @@ class TheoryEngine;
 
 namespace theory {
 
+struct Assertion;
 class TheoryModel;
 class SortInference;