Separate constraint set and constraint manager

5 files changed, 44 insertions, 56 deletions

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