More cleanup of includes to reduce compilation times (#6037)

Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index cddef79fd1f10a3136029aac6c3584f814da71ae..ad50ec35129aa91b51cfedcf57763dd4f18e64ad 100644 (file)
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -20,6 +20,7 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cstring>
+#include <sstream>
 #include <string>
 
 #include "base/check.h"
@@ -28,6 +29,13 @@ using namespace std;
 
 namespace CVC4 {
 
+std::string Exception::toString() const
+{
+  std::stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
 thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr;
 
 LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {}

diff --git a/src/base/exception.h b/src/base/exception.h
index 8a89c99fcf9755fdbfc2aeb016c773f320c60b70..815e4011f09db670dc6d0ed6d5a1aa9ebbb936d6 100644 (file)
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -19,12 +19,8 @@
 #ifndef CVC4__EXCEPTION_H
 #define CVC4__EXCEPTION_H
 
-#include <cstdarg>
-#include <cstdlib>
 #include <exception>
 #include <iosfwd>
-#include <sstream>
-#include <stdexcept>
 #include <string>
 
 namespace CVC4 {
@@ -61,12 +57,7 @@ class CVC4_PUBLIC Exception : public std::exception {
    * toString(), there is no stream, so the parameters are default
    * and you'll get exprs and types printed using the AST language.
    */
-  std::string toString() const
-  {
-    std::stringstream ss;
-    toStream(ss);
-    return ss.str();
-  }
+  std::string toString() const;
 
   /**
    * Printing: feel free to redefine toStream().  When overridden in

diff --git a/src/base/listener.cpp b/src/base/listener.cpp
index 72f9ee0868260b01f11d0cb727c3c04e7c4f93e2..6e9d659fd2e10e3dcf669aafb5b34fed10f4a68a 100644 (file)
--- a/src/base/listener.cpp
+++ b/src/base/listener.cpp
@@ -16,10 +16,6 @@
 
 #include "base/listener.h"
 
-#include <list>
-
-#include "base/check.h"
-
 namespace CVC4 {
 
 Listener::Listener(){}

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index e1327c0a7550c443395b6699d4583519793fcc6c..2cebfa44745480ae3829e23afa8b88084736cd31 100644 (file)
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -20,6 +20,7 @@
 #include "expr/node.h"
 #include "options/decision_options.h"
 #include "options/smt_options.h"
+#include "util/resource_manager.h"
 
 using namespace std;
 

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 914636fe9c46dabc1d03a28e6fc323787dcbbf8c..74a230e298bb5a3df9fc66f46c6348edf9bc6c64 100644 (file)
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -19,18 +19,15 @@
 #ifndef CVC4__DECISION__DECISION_ENGINE_H
 #define CVC4__DECISION__DECISION_ENGINE_H
 
-#include <vector>
-
 #include "base/output.h"
+#include "context/cdo.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
 #include "prop/cnf_stream.h"
-#include "prop/prop_engine.h"
+#include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/term_formula_removal.h"
+#include "util/result.h"
 
-using namespace std;
 using namespace CVC4::prop;
 using namespace CVC4::decision;
 

diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 1d0b386e3b6bff3c16192dea28ad85a8e7c8d55b..4950f4f3d0acd5c09d5ba57fa198477d165e459b 100644 (file)
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -18,15 +18,18 @@
  **/
 #include "justification_heuristic.h"
 
+#include "decision/decision_attributes.h"
+#include "decision/decision_engine.h"
 #include "expr/kind.h"
 #include "expr/node_manager.h"
 #include "options/decision_options.h"
-#include "theory/rewriter.h"
-#include "smt/term_formula_removal.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/term_formula_removal.h"
+#include "theory/rewriter.h"
 #include "util/random.h"
 
 namespace CVC4 {
+namespace decision {
 
 JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
                                                context::UserContext* uc,
@@ -67,8 +70,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch)
 {
   if(options::decisionThreshold() > 0) {
     bool stopSearchTmp = false;
-    SatLiteral lit = getNextThresh(stopSearchTmp, options::decisionThreshold());
-    if(lit != undefSatLiteral) {
+    prop::SatLiteral lit =
+        getNextThresh(stopSearchTmp, options::decisionThreshold());
+    if (lit != prop::undefSatLiteral)
+    {
       Assert(stopSearchTmp == false);
       return lit;
     }
@@ -88,9 +93,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
     for(JustifiedSet::key_iterator i = d_justified.key_begin();
         i != d_justified.key_end(); ++i) {
       TNode n = *i;
-      SatLiteral l = d_decisionEngine->hasSatLiteral(n) ?
-        d_decisionEngine->getSatLiteral(n) : -1;
-      SatValue v = tryGetSatValue(n);
+      prop::SatLiteral l = d_decisionEngine->hasSatLiteral(n)
+                               ? d_decisionEngine->getSatLiteral(n)
+                               : -1;
+      prop::SatValue v = tryGetSatValue(n);
       Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
     }
   }
@@ -102,12 +108,13 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
     // Commenting out. See bug 374. In short, to do with how CNF stream works.
     // Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
 
-    SatValue desiredVal = SAT_VALUE_TRUE;
-    SatLiteral litDecision;
+    prop::SatValue desiredVal = prop::SAT_VALUE_TRUE;
+    prop::SatLiteral litDecision;
 
     litDecision = findSplitter(d_assertions[i], desiredVal);
 
-    if(litDecision != undefSatLiteral) {
+    if (litDecision != prop::undefSatLiteral)
+    {
       setPrvsIndex(i);
       Trace("decision") << "jh: splitting on " << litDecision << std::endl;
       ++d_helpfulness;
@@ -136,25 +143,26 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
 
   // SAT solver can stop...
   stopSearch = true;
-  if(d_curThreshold == 0)
-    d_decisionEngine->setResult(SAT_VALUE_TRUE);
+  if (d_curThreshold == 0) d_decisionEngine->setResult(prop::SAT_VALUE_TRUE);
   return prop::undefSatLiteral;
 }
 
-
-inline void computeXorIffDesiredValues
-(Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2)
+inline void computeXorIffDesiredValues(Kind k,
+                                       prop::SatValue desiredVal,
+                                       prop::SatValue& desiredVal1,
+                                       prop::SatValue& desiredVal2)
 {
   Assert(k == kind::EQUAL || k == kind::XOR);
 
   bool shouldInvert =
-    (desiredVal == SAT_VALUE_TRUE && k == kind::EQUAL) ||
-    (desiredVal == SAT_VALUE_FALSE && k == kind::XOR);
+      (desiredVal == prop::SAT_VALUE_TRUE && k == kind::EQUAL)
+      || (desiredVal == prop::SAT_VALUE_FALSE && k == kind::XOR);
 
-  if(desiredVal1 == SAT_VALUE_UNKNOWN &&
-     desiredVal2 == SAT_VALUE_UNKNOWN) {
+  if (desiredVal1 == prop::SAT_VALUE_UNKNOWN
+      && desiredVal2 == prop::SAT_VALUE_UNKNOWN)
+  {
     // CHOICE: pick one of them arbitarily
-    desiredVal1 = SAT_VALUE_FALSE;
+    desiredVal1 = prop::SAT_VALUE_FALSE;
   }
 
   if(desiredVal2 == SAT_VALUE_UNKNOWN) {
@@ -214,9 +222,9 @@ bool JustificationHeuristic::checkJustified(TNode n)
 
 DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n)
 {
-  return
-    d_exploredThreshold.find(n) == d_exploredThreshold.end() ?
-    numeric_limits<DecisionWeight>::max() : d_exploredThreshold[n];
+  return d_exploredThreshold.find(n) == d_exploredThreshold.end()
+             ? std::numeric_limits<DecisionWeight>::max()
+             : d_exploredThreshold[n];
 }
 
 void JustificationHeuristic::setExploredThreshold(TNode n)
@@ -263,36 +271,36 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity
     } else {
 
       if(k == kind::OR) {
-        dW1 = numeric_limits<DecisionWeight>::max(), dW2 = 0;
+        dW1 = std::numeric_limits<DecisionWeight>::max(), dW2 = 0;
         for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
-          dW1 = min(dW1, getWeightPolarized(*i, true));
-          dW2 = max(dW2, getWeightPolarized(*i, false));
+          dW1 = std::min(dW1, getWeightPolarized(*i, true));
+          dW2 = std::max(dW2, getWeightPolarized(*i, false));
         }
       } else if(k == kind::AND) {
-        dW1 = 0, dW2 = numeric_limits<DecisionWeight>::max();
+        dW1 = 0, dW2 = std::numeric_limits<DecisionWeight>::max();
         for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
-          dW1 = max(dW1, getWeightPolarized(*i, true));
-          dW2 = min(dW2, getWeightPolarized(*i, false));
+          dW1 = std::max(dW1, getWeightPolarized(*i, true));
+          dW2 = std::min(dW2, getWeightPolarized(*i, false));
         }
       } else if(k == kind::IMPLIES) {
-        dW1 = min(getWeightPolarized(n[0], false),
-                  getWeightPolarized(n[1], true));
-        dW2 = max(getWeightPolarized(n[0], true),
-                  getWeightPolarized(n[1], false));
+        dW1 = std::min(getWeightPolarized(n[0], false),
+                       getWeightPolarized(n[1], true));
+        dW2 = std::max(getWeightPolarized(n[0], true),
+                       getWeightPolarized(n[1], false));
       } else if(k == kind::NOT) {
         dW1 = getWeightPolarized(n[0], false);
         dW2 = getWeightPolarized(n[0], true);
       } else {
         dW1 = 0;
         for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
-          dW1 = max(dW1, getWeightPolarized(*i, true));
-          dW1 = max(dW1, getWeightPolarized(*i, false));
+          dW1 = std::max(dW1, getWeightPolarized(*i, true));
+          dW1 = std::max(dW1, getWeightPolarized(*i, false));
         }
         dW2 = dW1;
       }
 
     }
-    d_weightCache[n] = make_pair(dW1, dW2);
+    d_weightCache[n] = std::make_pair(dW1, dW2);
   }
   return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second;
 }
@@ -315,7 +323,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
     {
       DecisionWeight dW = 0;
       for (TNode::iterator i = n.begin(); i != n.end(); ++i)
-        dW = max(dW, getWeight(*i));
+        dW = std::max(dW, getWeight(*i));
       n.setAttribute(DecisionWeightAttr(), dW);
     }
     else if (combiningFn == options::DecisionWeightInternal::SUM
@@ -323,7 +331,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
     {
       DecisionWeight dW = 0;
       for (TNode::iterator i = n.begin(); i != n.end(); ++i)
-        dW = max(dW, getWeight(*i));
+        dW = std::max(dW, getWeight(*i));
       n.setAttribute(DecisionWeightAttr(), dW);
     }
     else
@@ -334,7 +342,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) {
   return n.getAttribute(DecisionWeightAttr());
 }
 
-typedef vector<TNode> ChildList;
+typedef std::vector<TNode> ChildList;
 TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) {
   if(options::decisionUseWeight()) {
     // TODO: Optimize storing & access
@@ -389,7 +397,7 @@ void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l)
     SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]);
     if (it2 != d_skolemAssertions.end())
     {
-      l.push_back(make_pair(n[i], (*it2).second));
+      l.push_back(std::make_pair(n[i], (*it2).second));
       Assert(n[i].getNumChildren() == 0);
     }
     if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end())
@@ -610,8 +618,8 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TN
 {
   if(options::decisionUseWeight() &&
      getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
-    swap(node1, node2);
-    swap(desiredVal1, desiredVal2);
+    std::swap(node1, node2);
+    std::swap(desiredVal1, desiredVal2);
   }
 
   if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) {
@@ -635,8 +643,8 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TN
 {
   if(options::decisionUseWeight() &&
      getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
-    swap(node1, node2);
-    swap(desiredVal1, desiredVal2);
+    std::swap(node1, node2);
+    std::swap(desiredVal1, desiredVal2);
   }
 
   bool noSplitter = true;
@@ -722,4 +730,5 @@ JustificationHeuristic::handleEmbeddedSkolems(TNode node)
   return noSplitter ? NO_SPLITTER : DONT_KNOW;
 }
 
-} /* namespace CVC4 */
+} /* namespace decision */
+} /* namespace CVC4 */
\ No newline at end of file

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 0a16759e1ee6cc7a70e872a39d64237fc939d9b1..1cf2810fdb79d8d7fbee137fe0b3d24a735789bc 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -24,16 +24,17 @@
 #define CVC4__DECISION__JUSTIFICATION_HEURISTIC
 
 #include <unordered_set>
+#include <utility>
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
-#include "decision/decision_attributes.h"
-#include "decision/decision_engine.h"
+#include "context/cdo.h"
 #include "decision/decision_strategy.h"
 #include "expr/node.h"
-#include "preprocessing/assertion_pipeline.h"
+#include "options/decision_weight.h"
 #include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace decision {
@@ -42,12 +43,17 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   //                   TRUE           FALSE         MEH
   enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW};
 
-  typedef std::vector<pair<TNode, TNode> > SkolemList;
+  typedef std::vector<std::pair<TNode, TNode> > SkolemList;
   typedef context::CDHashMap<TNode, SkolemList, TNodeHashFunction> SkolemCache;
   typedef std::vector<TNode> ChildList;
-  typedef context::CDHashMap<TNode,pair<ChildList,ChildList>,TNodeHashFunction> ChildCache;
+  typedef context::
+      CDHashMap<TNode, std::pair<ChildList, ChildList>, TNodeHashFunction>
+          ChildCache;
   typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap;
