whitespace fixes

5 files changed, 29 insertions, 29 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index c3b2f28ac..d7d463d79 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -49,14 +49,14 @@ void DecisionEngine::init()
   d_engineState = 1;
 
   Trace("decision-init") << "DecisionEngine::init()" << std::endl;
-  Trace("decision-init") << " * options->decisionMode: " 
+  Trace("decision-init") << " * options->decisionMode: "
                          << options::decisionMode() << std:: endl;
   Trace("decision-init") << " * options->decisionStopOnly: "
                          << options::decisionStopOnly() << std::endl;
 
   if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
   if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
-    ITEDecisionStrategy* ds = 
+    ITEDecisionStrategy* ds =
       new decision::JustificationHeuristic(this, d_userContext, d_satContext);
     enableStrategy(ds);
     d_needIteSkolemMap.push_back(ds);
@@ -107,7 +107,7 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions)
   // d_result = SAT_VALUE_UNKNOWN;
   // d_assertions.reserve(assertions.size());
   // for(unsigned i = 0; i < assertions.size(); ++i)
-  //   d_assertions.push_back(assertions[i]); 
+  //   d_assertions.push_back(assertions[i]);
 }
 
 void DecisionEngine::addAssertions(const vector<Node> &assertions,
@@ -116,11 +116,11 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions,
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
-  
+
   // d_assertions.reserve(assertions.size());
   for(unsigned i = 0; i < assertions.size(); ++i)
     d_assertions.push_back(assertions[i]);
-  
+
   for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
     d_needIteSkolemMap[i]->
       addAssertions(assertions, assertionsEnd, iteSkolemMap);
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index bfd28e113..39ed89a68 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -71,7 +71,7 @@ public:
   ~DecisionEngine() {
     Trace("decision") << "Destroying decision engine" << std::endl;
   }
-  
+
   // void setPropEngine(PropEngine* pe) {
   //   // setPropEngine should not be called more than once
   //   Assert(d_propEngine == NULL);
@@ -123,8 +123,8 @@ public:
            "Forgot to set satSolver for decision engine?");
 
     SatLiteral ret = undefSatLiteral;
-    for(unsigned i = 0; 
-        i < d_enabledStrategies.size() 
+    for(unsigned i = 0;
+        i < d_enabledStrategies.size()
           and ret == undefSatLiteral
           and stopSearch == false; ++i) {
       ret = d_enabledStrategies[i]->getNext(stopSearch);
@@ -137,7 +137,7 @@ public:
 
   /**
    * Try to get tell SAT solver what polarity to try for a
-   * decision. Return SAT_VALUE_UNKNOWN if it can't help 
+   * decision. Return SAT_VALUE_UNKNOWN if it can't help
    */
   SatValue getPolarity(SatVariable var);
 
@@ -193,7 +193,7 @@ public:
   // (which was possibly requested by them on initialization)
 
   /**
-   * Get the assertions. Strategies are notified when these are available. 
+   * Get the assertions. Strategies are notified when these are available.
    */
   AssertionsList& getAssertions() {
     return d_assertions;
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index e4df8d4af..94db110c2 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -43,9 +43,9 @@ public:
   virtual ~DecisionStrategy() { }
 
   virtual prop::SatLiteral getNext(bool&) = 0;
-  
+
   virtual bool needIteSkolemMap() { return false; }
-  
+
   virtual void notifyAssertionsAvailable() { return; }
 };/* class DecisionStrategy */
 
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index ffff6952f..84f4d5074 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -124,7 +124,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
 
     if(Debug.isOn("decision")) {
       if(!checkJustified(curass))
-        Debug("decision") << "****** Not justified [i="<<i<<"]: " 
+        Debug("decision") << "****** Not justified [i="<<i<<"]: "
                           << d_assertions[i] << std::endl;
     }
   }
@@ -169,7 +169,7 @@ void JustificationHeuristic::addAssertions
  IteSkolemMap iteSkolemMap) {
 
   Trace("decision")
-    << "JustificationHeuristic::addAssertions()" 
+    << "JustificationHeuristic::addAssertions()"
     << " size = " << assertions.size()
     << " assertionsEnd = " << assertionsEnd
     << std::endl;
@@ -182,7 +182,7 @@ void JustificationHeuristic::addAssertions
   for(IteSkolemMap::iterator i = iteSkolemMap.begin();
       i != iteSkolemMap.end(); ++i) {
 
-    Trace("decision::jh::ite") 
+    Trace("decision::jh::ite")
       << " jh-ite: " << (i->first) << " maps to "
       << assertions[(i->second)] << std::endl;
     Assert(i->second >= assertionsEnd && i->second < assertions.size());
@@ -199,7 +199,7 @@ SatLiteral JustificationHeuristic::findSplitter(TNode node,
   d_curDecision = undefSatLiteral;
   if(findSplitterRec(node, desiredVal)) {
     ++d_helfulness;
-  } 
+  }
   return d_curDecision;
 }
 
@@ -405,9 +405,9 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
    * children to be true. this is done recursively.
    */
 
-  Trace("decision::jh") 
-    << "findSplitterRec(" << node << ", " 
-    << desiredVal << ", .. )" << std::endl; 
+  Trace("decision::jh")
+    << "findSplitterRec(" << node << ", "
+    << desiredVal << ", .. )" << std::endl;
 
   /* Handle NOT as a special case */
   while (node.getKind() == kind::NOT) {
@@ -417,7 +417,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
 
   /* Base case */
   if (checkJustified(node)) {
-    Debug("decision::jh") << "  justified, returning" << std::endl; 
+    Debug("decision::jh") << "  justified, returning" << std::endl;
     return NO_SPLITTER;
   }
   if (getExploredThreshold(node) < d_curThreshold) {
@@ -449,7 +449,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
   //       "invariant violated");
 
   /* What type of node is this */
-  Kind k = node.getKind();	
+  Kind k = node.getKind();
   theory::TheoryId tId = theory::kindToTheoryId(k);
 
   /* Some debugging stuff */
@@ -470,7 +470,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
       Assert(litVal == desiredVal);
       setJustified(node);
       return NO_SPLITTER;
-    } 
+    }
     else {
       Assert(d_decisionEngine->hasSatLiteral(node));
       if(d_curThreshold != 0 && getWeightPolarized(node, desiredVal) >= d_curThreshold)
@@ -548,7 +548,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
 JustificationHeuristic::SearchResult
 JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal)
 {
-  Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or 
+  Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or
           (node.getKind() == kind::OR  and desiredVal == SAT_VALUE_TRUE) );
 
   int numChildren = node.getNumChildren();
@@ -575,7 +575,7 @@ void JustificationHeuristic::saveStartIndex(TNode node, int val) {
 
 JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node,
                                              SatValue desiredVal) {
-  Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or 
+  Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or
           (node.getKind() == kind::OR  and desiredVal == SAT_VALUE_FALSE) );
 
   int numChildren = node.getNumChildren();
@@ -671,7 +671,7 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod
 
     if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER)
       return FOUND_SPLITTER;
-    
+
     Assert(d_curThreshold != 0, "No controlling input found (6)");
     return DONT_KNOW;
   } else {
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index a6bc68ce5..9177ba44d 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -127,10 +127,10 @@ private:
   prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
 
   SatLiteral findSplitter(TNode node, SatValue desiredVal);
-  
-  /** 
-   * Do all the hard work. 
-   */ 
+
+  /**
+   * Do all the hard work.
+   */
   SearchResult findSplitterRec(TNode node, SatValue value);
 
   /* Helper functions */