aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/AssignmentValidatingSolver.cpp20
-rw-r--r--lib/Solver/CachingSolver.cpp8
-rw-r--r--lib/Solver/FastCexSolver.cpp14
-rw-r--r--lib/Solver/IndependentSolver.cpp29
-rw-r--r--lib/Solver/MetaSMTSolver.cpp14
-rw-r--r--lib/Solver/Solver.cpp7
-rw-r--r--lib/Solver/ValidatingSolver.cpp10
7 files changed, 42 insertions, 60 deletions
diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp
index 7e1ccd38..54d6ec8c 100644
--- a/lib/Solver/AssignmentValidatingSolver.cpp
+++ b/lib/Solver/AssignmentValidatingSolver.cpp
@@ -63,10 +63,7 @@ bool AssignmentValidatingSolver::computeInitialValues(
// we can't compute a constant and flag this as a problem.
Assignment assignment(objects, values, /*_allowFreeValues=*/true);
// Check computed assignment satisfies query
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end();
- it != ie; ++it) {
- ref<Expr> constraint = *it;
+ for (const auto &constraint : query.constraints) {
ref<Expr> constraintEvaluated = assignment.evaluate(constraint);
ConstantExpr *CE = dyn_cast<ConstantExpr>(constraintEvaluated);
if (CE == NULL) {
@@ -124,16 +121,13 @@ void AssignmentValidatingSolver::dumpAssignmentQuery(
const Query &query, const Assignment &assignment) {
// Create a Query that is augmented with constraints that
// enforce the given assignment.
- std::vector<ref<Expr> > constraints;
- assignment.createConstraintsFromAssignment(constraints);
+ auto constraints = assignment.createConstraintsFromAssignment();
+
// Add Constraints from `query`
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end();
- it != ie; ++it) {
- constraints.push_back(*it);
- }
- ConstraintManager augmentedConstraints(constraints);
- Query augmentedQuery(augmentedConstraints, query.expr);
+ for (const auto &constraint : query.constraints)
+ constraints.push_back(constraint);
+
+ Query augmentedQuery(constraints, query.expr);
// Ask the solver for the log for this query.
char *logText = solver->getConstraintLog(augmentedQuery);
diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp
index 5e2d45a2..4a4c8e28 100644
--- a/lib/Solver/CachingSolver.cpp
+++ b/lib/Solver/CachingSolver.cpp
@@ -32,13 +32,13 @@ private:
IncompleteSolver::PartialValidity &result);
struct CacheEntry {
- CacheEntry(const ConstraintManager &c, ref<Expr> q)
- : constraints(c), query(q) {}
+ CacheEntry(const ConstraintSet &c, ref<Expr> q)
+ : constraints(c), query(q) {}
CacheEntry(const CacheEntry &ce)
: constraints(ce.constraints), query(ce.query) {}
-
- ConstraintManager constraints;
+
+ ConstraintSet constraints;
ref<Expr> query;
bool operator==(const CacheEntry &b) const {
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;
}
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 72623645..62632cd0 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -271,15 +271,13 @@ getAllIndependentConstraintsSets(const Query &query) {
factors->push_back(IndependentElementSet(neg));
}
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end();
- it != ie; ++it) {
+ for (const auto &constraint : query.constraints) {
// 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));
+ factors->push_back(IndependentElementSet(constraint));
}
bool doneLoop = false;
@@ -325,9 +323,9 @@ IndependentElementSet getIndependentConstraints(const Query& query,
IndependentElementSet eltsClosure(query.expr);
std::vector< std::pair<ref<Expr>, IndependentElementSet> > worklist;
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end(); it != ie; ++it)
- worklist.push_back(std::make_pair(*it, IndependentElementSet(*it)));
+ for (const auto &constraint : query.constraints)
+ worklist.push_back(
+ std::make_pair(constraint, IndependentElementSet(constraint)));
// XXX This should be more efficient (in terms of low level copy stuff).
bool done = false;
@@ -355,11 +353,10 @@ IndependentElementSet getIndependentConstraints(const Query& query,
errs() << "Q: " << query.expr << "\n";
errs() << "\telts: " << IndependentElementSet(query.expr) << "\n";
int i = 0;
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end(); it != ie; ++it) {
- errs() << "C" << i++ << ": " << *it;
- errs() << " " << (reqset.count(*it) ? "(required)" : "(independent)") << "\n";
- errs() << "\telts: " << IndependentElementSet(*it) << "\n";
+ for (const auto &constraint: query.constraints) {
+ errs() << "C" << i++ << ": " << constraint;
+ errs() << " " << (reqset.count(constraint) ? "(required)" : "(independent)") << "\n";
+ errs() << "\telts: " << IndependentElementSet(constraint) << "\n";
}
errs() << "elts closure: " << eltsClosure << "\n";
);
@@ -415,7 +412,7 @@ bool IndependentSolver::computeValidity(const Query& query,
std::vector< ref<Expr> > required;
IndependentElementSet eltsClosure =
getIndependentConstraints(query, required);
- ConstraintManager tmp(required);
+ ConstraintSet tmp(required);
return solver->impl->computeValidity(Query(tmp, query.expr),
result);
}
@@ -424,7 +421,7 @@ bool IndependentSolver::computeTruth(const Query& query, bool &isValid) {
std::vector< ref<Expr> > required;
IndependentElementSet eltsClosure =
getIndependentConstraints(query, required);
- ConstraintManager tmp(required);
+ ConstraintSet tmp(required);
return solver->impl->computeTruth(Query(tmp, query.expr),
isValid);
}
@@ -433,7 +430,7 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) {
std::vector< ref<Expr> > required;
IndependentElementSet eltsClosure =
getIndependentConstraints(query, required);
- ConstraintManager tmp(required);
+ ConstraintSet tmp(required);
return solver->impl->computeValue(Query(tmp, query.expr), result);
}
@@ -496,7 +493,7 @@ bool IndependentSolver::computeInitialValues(const Query& query,
if (arraysInFactor.size() == 0){
continue;
}
- ConstraintManager tmp(it->exprs);
+ ConstraintSet tmp(it->exprs);
std::vector<std::vector<unsigned char> > tempValues;
if (!solver->impl->computeInitialValues(Query(tmp, ConstantExpr::alloc(0, Expr::Bool)),
arraysInFactor, tempValues, hasSolution)){
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp
index fbb7da61..0f78bb5b 100644
--- a/lib/Solver/MetaSMTSolver.cpp
+++ b/lib/Solver/MetaSMTSolver.cpp
@@ -225,11 +225,9 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(
std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
// assume the constraints of the query
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end();
- it != ie; ++it) {
- assumption(_meta_solver, _builder->construct(*it));
- }
+ for (auto &constraint : query.constraints)
+ assumption(_meta_solver, _builder->construct(constraint));
+
// assume the negation of the query
assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));
hasSolution = solve(_meta_solver);
@@ -303,10 +301,8 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(
}
// assert constraints as we are in a child process
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end();
- it != ie; ++it) {
- assertion(_meta_solver, _builder->construct(*it));
+ for (const auto &constraint : query.constraints) {
+ assertion(_meta_solver, _builder->construct(constraint));
// assumption(_meta_solver, _builder->construct(*it));
}
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 855f7102..12cfb180 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -223,10 +223,9 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
void Query::dump() const {
llvm::errs() << "Constraints [\n";
- for (ConstraintManager::const_iterator i = constraints.begin();
- i != constraints.end(); i++) {
- (*i)->dump();
- }
+ for (const auto &constraint : constraints)
+ constraint->dump();
+
llvm::errs() << "]\n";
llvm::errs() << "Query [\n";
expr->dump();
diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp
index 93d743db..5d4dab39 100644
--- a/lib/Solver/ValidatingSolver.cpp
+++ b/lib/Solver/ValidatingSolver.cpp
@@ -93,7 +93,7 @@ bool ValidatingSolver::computeInitialValues(
if (hasSolution) {
// Assert the bindings as constraints, and verify that the
// conjunction of the actual constraints is satisfiable.
- std::vector<ref<Expr> > bindings;
+ ConstraintSet bindings;
for (unsigned i = 0; i != values.size(); ++i) {
const Array *array = objects[i];
assert(array);
@@ -107,12 +107,10 @@ bool ValidatingSolver::computeInitialValues(
}
ConstraintManager tmp(bindings);
ref<Expr> constraints = Expr::createIsZero(query.expr);
- for (ConstraintManager::const_iterator it = query.constraints.begin(),
- ie = query.constraints.end();
- it != ie; ++it)
- constraints = AndExpr::create(constraints, *it);
+ for (auto const &constraint : query.constraints)
+ constraints = AndExpr::create(constraints, constraint);
- if (!oracle->impl->computeTruth(Query(tmp, constraints), answer))
+ if (!oracle->impl->computeTruth(Query(bindings, constraints), answer))
return false;
if (!answer)
assert(0 && "invalid solver result (computeInitialValues)");
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-25 21:54:33 +0000