-  typedef context::CDHashMap<TNode,pair<DecisionWeight,DecisionWeight>,TNodeHashFunction> WeightCache;
+  typedef context::CDHashMap<TNode,
+                             std::pair<DecisionWeight, DecisionWeight>,
+                             TNodeHashFunction>
+      WeightCache;
 
   // being 'justified' is monotonic with respect to decisions
   typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet;
@@ -91,7 +97,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   std::unordered_set<TNode, TNodeHashFunction> d_visitedComputeSkolems;
 
   /** current decision for the recursive call */
-  SatLiteral d_curDecision;
+  prop::SatLiteral d_curDecision;
   /** current threshold for the recursive call */
   DecisionWeight d_curThreshold;
 
@@ -136,12 +142,12 @@ public:
   /* getNext with an option to specify threshold */
   prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
 
-  SatLiteral findSplitter(TNode node, SatValue desiredVal);
+  prop::SatLiteral findSplitter(TNode node, prop::SatValue desiredVal);
 
   /**
    * Do all the hard work.
    */
-  SearchResult findSplitterRec(TNode node, SatValue value);
+  SearchResult findSplitterRec(TNode node, prop::SatValue value);
 
   /* Helper functions */
   void setJustified(TNode);
@@ -151,7 +157,7 @@ public:
   void setPrvsIndex(int);
   int  getPrvsIndex();
   DecisionWeight getWeightPolarized(TNode n, bool polarity);
-  DecisionWeight getWeightPolarized(TNode n, SatValue);
+  DecisionWeight getWeightPolarized(TNode n, prop::SatValue);
   static DecisionWeight getWeight(TNode);
   bool compareByWeightFalse(TNode, TNode);
   bool compareByWeightTrue(TNode, TNode);
@@ -159,7 +165,7 @@ public:
 
   /* If literal exists corresponding to the node return
      that. Otherwise an UNKNOWN */
-  SatValue tryGetSatValue(Node n);
+  prop::SatValue tryGetSatValue(Node n);
 
   /* Get list of all term-ITEs for the atomic formula v */
   JustificationHeuristic::SkolemList getSkolems(TNode n);
@@ -176,13 +182,17 @@ public:
   /* Compute all term-removal skolems in a node recursively */
   void computeSkolems(TNode n, SkolemList& l);
 
-  SearchResult handleAndOrEasy(TNode node, SatValue desiredVal);
-  SearchResult handleAndOrHard(TNode node, SatValue desiredVal);
-  SearchResult handleBinaryEasy(TNode node1, SatValue desiredVal1,
-                        TNode node2, SatValue desiredVal2);
-  SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1,
-                        TNode node2, SatValue desiredVal2);
-  SearchResult handleITE(TNode node, SatValue desiredVal);
+  SearchResult handleAndOrEasy(TNode node, prop::SatValue desiredVal);
+  SearchResult handleAndOrHard(TNode node, prop::SatValue desiredVal);
+  SearchResult handleBinaryEasy(TNode node1,
+                                prop::SatValue desiredVal1,
+                                TNode node2,
+                                prop::SatValue desiredVal2);
+  SearchResult handleBinaryHard(TNode node1,
+                                prop::SatValue desiredVal1,
+                                TNode node2,
+                                prop::SatValue desiredVal2);
+  SearchResult handleITE(TNode node, prop::SatValue desiredVal);
   SearchResult handleEmbeddedSkolems(TNode node);
 };/* class JustificationHeuristic */
 

diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index da80891a299cff992c7d7d37e66bfea9b90db545..15ae6ea8373c3b170e4024760de9666d4c903821 100644 (file)
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -19,11 +19,11 @@
 
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
 class ProofNodeManager;
+class ProofStep;
 
 /**
  * The proof generator for buffered steps. This class is a context-dependent

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index f94f0063a185792a27feacc16610b8aa7fe36bd1..5451edc02652a6f2ddd7ba349519342e371e93f2 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -13,6 +13,8 @@
  **/
 #include "expr/dtype.h"
 
+#include <sstream>
+
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/type_matcher.h"

diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index 0bda68b7b34571d682d55a60118494516fd0f2c6..e82e614b379d2c5f0195fa508a4e3ee0392e8729 100644 (file)
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -15,6 +15,8 @@
  ** \todo document this file
  **/
 
