Separate constraint set and constraint manager

4 files changed, 41 insertions, 32 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) {
     }