diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-12-23 12:19:22 +0000 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-12-23 12:24:57 +0000 |
commit | 29d010c291558a4199b5116d312f32cad86807e7 (patch) | |
tree | 63e0385119d2a026f0d1fff720cb55eb97dce125 /lib/Solver | |
parent | 2287eb0d44bedd20484874da06615ace3ce4e2a2 (diff) | |
download | klee-29d010c291558a4199b5116d312f32cad86807e7.tar.gz |
[NFC]
Reformat ``getAllIndependentConstraintsSets()`` using clang-format. It was not formatted correctly and was consequently a little hard to read. Also add braces around a for loop body. The original code for this function came from d9bcbba2c94086039c11c86200670639ee2ec19f
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 70 |
1 files changed, 38 insertions, 32 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index a7685e46..6b5a5586 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -258,53 +258,59 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, // Breaks down a constraint into all of it's individual pieces, returning a // list of IndependentElementSets or the independent factors. -static -void getAllIndependentConstraintsSets(const Query& query, - std::list<IndependentElementSet> * &factors){ +static void +getAllIndependentConstraintsSets(const Query &query, + std::list<IndependentElementSet> *&factors) { ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr); - if (CE){ - assert(CE && CE->isFalse() && - "the expr should always be false and therefore not included in factors"); + if (CE) { + assert(CE && CE->isFalse() && "the expr should always be false and " + "therefore not included in factors"); } else { ref<Expr> neg = Expr::createIsZero(query.expr); factors->push_back(IndependentElementSet(neg)); } for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) + ie = query.constraints.end(); + it != ie; ++it) { // iterate through all the previously separated constraints. Until we // actually return, factors is treated as a queue of expressions to be // evaluated. If the queue property isn't maintained, then the exprs // could be returned in an order different from how they came it, negatively // affecting later stages. factors->push_back(IndependentElementSet(*it)); - bool doneLoop = false; - do { - doneLoop = true; - std::list<IndependentElementSet> * done = new std::list<IndependentElementSet>; - while (factors->size() > 0){ - IndependentElementSet current = factors->front(); + } + + bool doneLoop = false; + do { + doneLoop = true; + std::list<IndependentElementSet> *done = + new std::list<IndependentElementSet>; + while (factors->size() > 0) { + IndependentElementSet current = factors->front(); + factors->pop_front(); + // This list represents the set of factors that are separate from current. + // Those that are not inserted into this list (queue) intersect with + // current. + std::list<IndependentElementSet> *keep = + new std::list<IndependentElementSet>; + while (factors->size() > 0) { + IndependentElementSet compare = factors->front(); factors->pop_front(); - // This list represents the set of factors that are separate from current. - // Those that are not inserted into this list (queue) intersect with current. - std::list<IndependentElementSet> *keep = new std::list<IndependentElementSet>; - while (factors->size() > 0){ - IndependentElementSet compare = factors->front(); - factors->pop_front(); - if (current.intersects(compare)){ - if (current.add(compare)){ - // Means that we have added (z=y)added to (x=y) - // Now need to see if there are any (z=?)'s - doneLoop = false; - } - } else { - keep->push_back(compare); - } - } - done->push_back(current); - delete factors; - factors = keep; + if (current.intersects(compare)) { + if (current.add(compare)) { + // Means that we have added (z=y)added to (x=y) + // Now need to see if there are any (z=?)'s + doneLoop = false; + } + } else { + keep->push_back(compare); + } } + done->push_back(current); + delete factors; + factors = keep; + } delete factors; factors = done; } while (!doneLoop); |