From: Kshitij Bansal Date: Tue, 9 Sep 2014 20:24:15 +0000 (-0400) Subject: whitespace fixes X-Git-Tag: cvc5-1.0.0~6580 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=461a416e254095f4bdb4b3f5f4f3258b52722e23;p=cvc5.git whitespace fixes --- 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 &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 &assertions, @@ -116,11 +116,11 @@ void DecisionEngine::addAssertions(const vector &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="<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 */ diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h index a4f3f6a6d..dc5feecda 100644 --- 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(true); std::set terms; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 8db4c5688..810a718b9 100644 --- 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 3d93adb48..536987073 100644 --- 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);