Separate constraint set and constraint manager

6 files changed, 32 insertions, 27 deletions

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"