Separate constraint set and constraint manager

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)");