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.

4 files changed, 86 insertions, 69 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index e1327c0a7..2cebfa447 100644
--- 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 914636fe9..74a230e29 100644
--- 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 1d0b386e3..4950f4f3d 100644
--- 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 0a16759e1..1cf2810fd 100644
--- 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 */