diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2019-03-27 11:33:07 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-07-01 15:52:40 +0100 |
commit | a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0 (patch) | |
tree | 878d75da74e7a6ae4a917c41ed482fc5c0ffe3e0 /lib/Solver/FastCexSolver.cpp | |
parent | f56c7aa2a7200ece5d074651b9839eb917f910f5 (diff) | |
download | klee-a1b73df93e5a2fac4a7ac87fb1753c4eb518c8c0.tar.gz |
Separate constraint set and constraint manager
Diffstat (limited to 'lib/Solver/FastCexSolver.cpp')
-rw-r--r-- | lib/Solver/FastCexSolver.cpp | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index d3062407..a45a8f17 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -1007,10 +1007,9 @@ FastCexSolver::~FastCexSolver() { } /// \return - True if the propogation was able to prove validity or invalidity. static bool propogateValues(const Query& query, CexData &cd, bool checkExpr, bool &isValid) { - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - cd.propogatePossibleValue(*it, 1); - cd.propogateExactValue(*it, 1); + for (const auto &constraint : query.constraints) { + cd.propogatePossibleValue(constraint, 1); + cd.propogateExactValue(constraint, 1); } if (checkExpr) { cd.propogatePossibleValue(query.expr, 0); @@ -1032,14 +1031,13 @@ static bool propogateValues(const Query& query, CexData &cd, } } - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); it != ie; ++it) { - if (hasSatisfyingAssignment && !cd.evaluatePossible(*it)->isTrue()) + for (const auto &constraint : query.constraints) { + if (hasSatisfyingAssignment && !cd.evaluatePossible(constraint)->isTrue()) hasSatisfyingAssignment = false; // If this constraint is known to be false, then we can prove anything, so // the query is valid. - if (cd.evaluateExact(*it)->isFalse()) { + if (cd.evaluateExact(constraint)->isFalse()) { isValid = true; return true; } |