+#include <sstream>
+
 #include "expr/kind.h"
 
 namespace CVC4 {

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

diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 83dc90e4d90ce4f21dc837be60727f4db827ce57..7c39164fea7b509e9d814bd1b2f61592b9235c42 100644 (file)
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -17,14 +17,11 @@
 #ifndef CVC4__EXPR__LAZY_PROOF_H
 #define CVC4__EXPR__LAZY_PROOF_H
 
-#include <unordered_map>
-#include <vector>
-
 #include "expr/proof.h"
-#include "expr/proof_generator.h"
 
 namespace CVC4 {
 
+class ProofGenerator;
 class ProofNodeManager;
 
 /**

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index f80ab099c91b49bd87e5a677a3ad117b7114d639..0e5e8c3762244f5ca71f1fea50641c5f16f7d1f0 100644 (file)
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/proof.h"
 #include "expr/proof_ensure_closed.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "expr/proof_node_manager.h"
 #include "options/proof_options.h"

diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 1604bf18223bac2307687371352d8cef9e5a716a..e1b0f3cd0bd9ccab0c00fbee3b9832b55c462b54 100644 (file)
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H
 #define CVC4__EXPR__LAZY_PROOF_CHAIN_H
 
-#include <unordered_map>
 #include <vector>
 
 #include "context/cdhashmap.h"

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 1aca73d2eab83ea944873a5ebf63a74353a6037e..eee8d01363b0b5059a1b4469e31d6914dd928723 100644 (file)
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -15,8 +15,9 @@
  **/
 #include "expr/node.h"
 
-#include <iostream>
 #include <cstring>
+#include <iostream>
+#include <sstream>
 
 #include "base/exception.h"
 #include "base/output.h"

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

diff --git a/src/expr/proof.h b/src/expr/proof.h
index 3a26f097532a088b7e3d47e0818838c3faea92a7..abb0b9b37c63b3e108032fc8bf5d4845e976f62e 100644 (file)
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -17,17 +17,16 @@
 #ifndef CVC4__EXPR__PROOF_H
 #define CVC4__EXPR__PROOF_H
 
-#include <map>
 #include <vector>
 
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node.h"
 #include "expr/proof_step_buffer.h"
 
 namespace CVC4 {
 
+class ProofNode;
 class ProofNodeManager;
 
 /**

diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index dc87d1795bba00480e3ad190ae1ad2a89dcab042..a5655c9dbd0b3f8f0ec491edcd70d675f0586385 100644 (file)
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -14,6 +14,7 @@
 
 #include "expr/proof_checker.h"
 
+#include "expr/proof_node.h"
 #include "expr/skolem_manager.h"
 #include "options/proof_options.h"
 #include "smt/smt_statistics_registry.h"

diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index ab9c244348532b9299cdac4c7801b4b5fef27b1b..200a1839dfe57d28621f6ab1fd96b65dde605d3c 100644 (file)
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -20,12 +20,13 @@
 #include <map>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 
 class ProofChecker;
+class ProofNode;
 
 /** A virtual base class for checking a proof rule */
 class ProofRuleChecker

diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
index 6eebcd3ec2777abc28e5c959a111e2c9364a6435..183ff0d5bac2f41fb71d20adc2ad7ee397f0f8de 100644 (file)
--- a/src/expr/proof_ensure_closed.cpp
+++ b/src/expr/proof_ensure_closed.cpp
@@ -14,6 +14,10 @@
 
 #include "expr/proof_ensure_closed.h"
 
+#include <sstream>
+
+#include "expr/proof_generator.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "options/proof_options.h"
 #include "options/smt_options.h"

diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index 7b970a71adea4a11b78b42427705d2defe541325..c54a5dfd51364779f9bdb9b10cfcbd10a69492aa 100644 (file)
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -18,11 +18,12 @@
 #define CVC4__EXPR__PROOF_ENSURE_CLOSED_H
 
 #include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 
+class ProofGenerator;
+class ProofNode;
+
 /**
  * Debug check closed on Trace c. Context ctx is string for debugging.
  * This method throws an assertion failure if pg cannot provide a closed

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index d2206a5706d897345f152322420f1805daf543f8..31af09b7f5b7d85f4a88567ef7dd4e2ffa7c03c7 100644 (file)
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -14,7 +14,10 @@
 
 #include "expr/proof_generator.h"
 
+#include <sstream>
+
 #include "expr/proof.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "options/smt_options.h"
 

diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 869f226b8e6c7508d2b266a6b95b896186a1aa72..3b376d77c2891a86e768470e296f038f64dd5b09 100644 (file)
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -18,11 +18,11 @@
 #define CVC4__EXPR__PROOF_GENERATOR_H
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
 
 class CDProof;
+class ProofNode;
 
 /** An overwrite policy for CDProof */
 enum class CDPOverwrite : uint32_t

diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 2af2968130ef5eb1d76a18dbee1925cd37aaf258..751dcc39eae739a0689fd17772f187ddf5f6fa43 100644 (file)
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof_node_algorithm.h"
 
+#include "expr/proof_node.h"
+
 namespace CVC4 {
 namespace expr {
 

diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index 43d06ea919e20223458946c761dcd813db8222da..af8de066d7be37be44d12322c835708dc3cbaedf 100644 (file)
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -20,9 +20,11 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
 
 namespace CVC4 {
+
+class ProofNode;
+
 namespace expr {
 
 /**

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index f5e15f6d6aaff2a2fffbfad9596e258bbbba1786..91858f239c05461030c1af608492c3b64b0fabf4 100644 (file)
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -15,6 +15,8 @@
 #include "expr/proof_node_manager.h"
 
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_algorithm.h"
 #include "options/proof_options.h"
 #include "theory/rewriter.h"

diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 3ad56c92decfffb4033e1bdc659fd8406170bd2f..e7be500656685ed74d61b2ecb2ed2c3e0aea7167 100644 (file)
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -19,11 +19,14 @@
 
 #include <vector>
 
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
+#include "expr/node.h"
+#include "expr/proof_rule.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+class ProofNode;
+
 /**
  * A manager for proof node objects. This is a trusted interface for creating
  * and updating ProofNode objects.

diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index fbfc3e3d41d970b66654e7000af3a11c2129728c..6830326ba745d9c3b17f78a9c0412e3f15151779 100644 (file)
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -15,7 +15,9 @@
 #include "expr/proof_node_to_sexpr.h"
 
 #include <iostream>
+#include <sstream>
 
+#include "expr/proof_node.h"
 #include "options/proof_options.h"
 
 using namespace CVC4::kind;

diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
index 3e0d42a7d62afe0cd236edf992aff4019a278777..e6c003d100b314f4f4dc23c7e953c2e768c88816 100644 (file)
--- a/src/expr/proof_node_to_sexpr.h
+++ b/src/expr/proof_node_to_sexpr.h
@@ -20,10 +20,12 @@
 #include <map>
 
 #include "expr/node.h"
-#include "expr/proof_node.h"
+#include "expr/proof_rule.h"
 
 namespace CVC4 {
 
+class ProofNode;
+
 /** A class to convert ProofNode objects to s-expressions */
 class ProofNodeToSExpr
 {

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index e0f09607523e3e7af354d8330fcafb75572ca761..f421ff4f3c259cb7b7e329829f1961e3c5f2dedd 100644 (file)
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -17,6 +17,7 @@
 #include "expr/lazy_proof.h"
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 

diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 9814c81664ffbf9a72ab75c587ae54ce6c392e4a..2df668384744a431b5eaf1b17a30c126d4bab8af 100644 (file)
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -18,14 +18,17 @@
 #define CVC4__EXPR__PROOF_NODE_UPDATER_H
 
 #include <map>
-#include <unordered_set>
+#include <memory>
 
-#include "expr/proof.h"
+#include "expr/node.h"
 #include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
 
 namespace CVC4 {
 
+class CDProof;
+class ProofNode;
+class ProofNodeManager;
+
 /**
  * A virtual callback class for updating ProofNode. An example use case of this
  * class is to eliminate a proof rule by expansion.

diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp
index bb02aeb204062fd87e456c6d10047265a11c4114..4c99855df49422f511ab224f961d7a3cd7ef179c 100644 (file)
--- a/src/expr/proof_step_buffer.cpp
+++ b/src/expr/proof_step_buffer.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/proof_step_buffer.h"
 
+#include "expr/proof_checker.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {

diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index 4e463a7b3777c8e74dc3813a73b3a755b6fa48f4..1b09a8f963642afd424ab60015bfda076d44f768 100644 (file)
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -20,11 +20,12 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof_checker.h"
 #include "expr/proof_rule.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+
 /**
  * Information for constructing a step in a CDProof. Notice that the conclusion
  * of the proof step is intentionally not included in this data structure.

diff --git a/src/expr/record.h b/src/expr/record.h
index 4e1ff677266ef864fdccad167ca821a51211a245..1ab84c30c2914033580d517bd37b4124c2e25ec8 100644 (file)
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__RECORD_H
 #define CVC4__RECORD_H
 
-#include <functional>
 #include <iostream>
 #include <string>
 #include <vector>

diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index f655581845cc94009fbd58f8b1ddb607ac3ce202..68c4985bbb81341c98377b034abe25f6fca53ffa 100644 (file)
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -14,6 +14,7 @@
 
 #include "expr/sequence.h"
 
+#include <sstream>
 #include <vector>
 
 #include "expr/node.h"

diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp
index 541db1ac529ff5f88f907e2e4003346f51079874..3ca75050a19a561df09950b16c026ccc65614440 100644 (file)
--- a/src/expr/subs.cpp
+++ b/src/expr/subs.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/subs.h"
 
+#include <sstream>
+
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index 3401e55f772c0b5d5e3ba5910e014b3245513feb..e67a1befea20a9dedda5afca3083fdace43b2911 100644 (file)
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/sygus_datatype.h"
 
+#include <sstream>
+
 using namespace CVC4::kind;
 
 namespace CVC4 {

diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index fa5732854d71009ec7aaa0ad9f048de3f0b46d6e..73018d7ca002bccced27bfb38ce0c764a3812524 100644 (file)
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -19,7 +19,6 @@
 
 #include <map>
 #include <memory>
-#include <set>
 #include <string>
 
 #include "api/cvc4cpp.h"

diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp
index 8bd8504888cefb30e841ec34207b0cc33db882f4..105c811d4e91d2ce031d8ee6f3d5a90821ec56b8 100644 (file)
--- a/src/expr/tconv_seq_proof_generator.cpp
+++ b/src/expr/tconv_seq_proof_generator.cpp
@@ -14,6 +14,10 @@
 
 #include "expr/tconv_seq_proof_generator.h"
 
+#include <sstream>
+
+#include "expr/proof_node_manager.h"
+
 namespace CVC4 {
 
 TConvSeqProofGenerator::TConvSeqProofGenerator(

diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
index 95499d6b82326d263bb43376f3c8ea16ff8b1deb..9197028d6388b28adbf6757c6955fd789a3329be 100644 (file)
--- a/src/expr/tconv_seq_proof_generator.h
+++ b/src/expr/tconv_seq_proof_generator.h
@@ -20,11 +20,12 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+
 /**
  * The term conversion sequence proof generator. This is used for maintaining
  * a fixed sequence of proof generators that provide proofs for rewrites

diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp
index e5ebd020946df17f5c8f944f17b4bded11bf703b..91f7f3190a17281cf1209b6bc6dd57548a1677f5 100644 (file)
--- a/src/expr/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/term_canonize.h"
 
+#include <sstream>
+
 // TODO #1216: move the code in this include
 #include "theory/quantifiers/term_util.h"
 

diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index ff8187bbc65e3ce4c554fe6bdaf96905047521cf..061cf1ed220f866e32429d37d5b65ce3ae30318d 100644 (file)
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -18,11 +18,11 @@
 #define CVC4__EXPR__TERM_CONTEXT_NODE_H
 
 #include "expr/node.h"
-#include "expr/term_context.h"
 
 namespace CVC4 {
 
 class TCtxStack;
+class TermContext;
 
 /**
  * A (term-context) sensitive term. This is a wrapper around a Node that

diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp
index 64cab70355ea76c6cb8931f4e3f7631e497887e6..f35514fa653cfb99acde9f2e9938c1b2a6b7f603 100644 (file)
--- a/src/expr/term_context_stack.cpp
+++ b/src/expr/term_context_stack.cpp
@@ -14,6 +14,8 @@
 
 #include "expr/term_context_stack.h"
 
+#include "expr/term_context.h"
+
 namespace CVC4 {
 
 TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {}

diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index d37ccf9147fbe808524f6fc06e2c58193f656f00..a47214ae1c095f6187d7ecd9aea0e60d5bb546ca 100644 (file)
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -14,6 +14,9 @@
 
 #include "expr/term_conversion_proof_generator.h"
 
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+#include "expr/term_context.h"
 #include "expr/term_context_stack.h"
 
 using namespace CVC4::kind;

diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index dcf8b3fa46770d398423b0412a99f3dcdcf8d71a..4d6a169cb9398f78165511b95c063b10f0428952 100644 (file)
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -20,11 +20,12 @@
 #include "context/cdhashmap.h"
 #include "expr/lazy_proof.h"
 #include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
-#include "expr/term_context.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+class TermContext;
+
 /** A policy for how rewrite steps are applied in TConvProofGenerator */
 enum class TConvPolicy : uint32_t
 {

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index dadbdc91dd4dd32c086c720eeb243c0bf915975a..cbc15e153aef64f0d800752e9f57b8499ad48c6b 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -16,6 +16,7 @@
 #include "expr/type.h"
 
 #include <iostream>
+#include <sstream>
 #include <string>
 #include <vector>
 

diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index e7685dba83280b1625d1d52feb678634221f09af..f5a729b360dedcb147df948255ca0525a8ddfc19 100644 (file)
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -14,6 +14,8 @@
  ** TypeChecker implementation.
  **/
 
+#include <sstream>
+
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/type_checker.h"

diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
index 312ffe53a971fe711e7677ca7afa60140d526ed6..32c1254de03a27d2130fd4d363535d85c1bab445 100644 (file)
--- a/src/expr/type_checker_util.h
+++ b/src/expr/type_checker_util.h
@@ -19,6 +19,8 @@
 
 #include "cvc4_private.h"
 
+#include <sstream>
+
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"

diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
index 47fc36eee2f26a888c9281049208dce471228188..1261755826bb09b9c091866bce73e3621cbe5045 100644 (file)
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -19,7 +19,6 @@
 
 #include <vector>
 
-#include "expr/node.h"
 #include "expr/type_node.h"
 
 namespace CVC4 {

diff --git a/src/options/language.cpp b/src/options/language.cpp
index c2eb13852e5bd63f35cacca2c04775f086297e0d..ee6da3e4836144755aaa7ae985d9e9e309202175 100644 (file)
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -16,6 +16,11 @@
 
 #include "options/language.h"
 
+#include <sstream>
+
+#include "base/exception.h"
+#include "options/option_exception.h"
+
 namespace CVC4 {
 namespace language {
 

diff --git a/src/options/language.h b/src/options/language.h
index b34ac378e1cc56a30bd4dfff9854e7a3176c4cee..e1e4dfed3f7b238fc2a91ee247076cd3284f6eec 100644 (file)
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -19,12 +19,9 @@
 #ifndef CVC4__LANGUAGE_H
 #define CVC4__LANGUAGE_H
 
-#include <sstream>
+#include <ostream>
 #include <string>
 
-#include "base/exception.h"
-#include "options/option_exception.h"
-
 namespace CVC4 {
 namespace language {
 
@@ -182,9 +179,9 @@ bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC;
 bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC;
 
 /**
-  * Is the language smtlib 2.5 or above? If exact=true, then this method returns
-  * false if the input language is not exactly SMT-LIB 2.6.
-  */
+ * Is the language smtlib 2.5 or above? If exact=true, then this method returns
+ * false if the input language is not exactly SMT-LIB 2.5.
+ */
 bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
 bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
 /**

diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h
index 6b6a1afb79ea32776ae6011955a3eb90ec77953f..b62c5689848f94d7ff4d4aeae2027a5c966cea82 100644 (file)
--- a/src/options/open_ostream.h
+++ b/src/options/open_ostream.h
@@ -20,13 +20,11 @@
 #ifndef CVC4__OPEN_OSTREAM_H
 #define CVC4__OPEN_OSTREAM_H
 
+#include <iosfwd>
 #include <map>
-#include <ostream>
 #include <string>
 #include <utility>
 
-#include "options/option_exception.h"
-
 namespace CVC4 {
 
 class OstreamOpener {

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 07e62997650c6cb7a17b2a9f15b0ca255e8a98e4..9652c9f8eeff9a745ae97202d04fde795479e345 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -22,17 +22,18 @@
 #include <ostream>
 #include <string>
 
-#include "base/modal_exception.h"
 #include "options/base_handlers.h"
 #include "options/bv_options.h"
 #include "options/decision_options.h"
 #include "options/language.h"
 #include "options/option_exception.h"
-#include "options/options.h"
 #include "options/printer_modes.h"
 #include "options/quantifiers_options.h"
 
 namespace CVC4 {
+
+class Options;
+
 namespace options {
 
 /**

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 4bc3323e5c982bac2cf59e9bedb972e16899c692..250c0639cedf4e84068e712b0f1ac3bf589e1ed0 100644 (file)
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_manager.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
+#include "smt/preprocess_proof_generator.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 9d65329b00f0c98f3e4aafbd0eca0a348f946c7f..408c0718cdccfeac4413a6a7afb7401c97ac7ac5 100644 (file)
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -21,13 +21,15 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/proof_generator.h"
-#include "expr/proof_node_manager.h"
-#include "smt/preprocess_proof_generator.h"
-#include "smt/term_formula_removal.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class ProofGenerator;
+namespace smt {
+class PreprocessProofGenerator;
+}
+
 namespace preprocessing {
 
 using IteSkolemMap = std::unordered_map<size_t, Node>;

diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index a092a877890fbc408e7b113918e5119ff6d8c8a8..f8efa5de965a0f2e920c6ffcac62b38a783537ce 100644 (file)
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -22,11 +22,15 @@
  **/
 
 #include "preprocessing/passes/ackermann.h"
+
 #include <cmath>
+
 #include "base/check.h"
 #include "expr/node_algorithm.h"
 #include "options/options.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -197,7 +201,7 @@ size_t getBVSkolemSize(size_t capacity)
  * a sufficient bit-vector size.
  * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to
  * the fresh skolem BV variables. variables */
-void collectUSortsToBV(const unordered_set<TNode, TNodeHashFunction>& vars,
+void collectUSortsToBV(const std::unordered_set<TNode, TNodeHashFunction>& vars,
                        const USortToBVSizeMap& usortCardinality,
                        SubstitutionMap& usVarsToBVVars)
 {

diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index cd0d059e43af691e9b867fac9abb312db5e1c959..e28a1ca2d2eff876d580f411991a862f3ec03059 100644 (file)
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -27,9 +27,11 @@
 #define CVC4__PREPROCESSING__PASSES__ACKERMANN_H
 
 #include <unordered_map>
+
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/logic_info.h"
+#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index c93895e79885f9159f3906b3e3fdf7248c23fc12..0369dd0edeed24db2777860c25c397891d0ec31b 100644 (file)
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -18,6 +18,8 @@
 #include "preprocessing/passes/apply_substs.h"
 
 #include "context/cdo.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 

diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h
index 781fcc79e4fa8dc1fdcc673325f404e1d72a8663..197e08eafb425cb055eea610b62fa101629e98c9 100644 (file)
--- a/src/preprocessing/passes/apply_substs.h
+++ b/src/preprocessing/passes/apply_substs.h
@@ -21,10 +21,12 @@
 #define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
+
+class PreprocessingPassContext;
+
 namespace passes {
 
 class ApplySubsts : public PreprocessingPass

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 47a504d59cc262e620a46f5102f975adbe791485..6a1d76fad755fc4745b034818882f216829c39e5 100644 (file)
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -19,7 +19,10 @@
 
 #include "base/map_util.h"
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 

diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
index c5e6f380112acb622e79100b180a81a86f23d690..917954da6f7fc7e423dec2b6784fb657becc4acc 100644 (file)
--- a/src/preprocessing/passes/bool_to_bv.h
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -18,10 +18,9 @@
 #ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 #define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
 
+#include "expr/node.h"
 #include "options/bv_options.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index ebc169e421918e38198484a0f7a72dcc1f0ae173..67951d441991d438e9c2dceb2c8888950bfcb4de 100644 (file)
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -26,8 +26,11 @@
 #include <vector>
 
 #include "options/bv_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h
index a49bdae2c891096167f16cb066ee17a14243b443..f9d633bbcf325e9986c8049fac9e7a762beea864 100644 (file)
--- a/src/preprocessing/passes/bv_abstraction.h
+++ b/src/preprocessing/passes/bv_abstraction.h
@@ -27,7 +27,6 @@
 #define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index 460ef25977c1266f3c92302c733d40d08f016828..c521f736c83ea36cd790ff98c5330d9548f10ddb 100644 (file)
--- a/src/preprocessing/passes/bv_eager_atoms.cpp
+++ b/src/preprocessing/passes/bv_eager_atoms.cpp
@@ -18,6 +18,9 @@
 
 #include "preprocessing/passes/bv_eager_atoms.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h
index 4c1bb136c56d36c857bed8c6b6cfcea6d5f422f3..e0b0636548976f8b6541d8dbe3ef858d9540793c 100644 (file)
--- a/src/preprocessing/passes/bv_eager_atoms.h
+++ b/src/preprocessing/passes/bv_eager_atoms.h
@@ -21,7 +21,6 @@
 #define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index 02a08b13382fe8026f564f3cd40e278275b1af51..d8b309609f16b8753dd28bf04830c16da9267291 100644 (file)
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -17,16 +17,17 @@
 
 #include "preprocessing/passes/bv_gauss.h"
 
+#include <unordered_map>
+#include <vector>
+
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 
-#include <unordered_map>
-#include <vector>
-
-
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;

diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index 0b614251ff85d1c765700b369c1ac7343ffc61bb..3b8197f9bd7af697c7462a9c02c56b0c3cfa8acb 100644 (file)
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -20,8 +20,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
 #define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index 1e14e5b4b1fd52606f079315200e01aa92081f64..573d36207fc90f57c36cebdd62d97b3c7c30759c 100644 (file)
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -20,6 +20,8 @@
 
 #include <unordered_map>
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 

diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h
index 92bdc2fc70d30e40087288f7decb22481fa87a03..a270baa647b6050e8c20f405dcf53960470393a3 100644 (file)
--- a/src/preprocessing/passes/bv_intro_pow2.h
+++ b/src/preprocessing/passes/bv_intro_pow2.h
@@ -22,7 +22,6 @@
 #define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index ac8b01d74757a34ae80d400854b9aefda0827723..cf156692b854194c4eab8d52d525eadc79d2c9c9 100644 (file)
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -23,7 +23,10 @@
 
 #include "expr/node.h"
 #include "expr/node_visitor.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 

diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h
index 5054edfc4a71d439bc0a665d4babfc33928a0a69..a19116e7773ad37a0254f17eee3e78e24a2a6e33 100644 (file)
--- a/src/preprocessing/passes/bv_to_bool.h
+++ b/src/preprocessing/passes/bv_to_bool.h
@@ -19,9 +19,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
 #define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 704214d063d582e69d2d8ebfbd6762783613c465..5043718ca8b1055fc662e0e5fcb4e1cec9d3692f 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -18,6 +18,7 @@
 #include "preprocessing/passes/bv_to_int.h"
 
 #include <cmath>
+#include <sstream>
 #include <string>
 #include <unordered_map>
 #include <vector>
@@ -26,6 +27,8 @@
 #include "expr/node_traversal.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
@@ -34,6 +37,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
 

diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index dd830d7cf733b0008f81ecb2368e20035a713db5..edcc84622be42481d9f3536e18857a5152e0e2e1 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -69,10 +69,8 @@
 #define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
 
 #include "context/cdhashmap.h"
-#include "context/cdo.h"
-#include "context/context.h"
+#include "context/cdhashset.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/arith/nl/iand_utils.h"
 
 namespace CVC4 {
@@ -104,7 +102,7 @@ class BVToInt : public PreprocessingPass
    * @return a node representing the shift.
    *
    */
-  Node createShiftNode(vector<Node> children,
+  Node createShiftNode(std::vector<Node> children,
                        uint64_t bvsize,
                        bool isLeftShift);
 
@@ -209,7 +207,7 @@ class BVToInt : public PreprocessingPass
    */
   Node reconstructNode(Node originalNode,
                        TypeNode resultType,
-                       const vector<Node>& translated_children);
+                       const std::vector<Node>& translated_children);
 
   /**
    * A useful utility function.
@@ -247,7 +245,7 @@ class BVToInt : public PreprocessingPass
    * that have children.
    */
   Node translateWithChildren(Node original,
-                             const vector<Node>& translated_children);
+                             const std::vector<Node>& translated_children);
 
   /**
    * Performs the actual translation to integers for nodes

diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 95e10732861c440166bf63a86e64b03f170cb3cd..381e1b5893d886fcab4cf47174b679b1f0d107cc 100644 (file)
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -17,6 +17,8 @@
 #include "preprocessing/passes/extended_rewriter_pass.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h
index f4314a123d8b54f3ffb776bc9406492b721a6f1a..22b4d2da6aacbb6175a31ffe082a9c2522a90979 100644 (file)
--- a/src/preprocessing/passes/extended_rewriter_pass.h
+++ b/src/preprocessing/passes/extended_rewriter_pass.h
@@ -20,7 +20,6 @@
 #define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index c7bed4d31e27c87738e3ed80f6528e7838f13de3..6e898a3c250b20b165a28e24d65e0ef96ce96120 100644 (file)
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -17,6 +17,9 @@
 #include "preprocessing/passes/foreign_theory_rewrite.h"
 
 #include "expr/node_traversal.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h
index 2a882641e7597abd61d219a3fcf2f2119af4e6bb..aca3d0cfe11c00e8e98d37dbe810b7973f456dcd 100644 (file)
--- a/src/preprocessing/passes/foreign_theory_rewrite.h
+++ b/src/preprocessing/passes/foreign_theory_rewrite.h
@@ -20,10 +20,8 @@
 #define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H
 
 #include "context/cdhashmap.h"
-#include "context/cdo.h"
-#include "context/context.h"
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -57,7 +55,7 @@ class ForeignTheoryRewrite : public PreprocessingPass
   /** construct a node with the same operator as originalNode whose children are
    * processedChildren
    */
-  static Node reconstructNode(Node originalNode, vector<Node> newChildren);
+  static Node reconstructNode(Node originalNode, std::vector<Node> newChildren);
   /** A cache to store the simplified nodes */
   CDNodeMap d_cache;
 };

diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 8c7a7102192c9364db227c46725e931356dadd9f..1657aeafa7d50964e22fddc8789a1bf8cbf450e5 100644 (file)
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -14,11 +14,16 @@
 
 #include "preprocessing/passes/fun_def_fmf.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "proof/proof_manager.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace std;
 using namespace CVC4::kind;

diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h
index 36d1166b70360d5f03e8caea477ae799e128c3e5..d091d9db409496a55aaf456a2f08e85a06a43fd2 100644 (file)
--- a/src/preprocessing/passes/fun_def_fmf.h
+++ b/src/preprocessing/passes/fun_def_fmf.h
@@ -16,12 +16,11 @@
 #define CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H
 
 #include <map>
-#include <string>
 #include <vector>
 
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 00ca1efd3a22da79492c447eb7acb20d336c9d88..de7a7fb478584b02d9e91060d8dcb0c62bb23b90 100644 (file)
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -17,6 +17,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 
 using namespace std;

diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
index af8ae504824e67b471d684b1be943be3ee80cf93..b59303870a927a1a663fcda9f385842352c06e34 100644 (file)
--- a/src/preprocessing/passes/global_negate.h
+++ b/src/preprocessing/passes/global_negate.h
@@ -25,8 +25,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
 #define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 8cf4ad2eda97d263daf88f4e479121248eed3d8a..1f64e2e87aefb19987b6b80777d0784fdfec73bb 100644 (file)
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 #include "theory/uf/theory_uf_rewriter.h"
 

diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h
index a1dc05b835c513537a9695f91767f981509adfca..01683d2f5808efdba1d0e8f44ade5f219b3392d9 100644 (file)
--- a/src/preprocessing/passes/ho_elim.h
+++ b/src/preprocessing/passes/ho_elim.h
@@ -19,8 +19,12 @@
 #ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
 #define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H
 
+#include <map>
+#include <unordered_map>
+#include <unordered_set>
+
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index 5b046577293afa68eae6d09992c2a581bfa234d5..2e237df2b2ae6e27cf54b703b37d69fe2935ab47 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -25,6 +25,7 @@
 #include "expr/node.h"
 #include "expr/node_traversal.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
@@ -32,6 +33,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;

diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h
index 208e7ab6ac06f5c3025fa981a1e537641fa500cd..a2085d6ebaff0da780f4202d0948338d06742957 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.h
+++ b/src/preprocessing/passes/int_to_bv.h
@@ -22,7 +22,6 @@
 #define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index f788338be263849c002fafc75ae89a2e1b734936..b8253580478573a061e8537b3550e885a8dfc77b 100644 (file)
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -18,6 +18,10 @@
 #include "preprocessing/passes/ite_removal.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "proof/proof_manager.h"
+#include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_preprocessor.h"
 

diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h
index 2b8a05fe4171dca3e3f220f5371860f712d01a1d..a7ed8775223a9081752811cffdb3115b7010def5 100644 (file)
--- a/src/preprocessing/passes/ite_removal.h
+++ b/src/preprocessing/passes/ite_removal.h
@@ -20,11 +20,7 @@
 #ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
 #define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
 
-#include <unordered_set>
-#include <vector>
-
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 2a1f4c3e6e771a9057fa0f5bef4888a2a16005ee..6ed149895462afbd3f7af0c169f7af52e2b27e57 100644 (file)
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -17,10 +17,15 @@
 #include <vector>
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/nary_builder.h"
 #include "theory/arith/arith_ite_utils.h"
+#include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
+using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
 

diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h
index fe1dfa6e0813f07065678964607de212855c3479..603e7889e3ca5e991291b72b4375f36f030a4db9 100644 (file)
--- a/src/preprocessing/passes/ite_simp.h
+++ b/src/preprocessing/passes/ite_simp.h
@@ -18,7 +18,7 @@
 #define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
+#include "preprocessing/util/ite_utilities.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 50dbc4a2778c6d74fc191e765327968a81e32d8c..20a5fdbb0d92bfaf3225af76c54841b3f3dfeb10 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -15,14 +15,18 @@
 
 #include "preprocessing/passes/miplib_trick.h"
 
+#include <sstream>
 #include <vector>
 
 #include "expr/node_self_iterator.h"
 #include "options/arith_options.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/booleans/circuit_propagator.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
@@ -30,6 +34,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 namespace {

diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h
index f7be87f18d4b03fbcfaec5a69fd56c2d7eb59eed..99fd766caa8342c6cc6f096e021e735741e9bde8 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.h
+++ b/src/preprocessing/passes/miplib_trick.h
@@ -18,8 +18,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
 #define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index 88bdf2e5c0e4544b92b777491abf6b9999a2356a..553a850368feba090c0dd4354270ff31b55b65c1 100644 (file)
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -16,11 +16,14 @@
 
 #include "preprocessing/passes/nl_ext_purify.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 Node NlExtPurify::purifyNlTerms(TNode n,

diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h
index 5c7c5776e3fca5d9d3256f808cfec9713cf4d28c..df06dc22d4cbc303e0ba899807d567ec95f3cda6 100644 (file)
--- a/src/preprocessing/passes/nl_ext_purify.h
+++ b/src/preprocessing/passes/nl_ext_purify.h
@@ -25,7 +25,6 @@
 
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index 8cff66d721303d72b10fef290032a0df16849841..6d6cfac41d8487260da971a5e2bb0b30ee897b28 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -20,7 +20,13 @@
 
 #include "context/cdo.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/preprocess_proof_generator.h"
 #include "smt/smt_statistics_registry.h"
+#include "theory/booleans/circuit_propagator.h"
+#include "theory/theory.h"
+#include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
@@ -289,7 +295,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       << "Resize non-clausal learned literals to " << j << std::endl;
   learned_literals.resize(j);
 
-  unordered_set<TNode, TNodeHashFunction> s;
+  std::unordered_set<TNode, TNodeHashFunction> s;
   for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
   {
     Node assertion = (*assertionsToPreprocess)[i];

diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index f94eb2d700925bbe293de1a7f354d641cfb883ef..9539b6fd8a363dbe17fe4b2fa52820e17e215c99 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -17,16 +17,23 @@
 #ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
 #define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H
 
-#include <vector>
-
-#include "expr/lazy_proof.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "smt/preprocess_proof_generator.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {
+
+class LazyCDProof;
+class ProofNodeManager;
+
+namespace smt {
+class PreprocessProofGenerator;
+}
+namespace theory {
+class TrustSubstitutionMap;
+}
+
 namespace preprocessing {
 namespace passes {
 

diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index 2720d2f0b938b5e2ecf710cfd8b5ee42ef4b691d..a9396c570bc949ca1267c24b08b3606a87b3546d 100644 (file)
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -18,6 +18,8 @@
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 
 #include "base/output.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 #include "theory/rewriter.h"

diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h
index 03137dac5846deab72d6496ee21b2780161de176..b1338bb38d4032e3494aee5aff4a84eedc7f86cd 100644 (file)
--- a/src/preprocessing/passes/pseudo_boolean_processor.h
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -25,10 +25,8 @@
 
 #include "context/cdhashmap.h"
 #include "context/cdo.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/substitutions.h"
 #include "util/maybe.h"
 #include "util/rational.h"

diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index ea73b7958aa6c0d3e1053f1e822877cec1ee2475..4e4d30649570e3730f1deb3af5b5406b66004f1b 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -20,6 +20,9 @@
 
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "proof/proof_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/arith/arith_msum.h"
@@ -29,6 +32,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4::theory;

diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
index c5e557a9e0e37792abe40e80cd0c56ae8fe0759d..d5396be7de1c69ebd1d28d48096e155c476ee120 100644 (file)
--- a/src/preprocessing/passes/quantifier_macros.h
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -18,12 +18,9 @@
 #define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H
 
 #include <map>
-#include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type_node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
index 6daafff2d9a0f13ca00721ca30f72d01dc3b8137..5caf376118eeefbbcf4efbd87a412c6b1fb5754d 100644 (file)
--- a/src/preprocessing/passes/quantifiers_preprocess.cpp
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -20,6 +20,7 @@
 #include "preprocessing/passes/quantifiers_preprocess.h"
 
 #include "base/output.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/rewriter.h"
 
@@ -27,6 +28,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 QuantifiersPreprocess::QuantifiersPreprocess(PreprocessingPassContext* preprocContext)

diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h
index 43fce22b3902cc7e8339cd896b7037ad7e186b7b..ad18a382cbbcd6201734ed73c8f427f9e3284e62 100644 (file)
--- a/src/preprocessing/passes/quantifiers_preprocess.h
+++ b/src/preprocessing/passes/quantifiers_preprocess.h
@@ -23,7 +23,6 @@
 #define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 672e281d7ee6943cfb04cad0cb2ae07fc44fde3f..f7995c2d75341c7aaf82c5472aea45dd43c81c65 100644 (file)
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -18,6 +18,8 @@
 
 #include <string>
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -26,6 +28,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq)

diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h
index 9fd8aca53c4b68df33adb3bb6475393220936d3a..bab6f604c6f8ca5547b8eae6c122dbc046cf9f2c 100644 (file)
--- a/src/preprocessing/passes/real_to_int.h
+++ b/src/preprocessing/passes/real_to_int.h
@@ -19,12 +19,10 @@
 #ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
 #define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H
 
-#include <unordered_map>
 #include <vector>
 
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index b8c9498e17dc04fcb4d67551c34387773bc9d9f2..0684dde81df7117e0adabb25b2c23c253fd78e31 100644 (file)
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -16,6 +16,7 @@
 
 #include "preprocessing/passes/rewrite.h"
 
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h
index 76493958af381e2cbb4f7576d96f32773750c258..73ce82873f500a34434348076ed086ebbb55e1b6 100644 (file)
--- a/src/preprocessing/passes/rewrite.h
+++ b/src/preprocessing/passes/rewrite.h
@@ -20,7 +20,6 @@
 #define CVC4__PREPROCESSING__PASSES__REWRITE_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index ef2014b8a2e17fd9766259941f2ab01e73330ba6..20720668c81e146a09b3ade412b480f199eaa771 100644 (file)
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
@@ -28,6 +29,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 namespace {

diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h
index 912fd1b603c78525d97e4216af9e02c742e16647..50ea641e28d7d2a7fca659dfa66830d54ebcd38e 100644 (file)
--- a/src/preprocessing/passes/sep_skolem_emp.h
+++ b/src/preprocessing/passes/sep_skolem_emp.h
@@ -19,7 +19,6 @@
 #define CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 918b13140be0cc31c42dda0276ea4429419a7b0b..8e75acf9e8ba580d89ca45412617d793ae95406c 100644 (file)
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -16,9 +16,13 @@
 
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/dump_manager.h"
+#include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 

diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h
index 1a18b6fd1d1b43ac1d5e6c524303a772d92cb9fa..23a9107807ac174c91fbce4e5417f35743e9b6b1 100644 (file)
--- a/src/preprocessing/passes/sort_infer.h
+++ b/src/preprocessing/passes/sort_infer.h
@@ -15,13 +15,7 @@
 #ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
 #define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_
 
-#include <map>
-#include <string>
-#include <vector>
-
-#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index d48857396c5aa3220289c5c62e60a0b894ccb0f8..26055f718e29168c2f4565daf0d8052cd33c4d28 100644 (file)
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -18,7 +18,10 @@
 #include <string>
 
 #include "expr/node.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h
index c86ebf90fdeff38b58cca4face48a448c2d62c80..5c0ec816d3f97cec233529489b89a854646062d5 100644 (file)
--- a/src/preprocessing/passes/static_learning.h
+++ b/src/preprocessing/passes/static_learning.h
@@ -19,7 +19,6 @@
 #define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp
index 69cb8914c10ae63218fcf861d416c8d6280dc8cb..ddc7f4e21fc0063d9bea090f45fb2e4074e53069 100644 (file)
--- a/src/preprocessing/passes/strings_eager_pp.cpp
+++ b/src/preprocessing/passes/strings_eager_pp.cpp
@@ -14,8 +14,9 @@
 
 #include "preprocessing/passes/strings_eager_pp.h"
 
-#include "theory/strings/theory_strings_preprocess.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
+#include "theory/strings/theory_strings_preprocess.h"
 
 using namespace CVC4::theory;
 

diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h
index 299260c61f94cdca6beb012ced909fd5938cbce4..8679a6f700efc25e5d7e65a36778dd544f428a7c 100644 (file)
--- a/src/preprocessing/passes/strings_eager_pp.h
+++ b/src/preprocessing/passes/strings_eager_pp.h
@@ -18,7 +18,6 @@
 #define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index caf63b0ec18cf6af60e6855fcb63e85959276ecf..933efbfde9e2963cb880d2363e3610e4031debfa 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -14,6 +14,8 @@
 
 #include "preprocessing/passes/sygus_inference.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
@@ -21,6 +23,7 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_utils.h"
+#include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;

diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h
index 31d94efd2a678df902eba1d9b772e745091156eb..4a67ae224752efadf60495d88acea2cc97116c7f 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.h
+++ b/src/preprocessing/passes/sygus_inference.h
@@ -15,13 +15,10 @@
 #ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
 #define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
 
-#include <map>
-#include <string>
 #include <vector>
 #include "expr/node.h"
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 7b54fee6152e2dcfb5fb558abdd06ff30ebe5dbf..b899b2de745d52f9f080c62e83062fd7ba8fae57 100644 (file)
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -15,10 +15,13 @@
 
 #include "preprocessing/passes/synth_rew_rules.h"
 
+#include <sstream>
+
 #include "expr/sygus_datatype.h"
 #include "expr/term_canonize.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "printer/printer.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"

diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h
index 5613c1b220c2bbed81f3c6005ac2afd7feecf07f..3721f94578faf3dd8a1123fa65821b920ca09324 100644 (file)
--- a/src/preprocessing/passes/synth_rew_rules.h
+++ b/src/preprocessing/passes/synth_rew_rules.h
@@ -17,7 +17,6 @@
 #define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 22ae147629b6c11b54ef3a19a754bed5e15c7034..04d761d2fb3ffd91c7a9fb4ee2e7eb123f35a31b 100644 (file)
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -17,6 +17,10 @@
 #include "preprocessing/passes/theory_preprocess.h"
 
 #include "options/smt_options.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "proof/proof_manager.h"
+#include "prop/prop_engine.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
@@ -35,7 +39,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
   d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep);
 
   IteSkolemMap& imap = assertions->getIteSkolemMap();
-  PropEngine* propEngine = d_preprocContext->getPropEngine();
+  prop::PropEngine* propEngine = d_preprocContext->getPropEngine();
   // Remove all of the ITE occurrences and normalize
   for (unsigned i = 0, size = assertions->size(); i < size; ++i)
   {

diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h
index 49597828db810ec3de75d5ca0b32793ae34037f0..1635d4c3ba3bf4ed5cadc61a6bcde7f8cb53e108 100644 (file)
--- a/src/preprocessing/passes/theory_preprocess.h
+++ b/src/preprocessing/passes/theory_preprocess.h
@@ -20,7 +20,6 @@
 #define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H
 
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 68de75194145d71609014f8275f2f46cdfd71c85..95f70d0f6b110529b4a80f61c07c5717517279f2 100644 (file)
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -14,6 +14,8 @@
 
 #include "preprocessing/passes/theory_rewrite_eq.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::theory;

diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h
index bc4027310c501efe6587f8c4d7ea4ffb79bb8d1c..c15f5e36e725051def43ec7e3e657f0d42be7ddf 100644 (file)
--- a/src/preprocessing/passes/theory_rewrite_eq.h
+++ b/src/preprocessing/passes/theory_rewrite_eq.h
@@ -17,8 +17,8 @@
 #ifndef CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
 #define CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H
 
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 6ebf1b8c88205be2b904a8d47fb884e338130964..e50548ff8a8ab9ad2b85d7710ee9d1ddf89b2984 100644 (file)
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -19,6 +19,9 @@
 #include "preprocessing/passes/unconstrained_simplifier.h"
 
 #include "expr/dtype.h"
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
@@ -27,6 +30,7 @@ namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
+using namespace std;
 using namespace CVC4::theory;
 
 UnconstrainedSimplifier::UnconstrainedSimplifier(

diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index ebfe51e7987a6a1bf815153672a6ca6be1a97361..b4d18a424b5d61401d80cbe41d0fd35e463af2b6 100644 (file)
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -23,17 +23,16 @@
 
 #include <unordered_map>
 #include <unordered_set>
-#include <vector>
 
-#include "context/context.h"
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/logic_info.h"
 #include "theory/substitutions.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+namespace context {
+class Context;
+}
 namespace preprocessing {
 namespace passes {
 

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 169f10c9df2c442d89908bad2c159c1c357f94b3..3eec24414a2fbf70e083afa476be58822308736a 100644 (file)
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -16,9 +16,13 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
+#include "preprocessing/assertion_pipeline.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "printer/printer.h"
 #include "smt/dump.h"
+#include "smt/output_manager.h"
+#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
-#include "printer/printer.h"
 
 namespace CVC4 {
 namespace preprocessing {

diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index b8ddb9846e2e6ff254e4d5a45e6975fd45c435b2..3970ee8d3146f49c42f0a0845e77d608313eb8c8 100644 (file)
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -33,14 +33,14 @@
 
 #include <string>
 
-#include "preprocessing/assertion_pipeline.h"
-#include "preprocessing/preprocessing_pass_context.h"
-#include "smt/smt_engine_scope.h"
-#include "theory/logic_info.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
 
+class AssertionPipeline;
+class PreprocessingPassContext;
+
 /**
  * Preprocessing passes return a result which indicates whether a conflict has
  * been detected during preprocessing.

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index c22a69255b7528f5e2fc3d2f41ae18611a503ae8..2db213caf010aa95ebbd4caa7392f0e12fb7e33d 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -21,18 +21,20 @@
 #ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 #define CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 
-#include "context/cdo.h"
-#include "context/context.h"
-#include "decision/decision_engine.h"
-#include "preprocessing/util/ite_utilities.h"
+#include "context/cdhashset.h"
 #include "smt/smt_engine.h"
-#include "smt/term_formula_removal.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/theory_engine.h"
 #include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
+class SmtEngine;
+class TheoryEngine;
+namespace theory::booleans {
+class CircuitPropagator;
+}
+namespace prop {
+class PropEngine;
+}
 namespace preprocessing {
 
 class PreprocessingPassContext

diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index ce5c5da226fe4a6bcc286431844e6b1cf3912330..01bbab3a6ac01244122cd8f331368829f83fec7a 100644 (file)
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -19,15 +19,14 @@
 #ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
 #define CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H
 
-#include <memory>
+#include <functional>
 #include <string>
 #include <unordered_map>
 
-#include "preprocessing/preprocessing_pass.h"
-
 namespace CVC4 {
 namespace preprocessing {
 
+class PreprocessingPass;
 class PreprocessingPassContext;
 
 /**

diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 7e05af6981f9c28f75ea6f55e8f18ce3fcdf2d6c..33d5cb826e29273a325c203195c126059ef5501c 100644 (file)
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -21,6 +21,7 @@
 
 #include <utility>
 
+#include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/passes/rewrite.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter.h"

diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index c82bf7958d46cf81135ead6d81cc983b5be13598..fbe94302ff0bd038c024a695db7a14cd61980bfc 100644 (file)
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -27,16 +27,16 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "preprocessing/assertion_pipeline.h"
 #include "util/hash.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
 namespace preprocessing {
+
+class AssertionPipeline;
+
 namespace util {
 
-class IncomingArcCounter;
-class TermITEHeightCounter;
 class ITECompressor;
 class ITESimplifier;
 class ITECareSimplifier;

diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h
index 45a09d07f70479756341b3e620bd62a13756428e..1572ab014b758df439d708c0f50c4a7ced1aaf85 100644 (file)
--- a/src/printer/let_binding.h
+++ b/src/printer/let_binding.h
@@ -17,7 +17,6 @@
 #ifndef CVC4__PRINTER__LET_BINDING_H
 #define CVC4__PRINTER__LET_BINDING_H
 
-#include <map>
 #include <vector>
 
 #include "context/cdhashmap.h"

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 0a5ed1eac0275dc3ba8978520ba9831e89eab189..dba29e5241850cb0ce23cd7087f5683d0d5cd0b5 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__PRINTER__PRINTER_H
 #define CVC4__PRINTER__PRINTER_H
 
-#include <map>
 #include <string>
 
 #include "expr/node.h"

diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 286c4e0bf3a8e7823bff56c9f3777060f836cdad..acbfbb2a2d947310e4a4ecda7e7d05a8c9af6a49 100644 (file)
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -21,14 +21,12 @@
 #ifndef CVC4__CNF_PROOF_H
 #define CVC4__CNF_PROOF_H
 
-#include <iosfwd>
 #include <unordered_map>
 #include <unordered_set>
 
 #include "context/cdhashmap.h"
 #include "proof/clause_id.h"
-#include "proof/sat_proof.h"
-#include "util/maybe.h"
+#include "proof/proof_manager.h"
 
 namespace CVC4 {
 namespace prop {

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c7eb2282bcd90e1c155ab5ced14b111b83e22f6c..f05fb03866c27437bb6c4f21f06d41ffb565fe50 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -19,7 +19,6 @@
 #ifndef CVC4__PROOF_MANAGER_H
 #define CVC4__PROOF_MANAGER_H
 
-#include <iosfwd>
 #include <memory>
 #include <unordered_map>
 #include <unordered_set>
@@ -28,7 +27,6 @@
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "proof/clause_id.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 

diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 9907b8d7276e45a4b02fbfce186f2c00150c3e34..c76878da4be840b32948457b4a22f355575a54ee 100644 (file)
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -21,13 +21,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef BVMinisat_SimpSolver_h
 #define BVMinisat_SimpSolver_h
 
-#include "context/context.h"
 #include "proof/clause_id.h"
 #include "prop/bvminisat/core/Solver.h"
 #include "prop/bvminisat/mtl/Queue.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
+
+namespace context {
+class Context;
+}
+
 namespace BVMinisat {
 
 //=================================================================================================

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 69cbb02417d18f89f0b5f9443f750bf1c851c772..92bdd66ee3eaf0a2cb2891f12dbcf2b5859534cd 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -32,7 +32,7 @@
 #include "proof/proof_manager.h"
 #include "prop/proof_cnf_stream.h"
 #include "prop/registrar.h"
-#include "prop/theory_proxy.h"
+#include "prop/sat_solver_types.h"
 
 namespace CVC4 {
 
@@ -41,6 +41,8 @@ class OutputManager;
 namespace prop {
 
 class ProofCnfStream;
+class PropEngine;
+class SatSolver;
 
 /** A policy for how literals for formulas are handled in cnf_stream */
 enum class FormulaLitPolicy : uint32_t

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 8fa489f65f84d6c949301ad711ce3e48db5cb54e..f685017a7bd9713e87a8320a10060632ed069551 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -36,6 +36,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/utils/Options.h"
 #include "prop/sat_proof_manager.h"
 #include "theory/theory.h"
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 template <class Solver> class TSatProof;

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 738b4dc9c7732c5eb46f1969c63431f9d07164c3..4734491795ee300e2d25768a8205b0d0ebba3d88 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -32,6 +32,7 @@
 #include "proof/proof_manager.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
+#include "prop/prop_proof_manager.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_factory.h"
 #include "prop/theory_proxy.h"
@@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te,
       d_resourceManager(rm),
       d_outMgr(outMgr)
 {
-  Debug("prop") << "Constructing the PropEngine" << endl;
+  Debug("prop") << "Constructing the PropEngine" << std::endl;
 
   d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
   d_decisionEngine->init();  // enable appropriate strategies
@@ -146,7 +147,7 @@ void PropEngine::finishInit()
 }
 
 PropEngine::~PropEngine() {
-  Debug("prop") << "Destructing the PropEngine" << endl;
+  Debug("prop") << "Destructing the PropEngine" << std::endl;
   d_decisionEngine->shutdown();
   d_decisionEngine.reset(nullptr);
   delete d_cnfStream;
@@ -179,7 +180,7 @@ void PropEngine::notifyPreprocessedAssertions(
 
 void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
   d_decisionEngine->addAssertion(node);
   assertInternal(node, false, false, true);
 }
@@ -187,7 +188,7 @@ void PropEngine::assertFormula(TNode node) {
 void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
   d_decisionEngine->addSkolemDefinition(node, skolem);
   assertInternal(node, false, false, true);
 }
@@ -235,7 +236,7 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
                                             bool removable)
 {
   Node node = trn.getNode();
-  Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+  Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
   bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
   Assert(!isProofEnabled() || trn.getGenerator() != nullptr);
   assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
@@ -292,7 +293,7 @@ void PropEngine::assertLemmasInternal(
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
-  Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl;
+  Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << std::endl;
 
   Assert(n.getType().isBoolean());
   SatLiteral lit = d_cnfStream->getLiteral(n);
@@ -307,26 +308,26 @@ bool PropEngine::isDecision(Node lit) const {
 void PropEngine::printSatisfyingAssignment(){
   const CnfStream::NodeToLiteralMap& transCache =
     d_cnfStream->getTranslationCache();
-  Debug("prop-value") << "Literal | Value | Expr" << endl
+  Debug("prop-value") << "Literal | Value | Expr" << std::endl
                       << "----------------------------------------"
-                      << "-----------------" << endl;
+                      << "-----------------" << std::endl;
   for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(),
       end = transCache.end();
       i != end;
       ++i) {
-    pair<Node, SatLiteral> curr = *i;
+    std::pair<Node, SatLiteral> curr = *i;
     SatLiteral l = curr.second;
     if(!l.isNegated()) {
       Node n = curr.first;
       SatValue value = d_satSolver->modelValue(l);
-      Debug("prop-value") << "'" << l << "' " << value << " " << n << endl;
+      Debug("prop-value") << "'" << l << "' " << value << " " << n << std::endl;
     }
   }
 }
 
 Result PropEngine::checkSat() {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
-  Debug("prop") << "PropEngine::checkSat()" << endl;
+  Debug("prop") << "PropEngine::checkSat()" << std::endl;
 
   // Mark that we are in the checkSat
   ScopedBool scopedBool(d_inCheckSat);
@@ -360,7 +361,7 @@ Result PropEngine::checkSat() {
     printSatisfyingAssignment();
   }
 
-  Debug("prop") << "PropEngine::checkSat() => " << result << endl;
+  Debug("prop") << "PropEngine::checkSat() => " << result << std::endl;
   if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
     return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
   }
@@ -491,20 +492,20 @@ void PropEngine::push()
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   d_satSolver->push();
-  Debug("prop") << "push()" << endl;
+  Debug("prop") << "push()" << std::endl;
 }
 
 void PropEngine::pop()
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
   d_satSolver->pop();
-  Debug("prop") << "pop()" << endl;
+  Debug("prop") << "pop()" << std::endl;
 }
 
 void PropEngine::resetTrail()
 {
   d_satSolver->resetTrail();
-  Debug("prop") << "resetTrail()" << endl;
+  Debug("prop") << "resetTrail()" << std::endl;
 }
 
 unsigned PropEngine::getAssertionLevel() const
@@ -522,7 +523,7 @@ void PropEngine::interrupt()
 
   d_interrupted = true;
   d_satSolver->interrupt();
-  Debug("prop") << "interrupt()" << endl;
+  Debug("prop") << "interrupt()" << std::endl;
 }
 
 void PropEngine::spendResource(ResourceManager::Resource r)

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index d0c75a924ace73c424d5324757aaaf3209e0b633..834f35d90074165b15d6c9fe2eaceb66b880b67a 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -21,22 +21,11 @@
 #ifndef CVC4__PROP_ENGINE_H
 #define CVC4__PROP_ENGINE_H
 
-#include <sys/time.h>
-
-#include "base/modal_exception.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
-#include "options/options.h"
-#include "proof/proof_manager.h"
-#include "prop/minisat/core/Solver.h"
-#include "prop/minisat/minisat.h"
-#include "prop/proof_cnf_stream.h"
-#include "prop/prop_proof_manager.h"
-#include "prop/sat_solver_types.h"
+#include "theory/output_channel.h"
 #include "theory/trust_node.h"
-#include "theory/theory_inference_manager.h"
-#include "util/resource_manager.h"
 #include "util/result.h"
-#include "util/unsafe_interrupt_exception.h"
 
 namespace CVC4 {
 
@@ -45,16 +34,12 @@ class DecisionEngine;
 class OutputManager;
 class TheoryEngine;
 
-namespace theory {
-  class TheoryRegistrar;
-}/* CVC4::theory namespace */
-
 namespace prop {
 
 class CnfStream;
 class CDCLTSatSolverInterface;
-
-class PropEngine;
+class ProofCnfStream;
+class PropPfManager;
 
 /**
  * PropEngine is the abstraction of a Sat Solver, providing methods for

diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index 3c18dc8965c8a72771449b9a1686fade2c62dfa5..c19d09bb94c810e5883917b3665f0697b97a0e08 100644 (file)
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -16,6 +16,8 @@
 
 #include "expr/proof_ensure_closed.h"
 #include "expr/proof_node_algorithm.h"
+#include "prop/prop_proof_manager.h"
+#include "prop/sat_solver.h"
 
 namespace CVC4 {
 namespace prop {

diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index fc0151bcd97fa53fecf81abdb30279db3c7547bd..2e0d997df85837dcb830fe3f7966fdb71f60e6c6 100644 (file)
--- a/src/prop/prop_proof_manager.h
+++ b/src/prop/prop_proof_manager.h
@@ -27,6 +27,8 @@ namespace CVC4 {
 
 namespace prop {
 
+class CDCLTSatSolverInterface;
+
 /**
  * This class is responsible for managing the proof output of PropEngine, both
  * building and checking it.

diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 0555e7ba7874f63792f80ae57562fdf90d7dee1e..e0592326815d67206778b5273026e8dcac93b9de 100644 (file)
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -21,10 +21,7 @@
 #include "expr/buffered_proof_generator.h"
 #include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
-#include "expr/proof.h"
-#include "expr/proof_node_manager.h"
 #include "prop/minisat/core/SolverTypes.h"
-#include "prop/cnf_stream.h"
 #include "prop/sat_solver_types.h"
 
 namespace Minisat {
@@ -32,8 +29,13 @@ class Solver;
 }
 
 namespace CVC4 {
+
+class ProofNodeManager;
+
 namespace prop {
 
+class CnfStream;
+
 /**
  * This class is responsible for managing the proof production of the SAT
  * solver. It tracks resolutions produced during solving and stores them,

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index ac79cf967ca1528e3e917d86a6b7308b8d21b3f1..0492328688075f41b273c49c5bde94dff313cd28 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -23,19 +23,16 @@
 // Optional blocks below will be unconditionally included
 #define CVC4_USE_MINISAT
 
-#include <iosfwd>
 #include <unordered_set>
 
-#include "context/cdhashmap.h"
 #include "context/cdqueue.h"
 #include "expr/node.h"
 #include "prop/registrar.h"
-#include "prop/sat_solver.h"
+#include "prop/sat_solver_types.h"
 #include "theory/theory.h"
 #include "theory/theory_preprocessor.h"
 #include "theory/trust_node.h"
 #include "util/resource_manager.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 3f03c00e221b31ddc56d08117610c8958f4c0813..6a326ed2e6c67e5c80492c02e694ceeadf353b3d 100644 (file)
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/abduction_solver.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index 6776b06e28de615f95aef355ac1427cad398a265..5c1e1b879b7ac86e20cc55e5cb7781b65d627351 100644 (file)
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -19,6 +19,7 @@
 #include "options/language.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
+#include "smt/abstract_values.h"
 #include "smt/smt_engine.h"
 
 using namespace CVC4::theory;

diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index 5ce2556a79ba449f968e103e405241852ebac126..bba4d2e29bb9a81f23ae0b70a089a78128ed118f 100644 (file)
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -20,14 +20,14 @@
 #include <vector>
 
 #include "context/cdlist.h"
-#include "context/context.h"
 #include "expr/node.h"
 #include "preprocessing/assertion_pipeline.h"
-#include "smt/abstract_values.h"
 
 namespace CVC4 {
 namespace smt {
 
+class AbstractValues;
+
 /**
  * Contains all information pertaining to the assertions of an SMT engine.
  *

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 310201f47cbe8daed782124437db3589cf340bbc..b211c61c20b0a1c72aedb0618d1a6334bc248967 100644 (file)
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -15,8 +15,10 @@
 #include "smt/check_models.h"
 
 #include "options/smt_options.h"
+#include "smt/model.h"
 #include "smt/node_command.h"
 #include "smt/preprocessor.h"
+#include "smt/smt_solver.h"
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 #include "theory/theory_engine.h"

diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index 14af41b2793711870dd8b7ab1d5af719d3022886..f9d527867784c606c84140927b05f55d9f9ccac7 100644 (file)
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -19,12 +19,13 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
-#include "smt/model.h"
-#include "smt/smt_solver.h"
 
 namespace CVC4 {
 namespace smt {
 
+class Model;
+class SmtSolver;
+
 /**
  * This utility is responsible for checking the current model.
  */

diff --git a/src/smt/command.h b/src/smt/command.h
index c11012944aa3166550f84040f1c5d6a452d90d82..a2230e12a36446f5e1588646fc08cbb97c0f5cc4 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -23,7 +23,6 @@
 #define CVC4__COMMAND_H
 
 #include <iosfwd>
-#include <map>
 #include <sstream>
 #include <string>
 #include <vector>
@@ -40,8 +39,6 @@ class Term;
 }  // namespace api
 
 class SymbolManager;
-class UnsatCore;
-class SmtEngine;
 class Command;
 class CommandStatus;
 

diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index 192bb232411203e2b4b6ded474f8f6a86d167bda..c7a05e21b7267ee135c1f6d5d486f1ca8e1c67bd 100644 (file)
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -20,13 +20,17 @@
 #include <memory>
 #include <vector>
 
-#include "context/cdlist.h"
+#include "context/context.h"
 #include "expr/node.h"
 
 namespace CVC4 {
 
 class NodeCommand;
 
+namespace context {
+class UserContext;
+}
+
 namespace smt {
 
 /**

diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index c2c4b6fd228ba7e3a2da77c0893ab9b697a06ebe..c01b5a2435fae546f97ff897efbbb67619223d03 100644 (file)
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -18,8 +18,10 @@
 #include <utility>
 
 #include "expr/node_manager_attributes.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "smt/defined_function.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
 
 using namespace CVC4::preprocessing;

diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index 486aa0c3a15f06c1828d49865bd3d1148d3cb767..0c2f9b2d56815e403ce683ef616c7c731abb8158 100644 (file)
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -20,17 +20,23 @@
 #include <unordered_map>
 
 #include "expr/node.h"
-#include "expr/term_conversion_proof_generator.h"
-#include "preprocessing/assertion_pipeline.h"
-#include "smt/smt_engine_stats.h"
-#include "util/resource_manager.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 
+class ProofNodeManager;
+class ResourceManager;
 class SmtEngine;
+class TConvProofGenerator;
+
+namespace preprocessing {
+class AssertionPipeline;
+}
 
 namespace smt {
 
+struct SmtEngineStatistics;
+
 /**
  * Module in charge of expanding definitions for an SMT engine.
  *

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 09ddfde7555699545e9f9ec6f33ec5d02f50a594..965f49855bec1ecea0bd8cede6febae5af1e909a 100644 (file)
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -14,6 +14,8 @@
 
 #include "smt/interpolation_solver.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/quantifiers_attributes.h"

diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h
index d4cf33554db23cf6034e56d2a5a1d870dc79ec20..2482f77ef241aac2183d682ef13a479b8d4e88f9 100644 (file)
--- a/src/smt/managed_ostreams.h
+++ b/src/smt/managed_ostreams.h
@@ -22,11 +22,10 @@
 
 #include <ostream>
 
-#include "options/open_ostream.h"
-#include "smt/update_ostream.h"
-
 namespace CVC4 {
 
+class OstreamOpener;
+
 /** This abstracts the management of ostream memory and initialization. */
 class ManagedOstream {
  public:

diff --git a/src/smt/model.h b/src/smt/model.h
index e7c2434a652624ea52165a3a044e5b5e30f13c37..277803499abf3d99d2517f91d53be7f16c1ab16e 100644 (file)
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -21,13 +21,15 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "theory/theory_model.h"
-#include "util/cardinality.h"
 
 namespace CVC4 {
 
 class SmtEngine;
 
+namespace theory {
+class TheoryModel;
+}
+
 namespace smt {
 
 class Model;

diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index cabd7bd203481219f70a165ab44aac0ee661a072..95c9f1d18510199368e037984315958a637a4284 100644 (file)
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -18,6 +18,8 @@
 #include "expr/node.h"
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
+#include "theory/theory_model.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 5c45a6a564c3a76f2b39f2b88d7d3e5e34296157..6c453987e658131c6d1f441e5263172ff0d29772 100644 (file)
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -21,10 +21,13 @@
 
 #include "expr/node.h"
 #include "options/smt_options.h"
-#include "theory/theory_model.h"
 
 namespace CVC4 {
 
+namespace theory {
+class TheoryModel;
+}
+
 /**
  * A utility for blocking the current model.
  */

diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index 33b5d995341d9399ddfad6de5ee189d74e64549e..3fc3a2e0c5aee8f2379ccd82f147461fa6413136 100644 (file)
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -16,6 +16,8 @@
 
 #include "smt/node_command.h"
 
+#include <sstream>
+
 #include "printer/printer.h"
 
 namespace CVC4 {

diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index 983b98b3492cf07768746d0bb3841b79c7ef03be..81b935f36a979686c0110e2f33a3368b93b995d0 100644 (file)
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -15,15 +15,15 @@
 #ifndef CVC4__SMT__OPTIONS_MANAGER_H
 #define CVC4__SMT__OPTIONS_MANAGER_H
 
-#include "options/options.h"
 #include "options/options_listener.h"
 #include "smt/managed_ostreams.h"
 
 namespace CVC4 {
 
-class SmtEngine;
 class LogicInfo;
+class Options;
 class ResourceManager;
+class SmtEngine;
 
 namespace smt {
 

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index ef80ebdae374bde2d6ecc12f8e39e9b34f844fcc..261450dbbe9b9bcfcb65da93b2eb79e998fa2025 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -16,6 +16,8 @@
 #include "smt/preprocess_proof_generator.h"
 
 #include "expr/proof.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
 #include "options/proof_options.h"
 #include "theory/rewriter.h"
 

diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 01d9c89da6e072ebcd53dfe1b592eb113705c769..312e58453337ffa048c43c26b0d60704607733c6 100644 (file)
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -20,12 +20,10 @@
 #include <map>
 
 #include "context/cdhashmap.h"
-#include "context/cdlist.h"
 #include "expr/lazy_proof.h"
 #include "expr/proof_set.h"
 #include "expr/proof_generator.h"
 #include "expr/proof_node_manager.h"
-#include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 
 namespace CVC4 {

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 3e4ef0cdd67f3c8ff7b840ab66cff21ecd4996d8..e5e9b98f44b3115f161edb4a7f1cb28559580b6a 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -19,8 +19,10 @@
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/dump.h"
+#include "smt/preprocess_proof_generator.h"
 #include "smt/smt_engine.h"
 
+using namespace std;
 using namespace CVC4::theory;
 using namespace CVC4::kind;
 

diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h
index 22b585e0543ac44f45807d8c2386c2b31dc9ef83..ece5fb5a8ce60443a36f6e158dbc0668a0177b56 100644 (file)
--- a/src/smt/preprocessor.h
+++ b/src/smt/preprocessor.h
@@ -17,14 +17,16 @@
 #ifndef CVC4__SMT__PREPROCESSOR_H
 #define CVC4__SMT__PREPROCESSOR_H
 
-#include <vector>
+#include <memory>
 
-#include "preprocessing/preprocessing_pass_context.h"
 #include "smt/expand_definitions.h"
 #include "smt/process_assertions.h"
 #include "theory/booleans/circuit_propagator.h"
 
 namespace CVC4 {
+namespace preprocessing {
+class PreprocessingPassContext;
+}
 namespace smt {
 
 class AbstractValues;

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 0c01abbbbe20b208b74f0d8d20a93da4647a8039..23890d9fc50554a76d320b61b97d6ad38638734a 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -31,10 +31,13 @@
 #include "printer/printer.h"
 #include "smt/defined_function.h"
 #include "smt/dump.h"
+#include "smt/expand_definitions.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/logic_info.h"
 #include "theory/theory_engine.h"
 
+using namespace std;
 using namespace CVC4::preprocessing;
 using namespace CVC4::theory;
 using namespace CVC4::kind;

diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h
index ca834459d48f33cda55a19c9291eea36f2c22cb1..891ef93f1043526cb7db66d600c3f1a1f91b6ad8 100644 (file)
--- a/src/smt/process_assertions.h
+++ b/src/smt/process_assertions.h
@@ -17,17 +17,14 @@
 #ifndef CVC4__SMT__PROCESS_ASSERTIONS_H
 #define CVC4__SMT__PROCESS_ASSERTIONS_H
 
-#include <map>
+#include <unordered_map>
 
-#include "context/cdhashmap.h"
 #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 "smt/expand_definitions.h"
-#include "smt/smt_engine_stats.h"
 #include "util/resource_manager.h"
 
 namespace CVC4 {
@@ -36,6 +33,9 @@ class SmtEngine;
 
 namespace smt {
 
+class ExpandDefs;
+struct SmtEngineStatistics;
+
 /**
  * Module in charge of processing assertions for an SMT engine.
  *
@@ -54,7 +54,7 @@ class ProcessAssertions
 {
   /** The types for the recursive function definitions */
   typedef context::CDList<Node> NodeList;
-  typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+  typedef std::unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
 
  public:
   ProcessAssertions(SmtEngine& smt,

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index cb7943aedff72695a46f66233bb4347a797f7a43..2f7683e7c5ad05fff475db388b47b898868a17a7 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -14,11 +14,15 @@
 
 #include "smt/proof_manager.h"
 
+#include "expr/proof_checker.h"
 #include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_manager.h"
 #include "options/base_options.h"
 #include "options/proof_options.h"
 #include "smt/assertions.h"
 #include "smt/defined_function.h"
+#include "smt/preprocess_proof_generator.h"
+#include "smt/proof_post_processor.h"
 
 namespace CVC4 {
 namespace smt {

diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index a6f284cade2a709a873cfeb7c8c4448691b782d9..abb984ea9009ec54bc57eb9c5439d50b45373f2c 100644 (file)
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -18,22 +18,21 @@
 #define CVC4__SMT__PROOF_MANAGER_H
 
 #include "context/cdhashmap.h"
-#include "context/cdlist.h"
 #include "expr/node.h"
-#include "expr/proof_checker.h"
-#include "expr/proof_node.h"
-#include "expr/proof_node_manager.h"
-#include "smt/preprocess_proof_generator.h"
-#include "smt/proof_post_processor.h"
 
 namespace CVC4 {
 
+class ProofChecker;
+class ProofNode;
+class ProofNodeManager;
 class SmtEngine;
 
 namespace smt {
 
 class Assertions;
 class DefinedFunction;
+class PreprocessProofGenerator;
+class ProofPostproccess;
 
 /**
  * This class is responsible for managing the proof output of SmtEngine, as

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 0898096f5dc6a0b94ff8a54cffec750a3cf60bec..f7811911b239e5edff40ec0de0cf2c05c6a54307 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/proof_post_processor.h"
 
+#include "expr/proof_node_manager.h"
 #include "expr/skolem_manager.h"
 #include "options/proof_options.h"
 #include "options/smt_options.h"

diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index de74d4869c34a41b9aac9696f3408abc68c7e86e..b3e636b581c4535a2012633642407fe023663113 100644 (file)
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -22,6 +22,7 @@
 
 #include "expr/proof_node_updater.h"
 #include "smt/witness_form.h"
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 80d7b96fabac6e7b1cfaedf21cd1b8f9029fb050..8913498093e8fdf299f16f0c5c4215306a27924e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -34,11 +34,13 @@
 #include "printer/printer.h"
 #include "proof/proof_manager.h"
 #include "proof/unsat_core.h"
+#include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
 #include "smt/assertions.h"
 #include "smt/check_models.h"
 #include "smt/defined_function.h"
+#include "smt/dump.h"
 #include "smt/dump_manager.h"
 #include "smt/interpolation_solver.h"
 #include "smt/listeners.h"

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8974e5e60e4e1623fcf49aba7d30f5eb2954f586..50e45c52f07727b9c33f2e537b84f5f3e1b12808 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -887,8 +887,6 @@ class CVC4_PUBLIC SmtEngine
   /* .......................................................................  */
  private:
   /* .......................................................................  */
-  /** The type of our internal assertion list */
-  typedef context::CDList<Node> AssertionList;
 
   // disallow copy/assignment
   SmtEngine(const SmtEngine&) = delete;

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 996a51e9057b0b66f6b09d2f92f551b42989dbfe..9b58711391db6e5959fe1af2f82d342929bbac9f 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -20,9 +20,12 @@
 #include "smt/preprocessor.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_state.h"
+#include "smt/smt_engine_stats.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_traits.h"
 
+using namespace std;
+
 namespace CVC4 {
 namespace smt {
 
@@ -67,12 +70,12 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo)
    * are unregistered by the obsolete PropEngine object before registered
    * again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
-                                    d_smt.getContext(),
-                                    d_smt.getUserContext(),
-                                    d_rm,
-                                    d_smt.getOutputManager(),
-                                    d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
+                                          d_smt.getContext(),
+                                          d_smt.getUserContext(),
+                                          d_rm,
+                                          d_smt.getOutputManager(),
+                                          d_pnm));
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(getPropEngine());
@@ -88,12 +91,12 @@ void SmtSolver::resetAssertions()
    * statistics are unregistered by the obsolete PropEngine object before
    * registered again by the new PropEngine object */
   d_propEngine.reset(nullptr);
-  d_propEngine.reset(new PropEngine(d_theoryEngine.get(),
-                                    d_smt.getContext(),
-                                    d_smt.getUserContext(),
-                                    d_rm,
-                                    d_smt.getOutputManager(),
-                                    d_pnm));
+  d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
+                                          d_smt.getContext(),
+                                          d_smt.getUserContext(),
+                                          d_rm,
+                                          d_smt.getOutputManager(),
+                                          d_pnm));
   d_theoryEngine->setPropEngine(getPropEngine());
   // Notice that we do not reset TheoryEngine, nor does it require calling
   // finishInit again. In particular, TheoryEngine::finishInit does not

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 5f08efb14df5c35f3fe8d2c41f2b4c91cee95e56..133d1e6925aeb873907893fd089adeb3ee89320f 100644 (file)
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -18,8 +18,11 @@
 #include <vector>
 
 #include "expr/attribute.h"
+#include "expr/lazy_proof.h"
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
+#include "expr/term_context_stack.h"
+#include "expr/term_conversion_proof_generator.h"
 #include "options/smt_options.h"
 #include "proof/proof_manager.h"
 

diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 803021fc349ccd49b400c0abc51af8ca4c6ff78e..c2a88d718f3e61298952bc6fb7774cd729b894ed 100644 (file)
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -18,22 +18,22 @@
 
 #pragma once
 
-#include <unordered_map>
+#include <unordered_set>
 #include <vector>
 
 #include "context/cdinsert_hashmap.h"
 #include "context/context.h"
-#include "expr/lazy_proof.h"
 #include "expr/node.h"
-#include "expr/term_context_stack.h"
-#include "expr/term_conversion_proof_generator.h"
-#include "theory/eager_proof_generator.h"
+#include "expr/term_context.h"
 #include "theory/trust_node.h"
-#include "util/bool.h"
 #include "util/hash.h"
 
 namespace CVC4 {
 
+class LazyCDProof;
+class ProofNodeManager;
+class TConvProofGenerator;
+
 class RemoveTermFormulas {
  public:
   RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr);

diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index f5a9a2a75de037a1e9d0c64a43a099f799bc3aa3..8107136c37bb37ae43d88648b11c05a8d35a56d6 100644 (file)
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -18,6 +18,8 @@
 
 #include "theory/arith/delta_rational.h"
 
+#include <sstream>
+
 using namespace std;
 
 namespace CVC4 {

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 6487b48eccea8e0913a5c815a6e140e4cd7042e0..5e34aebc79ba947c17ac060f13ad761580628325 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -22,6 +22,7 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/nl_model.h"
+#include "theory/rewriter.h"
 #include "util/iand.h"
 
 using namespace CVC4::kind;

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index bc4e0c8ae942434d5bdadd37ae5608d7ba50bb4e..01b834482e0cb58e6e51ac26bc518e73d2201009 100644 (file)
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/booleans/proof_circuit_propagator.h"
 
+#include <sstream>
+
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {

diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index d71fae8d00a2e3f4a16898dc116a0f9c59d5efed..a1763d081c383431dcf434c4c3738acc25445c67 100644 (file)
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -31,6 +31,7 @@
 #include "prop/sat_solver_types.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
+#include "theory/theory.h"
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 

diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 4eec45e4b87d186f5c0edd1ba69f5cfb8a27de7f..94f74a638c92cfb197c15155f03c0be41f4d633b 100644 (file)
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -21,6 +21,7 @@
 
 #include <unordered_map>
 
+#include "context/cdqueue.h"
 #include "prop/cnf_stream.h"
 #include "prop/sat_solver.h"
 #include "theory/bv/bitblast/simple_bitblaster.h"

diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp
index 6169d375250ce79601fe8a7c6614b1af47d0befb..e11f773a3c70ce1142e19fa8ae35bb7ae6c53d91 100644 (file)
--- a/src/theory/datatypes/sygus_datatype_utils.cpp
+++ b/src/theory/datatypes/sygus_datatype_utils.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/datatypes/sygus_datatype_utils.h"
 
+#include <sstream>
+
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9105cdfd6c1dd1b106034b84ee768a0c7d07f576..97600f76fbc2c7dcf711b91eee3d554cb8c929bb 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -16,6 +16,7 @@
 #include "theory/datatypes/theory_datatypes.h"
 
 #include <map>
+#include <sstream>
 
 #include "base/check.h"
 #include "expr/dtype.h"

diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp
index fda694e3da742c9b540c556a795849e0cdc182c2..94f90bc468f73398371363e5ff6ac8a6431ae7a5 100644 (file)
--- a/src/theory/inference_id.cpp
+++ b/src/theory/inference_id.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/inference_id.h"
 
+#include <iostream>
+
 namespace CVC4 {
 namespace theory {
 

diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/theory/lazy_tree_proof_generator.cpp
index 126ce60b9680d0f14a109a232e80c8ee3df25af2..b6155f19e8bbc9f2ed984499df3e2019771ad8d2 100644 (file)
--- a/src/theory/lazy_tree_proof_generator.cpp
+++ b/src/theory/lazy_tree_proof_generator.cpp
@@ -18,6 +18,7 @@
 
 #include "expr/node.h"
 #include "expr/proof_generator.h"
+#include "expr/proof_node.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {

diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index f1307f1425cc6ee454cbb6302d2e437277f41ad3..842ef59bf944c1168e0902ce68492d72e766c666 100644 (file)
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -14,6 +14,8 @@
  **/
 #include "theory/quantifiers/single_inv_partition.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index cdc43658d604a2af24f5d7023b712496f3587955..69adc9a4b6b7d5c9d2714d6919acf74ecf8a1998 100644 (file)
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -18,11 +18,12 @@
 #define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
 
 #include <unordered_set>
+
 #include "expr/node.h"
 #include "expr/node_trie.h"
-
 #include "theory/evaluator.h"
 #include "theory/quantifiers/sygus/cegis.h"
+#include "util/result.h"
 
 namespace CVC4 {
 namespace theory {

diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 67f02b558255458bf8b614a8d9731dfbded8843c..e56312362eaec4cb8d05a692ea0beee3a9067856 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -15,6 +15,8 @@
 
 #include "theory/quantifiers/sygus/sygus_abduct.h"
 
+#include <sstream>
+
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "expr/sygus_datatype.h"

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 3edec96c71529504ed2fc1d4898a2e8cf29a3253..9f8ac0e3cf51a67b186b33b7d23fcf36168bc139 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/quantifiers/sygus/sygus_interpol.h"
 
+#include <sstream>
+
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/smt_options.h"

diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp
index ca87e1049d654a025887d1ad8d2ac7514535395b..d793fb718ddd63b58d29cb3e7f9389eb4ae2c6e5 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_utils.cpp
+++ b/src/theory/quantifiers/sygus/sygus_utils.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/quantifiers/sygus/sygus_utils.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 275e9a27f34f50d83d7b883ebb6659c76801bfd1..a5be5871faf0f7b18e9174694eb6438c29a83559 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4::kind;
 

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index a72054f6d53594ac4bdcf42cff79e752dc10bfd0..c835369b77ee8355e80b222204718f007c9d8fce 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/lazy_trie.h"
+#include "theory/rewriter.h"
 #include "util/bitvector.h"
 #include "util/random.h"
 #include "util/sampler.h"

diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 24d2e00bdfe4076bcab0695c799f2587445605d0..21480e8ecd5dfeb30bf60feb4c1359c26df236fa 100644 (file)
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/strings/regexp_operation.h"
 
+#include <sstream>
+
 #include "expr/node_algorithm.h"
 #include "options/strings_options.h"
 #include "theory/rewriter.h"

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index b807fe1b3193cdee0fc8a1fb1a1bc85ef829208b..4338d38c4790d018faa116c38d5e20a128484b5e 100644 (file)
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/strings/theory_strings_utils.h"
 
+#include <sstream>
+
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e49ca8b05ff161ab714c4e7ae5e38b005f021e7c..07b23525e780b9a9daf9149eb26f5abef4646447 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/theory_engine.h"
 
+#include <sstream>
+
 #include "base/map_util.h"
 #include "decision/decision_engine.h"
 #include "expr/attribute.h"

diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp
index 2ba0a49ff8ec82782b1f03e1d591b9c3df824ba3..1eb191fd7437ffb05a541fc3fe525bef418ac0be 100644 (file)
--- a/src/theory/theory_engine_proof_generator.cpp
+++ b/src/theory/theory_engine_proof_generator.cpp
@@ -14,6 +14,10 @@
 
 #include "theory/theory_engine_proof_generator.h"
 
+#include <sstream>
+
+#include "expr/proof_node.h"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {

diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index e9111db8c164d021879d943579285dc6fdc10907..5859b5c997db9fd558ba201879bf6dbea3ed5d69 100644 (file)
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -17,6 +17,8 @@
 
 #include "theory/theory_id.h"
 
+#include <sstream>
+
 #include "base/check.h"
 #include "lib/ffs.h"
 

diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 94402e2d9af7a61945fbea983f031b025c678bdc..d2fc4cf9e7cc054e1b91018ff30f66493e48c9ad 100644 (file)
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/uf/cardinality_extension.h"
 
+#include <sstream>
+
 #include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "theory/quantifiers/term_database.h"

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

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index db8b89d895e9cd2f5258de98842b1daac82f5caa..e6e8095331c315d7e6ddb9110f81e5e09f9c7734 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -18,6 +18,7 @@
 #include "theory/uf/theory_uf.h"
 
 #include <memory>
+#include <sstream>
 
 #include "expr/node_algorithm.h"
 #include "expr/proof_node_manager.h"

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index b1a27929ac8f50a407b6e52cd28865d756586591..a5ef3a6071c45682285b623baebace8810289e9f 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -20,7 +20,9 @@
 #define CVC4__BITVECTOR_H
 
 #include <iosfwd>
+#include <iostream>
 
+#include "base/exception.h"
 #include "util/integer.h"
 
 namespace CVC4 {

diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index f78b076deeddb205cff0f323318140e08ce87728..bf3a8ef2baf99c9321fc4ee7a4af910242ee8870 100644 (file)
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -17,6 +17,7 @@
 #include "util/cardinality.h"
 
 #include <ostream>
+#include <sstream>
 
 #include "base/check.h"
 #include "base/exception.h"

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index fe05dc982788c6d3419caf42d6a90da6b50e6fd9..cca141094797ea5640f2424d68ac8c85fcdba8fa 100644 (file)
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -20,13 +20,11 @@
 #ifndef CVC4__INTEGER_H
 #define CVC4__INTEGER_H
 
+#include <gmpxx.h>
+
 #include <iosfwd>
-#include <limits>
 #include <string>
 
-#include "base/exception.h"
-#include "util/gmp_util.h"
-
 namespace CVC4 {
 
 class Rational;

diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp
index ad769b7793a144e3a4ff215aad51c8ebaf71c8d0..2e2f200a3a07fc4de9f8391d790d226cfe8b75d3 100644 (file)
--- a/src/util/poly_util.cpp
+++ b/src/util/poly_util.cpp
@@ -27,6 +27,7 @@
 #include <poly/polyxx.h>
 
 #include <map>
+#include <sstream>
 
 #include "base/check.h"
 #include "maybe.h"

diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index f166d9cdc3f00c45a57eea99202350ce53565b21..f6c9a1e444bf46909d02a88c9d9c4dd2036e1d1a 100644 (file)
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -24,7 +24,7 @@
 
 #include <string>
 
-#include "base/exception.h"
+#include "util/gmp_util.h"
 #include "util/integer.h"
 #include "util/maybe.h"
 

diff --git a/src/util/result.cpp b/src/util/result.cpp
index f4e4d13c7a6fda03a271537a597526f3bff5e45b..09445fa3bff5c677b72fd5f040e857e5d127246d 100644 (file)
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -18,6 +18,7 @@
 #include <algorithm>
 #include <cctype>
 #include <iostream>
+#include <sstream>
 #include <string>
 
 #include "base/check.h"

diff --git a/src/util/result.h b/src/util/result.h
index 96fe919d05ada73017f605329d1d8929df237c6c..d0b0896bc27a82754f04e3a62f78743ea102f56f 100644 (file)
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -19,10 +19,9 @@
 #ifndef CVC4__RESULT_H
 #define CVC4__RESULT_H
 
-#include <iostream>
+#include <iosfwd>
 #include <string>
 
-#include "base/exception.h"
 #include "options/language.h"
 
 namespace CVC4 {

diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp
index f45849736df98cc8664eaffd3987b0eff95d5844..aa2918cde6441833562be1521215a1f25760393d 100644 (file)
--- a/src/util/safe_print.cpp
+++ b/src/util/safe_print.cpp
@@ -20,8 +20,11 @@
 
 #include "safe_print.h"
 
+#include <time.h>
 #include <unistd.h>
 
+#include <cstdlib>
+
 /* Size of buffers used */
 #define BUFFER_SIZE 20
 

diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index 6f72569bb90a15b5ec8d1219216a93c3a9b8966e..b98b4f3e92eca25d0c3121ed7b02d7a35c7924d8 100644 (file)
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -40,10 +40,7 @@
 #include <unistd.h>
 
 #include <cstring>
-#include <type_traits>
-
-#include "lib/clock_gettime.h"
-#include "util/result.h"
+#include <string>
 
 namespace CVC4 {
 

diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp
index 20dfb92a73920ce68ce36881dbb74c9fd4e1b166..8b1a2c3db450b1ab3dc525a3b55ad9ae67ada6cb 100644 (file)
--- a/src/util/sampler.cpp
+++ b/src/util/sampler.cpp
@@ -17,8 +17,11 @@
 
 #include "util/sampler.h"
 
+#include <sstream>
+
 #include "base/check.h"
 #include "util/bitvector.h"
+#include "util/random.h"
 
 namespace CVC4 {
 

diff --git a/src/util/sampler.h b/src/util/sampler.h
index 8968f5dc771fd3bd8fb2361f28ef3ca68af3cafd..dad6605a54ce339d12091b569a64712565b31716 100644 (file)
--- a/src/util/sampler.h
+++ b/src/util/sampler.h
@@ -21,7 +21,6 @@
 #define CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
 
 #include "util/floatingpoint.h"
-#include "util/random.h"
 
 namespace CVC4 {
 

diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 3bcf36abfe7aa5122ce368149396f1b9d44e7e54..5c47fa4fdcfd4d409905bdc915330f89cc247aee 100644 (file)
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -26,12 +26,10 @@
 #ifndef CVC4__SEXPR_H
 #define CVC4__SEXPR_H
 
-#include <iomanip>
 #include <iosfwd>
 #include <string>
 #include <vector>
 
-#include "base/exception.h"
 #include "options/language.h"
 #include "util/integer.h"
 #include "util/rational.h"

diff --git a/src/util/string.h b/src/util/string.h
index 9e503bb0771f29b79631fe69202717564ac7f9e1..f908c2f0fa1b4b7bb7f6782f949835b7bf6f3d04 100644 (file)
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -17,10 +17,10 @@
 #ifndef CVC4__UTIL__STRING_H
 #define CVC4__UTIL__STRING_H
 
-#include <functional>
-#include <ostream>
+#include <iosfwd>
 #include <string>
 #include <vector>
+
 #include "util/rational.h"
 
 namespace CVC4 {

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 1a3412186f23ea1c548610ca18bcd2188bbb0aa4..5e2e80e4aa59214dd54be3694ecfa96143e162e3 100644 (file)
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -20,6 +20,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/passes/bv_gauss.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"

diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index 569c8a0e123d4f7be9fcae8a7b7cc0c37acb0649..ceaf694230662d0089e723be7032482c75cbeb35 100644 (file)
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -19,6 +19,7 @@
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
 #include "prop/registrar.h"
+#include "prop/sat_solver.h"
 #include "prop/theory_proxy.h"
 #include "test_smt.h"
 #include "theory/arith/theory_arith.h"

diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp
index 8329658360ed8e1d730d5b9197fb5a6844ab795e..c5ffe0b8700945115e0ac3d77da9672e309c6018 100644 (file)
--- a/test/unit/util/cardinality_black.cpp
+++ b/test/unit/util/cardinality_black.cpp
@@ -17,6 +17,7 @@
 #include <sstream>
 #include <string>
 
+#include "base/exception.h"
 #include "test.h"
 #include "util/cardinality.h"
 #include "util/integer.h"

diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp
index 41497a7a47e9ededc132f52d52b3f2b03819292b..f447246e2ea613cf30d94cd1c4563b0ecef9d229 100644 (file)
--- a/test/unit/util/integer_black.cpp
+++ b/test/unit/util/integer_black.cpp
@@ -17,6 +17,7 @@
 #include <limits>
 #include <sstream>
 
+#include "base/exception.h"
 #include "test.h"
 #include "util/integer.h"