whitespace fixes

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index c3b2f28acf91c87b2d4bfc1a3082b113a45ea614..d7d463d79e7f1344e00e02b68ccfc9843540ae7e 100644 (file)
--- 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 bfd28e1131735f40e475c9e441f2aed0fc4ecd87..39ed89a684aed395c9f24b8eaf50bd97970a5cf3 100644 (file)
--- 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 e4df8d4af04a1c00af42be6f425e84dfecd07453..94db110c2a3e896e2ece34e8734df92775d5e968 100644 (file)
--- 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 ffff6952ff80e02b84540d30588915925b254b9a..84f4d507460c9d4febb540ea206f370e5dcd6c28 100644 (file)
--- 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 a6bc68ce560fdcbd9e365c2b6b0aa397dfb59205..9177ba44d64c533fab5592b6ccf3f124791d4ab2 100644 (file)
--- 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 */

diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h
index a4f3f6a6db5a234c8dd65572b510a0bf1ce79ed5..dc5feecda4313d075ab1f40d4ea42f9f7ebeaeb2 100644 (file)
--- a/src/theory/sets/scrutinize.h
+++ b/src/theory/sets/scrutinize.h
@@ -35,11 +35,11 @@ public:
   }
   void postCheckInvariants() const {
     Debug("sets-scrutinize") << "[sets-scrutinize] postCheckInvariants()" << std::endl;
-    
+
     // assume not in conflict, and complete:
     // - try building model
     // - check it
-    
+
     TheorySetsPrivate::SettermElementsMap settermElementsMap;
     TNode true_atom = NodeManager::currentNM()->mkConst<bool>(true);
     std::set<Node> terms;

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 8db4c568865f8fa93732b4f0eac3f1c6131b3ed7..810a718b9e40485ac53d90d1124d37080e8c5764 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -553,7 +553,7 @@ void TheorySetsPrivate::computeCareGraph() {
         }
        if(Debug.isOn("sets-care")) {
          Debug("sets-care") << "[sets-care] Requesting split between" << a << " and "
-                            << b << "." << std::endl << "[sets-care] " 
+                            << b << "." << std::endl << "[sets-care] "
                             << "  Both current have value "
                             << d_external.d_valuation.getModelValue(a) << std::endl;
        }

diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 3d93adb48fcb0595a41cff619f0f5b70fd3783df..5369870737ddccef34f641b8c2665532a245e86d 100644 (file)
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -47,7 +47,7 @@ public:
                     context::UserContext* u);
 
   ~TheorySetsPrivate();
-  
+
   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 
   void addSharedTerm(TNode);