Separate constraint set and constraint manager

25 files changed, 175 insertions, 189 deletions

diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h
index 395a3387..7384e0cc 100644
--- a/include/klee/Expr/Assignment.h
+++ b/include/klee/Expr/Assignment.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_ASSIGNMENT_H
 #define KLEE_ASSIGNMENT_H
 
+#include "klee/Expr/Constraints.h"
 #include "klee/Expr/ExprEvaluator.h"
 
 #include <map>
@@ -44,7 +45,7 @@ namespace klee {
     
     ref<Expr> evaluate(const Array *mo, unsigned index) const;
     ref<Expr> evaluate(ref<Expr> e);
-    void createConstraintsFromAssignment(std::vector<ref<Expr> > &out) const;
+    ConstraintSet createConstraintsFromAssignment() const;
 
     template<typename InputIterator>
     bool satisfies(InputIterator begin, InputIterator end);
diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
index c6521c82..ae0f86f2 100644
--- a/include/klee/Expr/Constraints.h
+++ b/include/klee/Expr/Constraints.h
@@ -12,52 +12,60 @@
 
 #include "klee/Expr/Expr.h"
 
-// FIXME: Currently we use ConstraintManager for two things: to pass
-// sets of constraints around, and to optimize constraints. We should
-// move the first usage into a separate data structure
-// (ConstraintSet?) which ConstraintManager could embed if it likes.
 namespace klee {
 
-class ExprVisitor;
+/// Resembles a set of constraints that can be passed around
+///
+class ConstraintSet {
+  friend class ConstraintManager;
 
-class ConstraintManager {
 public:
   using constraints_ty = std::vector<ref<Expr>>;
   using iterator = constraints_ty::iterator;
   using const_iterator = constraints_ty::const_iterator;
 
-  ConstraintManager() = default;
-  ConstraintManager(const ConstraintManager &cs) = default;
-  ConstraintManager &operator=(const ConstraintManager &cs) = default;
-  ConstraintManager(ConstraintManager &&cs) = default;
-  ConstraintManager &operator=(ConstraintManager &&cs) = default;
-
-  // create from constraints with no optimization
-  explicit ConstraintManager(const std::vector<ref<Expr>> &_constraints);
-
-  typedef std::vector<ref<Expr>>::const_iterator constraint_iterator;
-
-  ref<Expr> simplifyExpr(ref<Expr> e) const;
+  typedef const_iterator constraint_iterator;
 
-  void addConstraint(ref<Expr> e);
-
-  bool empty() const noexcept;
-  ref<Expr> back() const;
+  bool empty() const;
   constraint_iterator begin() const;
   constraint_iterator end() const;
   size_t size() const noexcept;
 
-  bool operator==(const ConstraintManager &other) const;
+  explicit ConstraintSet(constraints_ty cs) : constraints(std::move(cs)) {}
+  ConstraintSet() = default;
+
+  void push_back(const ref<Expr> &e);
+
+  bool operator==(const ConstraintSet &b) const {
+    return constraints == b.constraints;
+  }
 
 private:
-  std::vector<ref<Expr>> constraints;
+  constraints_ty constraints;
+};
+
+class ExprVisitor;
+
+/// Manages constraints, e.g. optimisation
+class ConstraintManager {
+public:
+  // create from constraints with no optimization
+  explicit ConstraintManager(ConstraintSet &constraints);
+
+  static ref<Expr> simplifyExpr(const ConstraintSet &constraints,
+                                const ref<Expr> &e);
+
+  void addConstraint(ref<Expr> e);
 
   // returns true iff the constraints were modified
   bool rewriteConstraints(ExprVisitor &visitor);
 
   void addConstraintInternal(ref<Expr> e);
+
+private:
+  ConstraintSet &constraints;
 };
 
 } // namespace klee
 
-#endif /* KLEE_CONSTRAINTS_H */
+#endif /* KLEE_CONSTRAINTS_H */
\ No newline at end of file
diff --git a/include/klee/Expr/ExprPPrinter.h b/include/klee/Expr/ExprPPrinter.h
index 7541c132..8db9a5c7 100644
--- a/include/klee/Expr/ExprPPrinter.h
+++ b/include/klee/Expr/ExprPPrinter.h
@@ -16,7 +16,7 @@ namespace llvm {
   class raw_ostream;
 }
 namespace klee {
-  class ConstraintManager;
+  class ConstraintSet;
 
   class ExprPPrinter {
   protected:
@@ -61,10 +61,10 @@ namespace klee {
     static void printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e);
 
     static void printConstraints(llvm::raw_ostream &os,
-                                 const ConstraintManager &constraints);
+                                 const ConstraintSet &constraints);
 
     static void printQuery(llvm::raw_ostream &os,
-                           const ConstraintManager &constraints,
+                           const ConstraintSet &constraints,
                            const ref<Expr> &q,
                            const ref<Expr> *evalExprsBegin = 0,
                            const ref<Expr> *evalExprsEnd = 0,
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
index ec107c20..06b9b573 100644
--- a/include/klee/Solver/Solver.h
+++ b/include/klee/Solver/Solver.h
@@ -17,16 +17,16 @@
 #include <vector>
 
 namespace klee {
-  class ConstraintManager;
+  class ConstraintSet;
   class Expr;
   class SolverImpl;
 
   struct Query {
   public:
-    const ConstraintManager &constraints;
+    const ConstraintSet &constraints;
     ref<Expr> expr;
 
-    Query(const ConstraintManager& _constraints, ref<Expr> _expr)
+    Query(const ConstraintSet& _constraints, ref<Expr> _expr)
       : constraints(_constraints), expr(_expr) {
     }
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 14d596fc..0b848f41 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -310,11 +310,12 @@ bool ExecutionState::merge(const ExecutionState &b) {
     }
   }
 
-  constraints = ConstraintManager();
-  for (std::set< ref<Expr> >::iterator it = commonConstraints.begin(), 
-         ie = commonConstraints.end(); it != ie; ++it)
-    constraints.addConstraint(*it);
-  constraints.addConstraint(OrExpr::create(inA, inB));
+  constraints = ConstraintSet();
+
+  ConstraintManager m(constraints);
+  for (const auto &constraint : commonConstraints)
+    m.addConstraint(constraint);
+  m.addConstraint(OrExpr::create(inA, inB));
 
   return true;
 }
@@ -352,3 +353,8 @@ void ExecutionState::dumpStack(llvm::raw_ostream &out) const {
     target = sf.caller;
   }
 }
+
+void ExecutionState::addConstraint(ref<Expr> e) {
+  ConstraintManager c(constraints);
+  c.addConstraint(e);
+}
diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h
index f1b09644..397b2364 100644
--- a/lib/Core/ExecutionState.h
+++ b/lib/Core/ExecutionState.h
@@ -92,7 +92,7 @@ public:
   AddressSpace addressSpace;
 
   /// @brief Constraints collected so far
-  ConstraintManager constraints;
+  ConstraintSet constraints;
 
   /// Statistics and information
 
@@ -171,7 +171,8 @@ public:
   void popFrame();
 
   void addSymbolic(const MemoryObject *mo, const Array *array);
-  void addConstraint(ref<Expr> e) { constraints.addConstraint(std::move(e)); }
+
+  void addConstraint(ref<Expr> e);
 
   bool merge(const ExecutionState &b);
   void dumpStack(llvm::raw_ostream &out) const;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index af376755..39de6e8d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1252,7 +1252,7 @@ ref<klee::ConstantExpr>
 Executor::toConstant(ExecutionState &state, 
                      ref<Expr> e,
                      const char *reason) {
-  e = state.constraints.simplifyExpr(e);
+  e = ConstraintManager::simplifyExpr(state.constraints, e);
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
     return CE;
 
@@ -1280,7 +1280,7 @@ Executor::toConstant(ExecutionState &state,
 void Executor::executeGetValue(ExecutionState &state,
                                ref<Expr> e,
                                KInstruction *target) {
-  e = state.constraints.simplifyExpr(e);
+  e = ConstraintManager::simplifyExpr(state.constraints, e);
   std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
     seedMap.find(&state);
   if (it==seedMap.end() || isa<ConstantExpr>(e)) {
@@ -3651,9 +3651,9 @@ void Executor::executeMemoryOperation(ExecutionState &state,
 
   if (SimplifySymIndices) {
     if (!isa<ConstantExpr>(address))
-      address = state.constraints.simplifyExpr(address);
+      address = ConstraintManager::simplifyExpr(state.constraints, address);
     if (isWrite && !isa<ConstantExpr>(value))
-      value = state.constraints.simplifyExpr(value);
+      value = ConstraintManager::simplifyExpr(state.constraints, value);
   }
 
   address = optimizer.optimizeExpr(address, true);
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index a09e4b7c..4baec512 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -193,14 +193,12 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
 
   getImpliedValues(e, value, results);
 
-  for (ImpliedValueList::iterator i = results.begin(), ie = results.end();
-       i != ie; ++i) {
-    std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = 
-      found.find(i->first);
+  for (auto &i : results) {
+    auto it = found.find(i.first);
     if (it != found.end()) {
-      assert(it->second == i->second && "Invalid ImpliedValue!");
+      assert(it->second == i.second && "Invalid ImpliedValue!");
     } else {
-      found.insert(std::make_pair(i->first, i->second));
+      found.insert(std::make_pair(i.first, i.second));
     }
   }
 
@@ -208,7 +206,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
   std::set< ref<ReadExpr> > readsSet(reads.begin(), reads.end());
   reads = std::vector< ref<ReadExpr> >(readsSet.begin(), readsSet.end());
 
-  std::vector<ref<Expr> > assumption;
+  ConstraintSet assumption;
   assumption.push_back(EqExpr::create(e, value));
 
   // obscure... we need to make sure that all the read indices are
@@ -225,16 +223,15 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
                                                              Context::get().getPointerWidth())));
   }
 
-  ConstraintManager assume(assumption);
-  for (std::vector< ref<ReadExpr> >::iterator i = reads.begin(), 
-         ie = reads.end(); i != ie; ++i) {
-    ref<ReadExpr> var = *i;
+  for (const auto &var : reads) {
     ref<ConstantExpr> possible;
-    bool success = S->getValue(Query(assume, var), possible); (void) success;
+    bool success = S->getValue(Query(assumption, var), possible);
+    (void)success;
     assert(success && "FIXME: Unhandled solver failure");    
     std::map<ref<ReadExpr>, ref<ConstantExpr> >::iterator it = found.find(var);
     bool res;
-    success = S->mustBeTrue(Query(assume, EqExpr::create(var, possible)), res);
+    success =
+        S->mustBeTrue(Query(assumption, EqExpr::create(var, possible)), res);
     assert(success && "FIXME: Unhandled solver failure");    
     if (res) {
       if (it != found.end()) {
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index d525a9db..cc0afff8 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -34,7 +34,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = state.constraints.simplifyExpr(expr);
+    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
 
   bool success = solver->evaluate(Query(state.constraints, expr), result);
 
@@ -54,7 +54,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = state.constraints.simplifyExpr(expr);
+    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
 
   bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
 
@@ -97,7 +97,7 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = state.constraints.simplifyExpr(expr);
+    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
 
   bool success = solver->getValue(Query(state.constraints, expr), result);
 
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index f6dfd5b9..8e25b21c 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_TIMINGSOLVER_H
 #define KLEE_TIMINGSOLVER_H
 
+#include "klee/Expr/Constraints.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Solver/Solver.h"
 #include "klee/System/Time.h"
diff --git a/lib/Expr/Assignment.cpp b/lib/Expr/Assignment.cpp
index 2fc569cc..98b92337 100644
--- a/lib/Expr/Assignment.cpp
+++ b/lib/Expr/Assignment.cpp
@@ -25,20 +25,20 @@ void Assignment::dump() {
   }
 }
 
-void Assignment::createConstraintsFromAssignment(
-    std::vector<ref<Expr> > &out) const {
-  assert(out.size() == 0 && "out should be empty");
-  for (bindings_ty::const_iterator it = bindings.begin(), ie = bindings.end();
-       it != ie; ++it) {
-    const Array *array = it->first;
-    const std::vector<unsigned char> &values = it->second;
+ConstraintSet Assignment::createConstraintsFromAssignment() const {
+  ConstraintSet result;
+  for (const auto &binding : bindings) {
+    const auto &array = binding.first;
+    const auto &values = binding.second;
+
     for (unsigned arrayIndex = 0; arrayIndex < array->size; ++arrayIndex) {
       unsigned char value = values[arrayIndex];
-      out.push_back(EqExpr::create(
+      result.push_back(EqExpr::create(
           ReadExpr::create(UpdateList(array, 0),
                            ConstantExpr::alloc(arrayIndex, array->getDomain())),
           ConstantExpr::alloc(value, array->getRange())));
     }
   }
+  return result;
 }
 }
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 1c7bee57..6b576435 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -59,9 +59,8 @@ private:
   const std::map< ref<Expr>, ref<Expr> > &replacements;
 
 public:
-  ExprReplaceVisitor2(const std::map< ref<Expr>, ref<Expr> > &_replacements) 
-    : ExprVisitor(true),
-      replacements(_replacements) {}
+  ExprReplaceVisitor2(const std::map<ref<Expr>, ref<Expr>> &_replacements)
+      : ExprVisitor(true), replacements(_replacements) {}
 
   Action visitExprPost(const Expr &e) {
     std::map< ref<Expr>, ref<Expr> >::const_iterator it =
@@ -75,13 +74,11 @@ public:
 };
 
 bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
-  ConstraintManager::constraints_ty old;
+  ConstraintSet old;
   bool changed = false;
 
-  constraints.swap(old);
-  for (ConstraintManager::constraints_ty::iterator 
-         it = old.begin(), ie = old.end(); it != ie; ++it) {
-    ref<Expr> &ce = *it;
+  std::swap(constraints, old);
+  for (auto &ce : old) {
     ref<Expr> e = visitor.visit(ce);
 
     if (e!=ce) {
@@ -95,25 +92,26 @@ bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
   return changed;
 }
 
-ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
+ref<Expr> ConstraintManager::simplifyExpr(const ConstraintSet &constraints,
+                                          const ref<Expr> &e) {
+
   if (isa<ConstantExpr>(e))
     return e;
 
   std::map< ref<Expr>, ref<Expr> > equalities;
-  
-  for (ConstraintManager::constraints_ty::const_iterator 
-         it = constraints.begin(), ie = constraints.end(); it != ie; ++it) {
-    if (const EqExpr *ee = dyn_cast<EqExpr>(*it)) {
+
+  for (auto &constraint : constraints) {
+    if (const EqExpr *ee = dyn_cast<EqExpr>(constraint)) {
       if (isa<ConstantExpr>(ee->left)) {
         equalities.insert(std::make_pair(ee->right,
                                          ee->left));
       } else {
-        equalities.insert(std::make_pair(*it,
-                                         ConstantExpr::alloc(1, Expr::Bool)));
+        equalities.insert(
+            std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool)));
       }
     } else {
-      equalities.insert(std::make_pair(*it,
-                                       ConstantExpr::alloc(1, Expr::Bool)));
+      equalities.insert(
+          std::make_pair(constraint, ConstantExpr::alloc(1, Expr::Bool)));
     }
   }
 
@@ -125,10 +123,10 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
 
   switch (e->getKind()) {
   case Expr::Constant:
-    assert(cast<ConstantExpr>(e)->isTrue() && 
+    assert(cast<ConstantExpr>(e)->isTrue() &&
            "attempt to add invalid (false) constraint");
     break;
-    
+
     // split to enable finer grained independence and other optimizations
   case Expr::And: {
     BinaryExpr *be = cast<BinaryExpr>(e);
@@ -153,7 +151,7 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
     constraints.push_back(e);
     break;
   }
-    
+
   default:
     constraints.push_back(e);
     break;
@@ -161,27 +159,23 @@ void ConstraintManager::addConstraintInternal(ref<Expr> e) {
 }
 
 void ConstraintManager::addConstraint(ref<Expr> e) {
-  e = simplifyExpr(e);
+  e = simplifyExpr(constraints, e);
   addConstraintInternal(e);
 }
 
-ConstraintManager::ConstraintManager(const std::vector<ref<Expr>> &_constraints)
+ConstraintManager::ConstraintManager(ConstraintSet &_constraints)
     : constraints(_constraints) {}
 
-bool ConstraintManager::empty() const { return constraints.empty(); }
-
-klee::ref<Expr> ConstraintManager::back() const { return constraints.back(); }
+bool ConstraintSet::empty() const { return constraints.empty(); }
 
-klee::ConstraintManager::constraint_iterator ConstraintManager::begin() const {
+klee::ConstraintSet::constraint_iterator ConstraintSet::begin() const {
   return constraints.begin();
 }
 
-klee::ConstraintManager::constraint_iterator ConstraintManager::end() const {
+klee::ConstraintSet::constraint_iterator ConstraintSet::end() const {
   return constraints.end();
 }
 
 size_t ConstraintSet::size() const noexcept { return constraints.size(); }
 
-bool ConstraintManager::operator==(const ConstraintManager &other) const {
-  return constraints == other.constraints;
-}
+void ConstraintSet::push_back(const ref<Expr> &e) { constraints.push_back(e); }
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 267be7e8..ba0458ae 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -472,7 +472,7 @@ void ExprPPrinter::printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e) {
 }
 
 void ExprPPrinter::printConstraints(llvm::raw_ostream &os,
-                                    const ConstraintManager &constraints) {
+                                    const ConstraintSet &constraints) {
   printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
 }
 
@@ -486,7 +486,7 @@ struct ArrayPtrsByName {
 }
 
 void ExprPPrinter::printQuery(llvm::raw_ostream &os,
-                              const ConstraintManager &constraints,
+                              const ConstraintSet &constraints,
                               const ref<Expr> &q,
                               const ref<Expr> *evalExprsBegin,
                               const ref<Expr> *evalExprsEnd,
@@ -494,10 +494,9 @@ void ExprPPrinter::printQuery(llvm::raw_ostream &os,
                               const Array * const *evalArraysEnd,
                               bool printArrayDecls) {
   PPrinter p(os);
-  
-  for (ConstraintManager::const_iterator it = constraints.begin(),
-         ie = constraints.end(); it != ie; ++it)
-    p.scan(*it);
+
+  for (const auto &constraint : constraints)
+    p.scan(constraint);
   p.scan(q);
 
   for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it)
@@ -537,8 +536,7 @@ void ExprPPrinter::printQuery(llvm::raw_ostream &os,
   
   // Ident at constraint list;
   unsigned indent = PC.pos;
-  for (ConstraintManager::const_iterator it = constraints.begin(),
-         ie = constraints.end(); it != ie;) {
+  for (auto it = constraints.begin(), ie = constraints.end(); it != ie;) {
     p.print(*it, PC);
     ++it;
     if (it != ie)
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index 069eb32f..523e7f8c 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -505,9 +505,8 @@ void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode *un,
 
 void ExprSMTLIBPrinter::scanAll() {
   // perform scan of all expressions
-  for (ConstraintManager::const_iterator i = query->constraints.begin();
-       i != query->constraints.end(); i++)
-    scan(*i);
+  for (const auto &constraint : query->constraints)
+    scan(constraint);
 
   // Scan the query too
   scan(query->expr);
@@ -629,10 +628,8 @@ void ExprSMTLIBPrinter::printHumanReadableQuery() {
 
   if (abbrMode != ABBR_LET) {
     // Generate assert statements for each constraint
-    for (ConstraintManager::const_iterator i = query->constraints.begin();
-         i != query->constraints.end(); i++) {
-      printAssert(*i);
-    }
+    for (const auto &constraint : query->constraints)
+      printAssert(constraint);
 
     *o << "; QueryExpr\n";
 
diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index 6b29ac3e..7ef56849 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -1632,9 +1632,8 @@ void QueryCommand::dump() {
     ObjectsBegin = &Objects[0];
     ObjectsEnd = ObjectsBegin + Objects.size();
   }
-  ExprPPrinter::printQuery(llvm::outs(), ConstraintManager(Constraints),
-                           Query, ValuesBegin, ValuesEnd,
-                           ObjectsBegin, ObjectsEnd,
+  ExprPPrinter::printQuery(llvm::outs(), ConstraintSet(Constraints), Query,
+                           ValuesBegin, ValuesEnd, ObjectsBegin, ObjectsEnd,
                            false);
 }
 
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)");
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 512a1e4e..9a79474c 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -227,7 +227,7 @@ static bool EvaluateInputAST(const char *Filename,
       assert("FIXME: Support counterexample query commands!");
       if (QC->Values.empty() && QC->Objects.empty()) {
         bool result;
-        if (S->mustBeTrue(Query(ConstraintManager(QC->Constraints), QC->Query),
+        if (S->mustBeTrue(Query(ConstraintSet(QC->Constraints), QC->Query),
                           result)) {
           llvm::outs() << (result ? "VALID" : "INVALID");
         } else {
@@ -243,8 +243,7 @@ static bool EvaluateInputAST(const char *Filename,
         assert(QC->Query->isFalse() &&
                "FIXME: Support counterexamples with non-trivial query!");
         ref<ConstantExpr> result;
-        if (S->getValue(Query(ConstraintManager(QC->Constraints), 
-                              QC->Values[0]),
+        if (S->getValue(Query(ConstraintSet(QC->Constraints), QC->Values[0]),
                         result)) {
           llvm::outs() << "INVALID\n";
           llvm::outs() << "\tExpr 0:\t" << result;
@@ -255,10 +254,10 @@ static bool EvaluateInputAST(const char *Filename,
         }
       } else {
         std::vector< std::vector<unsigned char> > result;
-        
-        if (S->getInitialValues(Query(ConstraintManager(QC->Constraints), 
-                                      QC->Query),
-                                QC->Objects, result)) {
+
+        if (S->getInitialValues(
+                Query(ConstraintSet(QC->Constraints), QC->Query), QC->Objects,
+                result)) {
           llvm::outs() << "INVALID\n";
 
           for (unsigned i = 0, e = result.size(); i != e; ++i) {
@@ -364,9 +363,9 @@ static bool printInputAsSMTLIBv2(const char *Filename,
 			 * constraint in the constraint set is set to NULL and
 			 * will later cause a NULL pointer dereference.
 			 */
-			ConstraintManager constraintM(QC->Constraints);
-			Query query(constraintM,QC->Query);
-			printer.setQuery(query);
+                        ConstraintSet constraintM(QC->Constraints);
+                        Query query(constraintM, QC->Query);
+                        printer.setQuery(query);
 
 			if(!QC->Objects.empty())
 				printer.setArrayValuesToGet(QC->Objects);
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp
index 9c1089e0..d5d207a0 100644
--- a/unittests/Solver/SolverTest.cpp
+++ b/unittests/Solver/SolverTest.cpp
@@ -80,9 +80,10 @@ void testOperation(Solver &solver,
     
     ref<Expr> queryExpr = EqExpr::create(fullySymbolicExpr, 
                                          partiallyConstantExpr);
-    
-    ConstraintManager constraints;
-    constraints.addConstraint(expr);
+
+    ConstraintSet constraints;
+    ConstraintManager cm(constraints);
+    cm.addConstraint(expr);
     bool res;
     bool success = solver.mustBeTrue(Query(constraints, queryExpr), res);
     EXPECT_EQ(true, success) << "Constraint solving failed";
diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp
index a3aa52f6..eab43d79 100644
--- a/unittests/Solver/Z3SolverTest.cpp
+++ b/unittests/Solver/Z3SolverTest.cpp
@@ -36,7 +36,9 @@ protected:
 };
 
 TEST_F(Z3SolverTest, GetConstraintLog) {
-  ConstraintManager Constraints;
+  ConstraintSet Constraints;
+  ConstraintManager cm(Constraints);
+
   const std::vector<uint64_t> ConstantValues{1, 2, 3, 4};
   std::vector<ref<ConstantExpr>> ConstantExpressions;