3 files changed, 30 insertions, 22 deletions

diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
index b9bf3464..c6521c82 100644
--- a/include/klee/Expr/Constraints.h
+++ b/include/klee/Expr/Constraints.h
@@ -33,30 +33,21 @@ public:
   ConstraintManager &operator=(ConstraintManager &&cs) = default;
 
   // create from constraints with no optimization
-  explicit ConstraintManager(const std::vector<ref<Expr>> &_constraints)
-      : constraints(_constraints) {}
+  explicit ConstraintManager(const std::vector<ref<Expr>> &_constraints);
 
-  // given a constraint which is known to be valid, attempt to
-  // simplify the existing constraint set
-  void simplifyForValidConstraint(ref<Expr> e);
+  typedef std::vector<ref<Expr>>::const_iterator constraint_iterator;
 
   ref<Expr> simplifyExpr(ref<Expr> e) const;
 
   void addConstraint(ref<Expr> e);
 
-  bool empty() const noexcept { return constraints.empty(); }
-  ref<Expr> back() const { return constraints.back(); }
-  const_iterator begin() const { return constraints.cbegin(); }
-  const_iterator end() const { return constraints.cend(); }
-  std::size_t size() const noexcept { return constraints.size(); }
+  bool empty() const noexcept;
+  ref<Expr> back() const;
+  constraint_iterator begin() const;
+  constraint_iterator end() const;
+  size_t size() const noexcept;
 
-  bool operator==(const ConstraintManager &other) const {
-    return constraints == other.constraints;
-  }
-
-  bool operator!=(const ConstraintManager &other) const {
-    return constraints != other.constraints;
-  }
+  bool operator==(const ConstraintManager &other) const;
 
 private:
   std::vector<ref<Expr>> constraints;
diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp
index 89e2ca59..1c7bee57 100644
--- a/lib/Expr/Constraints.cpp
+++ b/lib/Expr/Constraints.cpp
@@ -95,10 +95,6 @@ bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
   return changed;
 }
 
-void ConstraintManager::simplifyForValidConstraint(ref<Expr> e) {
-  // XXX 
-}
-
 ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
   if (isa<ConstantExpr>(e))
     return e;
@@ -168,3 +164,24 @@ void ConstraintManager::addConstraint(ref<Expr> e) {
   e = simplifyExpr(e);
   addConstraintInternal(e);
 }
+
+ConstraintManager::ConstraintManager(const std::vector<ref<Expr>> &_constraints)
+    : constraints(_constraints) {}
+
+bool ConstraintManager::empty() const { return constraints.empty(); }
+
+klee::ref<Expr> ConstraintManager::back() const { return constraints.back(); }
+
+klee::ConstraintManager::constraint_iterator ConstraintManager::begin() const {
+  return constraints.begin();
+}
+
+klee::ConstraintManager::constraint_iterator ConstraintManager::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;
+}
diff --git a/unittests/Assignment/CMakeLists.txt b/unittests/Assignment/CMakeLists.txt
index 8ca55b94..e5dd1b4c 100644
--- a/unittests/Assignment/CMakeLists.txt
+++ b/unittests/Assignment/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_klee_unit_test(AssignmentTest
   AssignmentTest.cpp)
-target_link_libraries(AssignmentTest PRIVATE kleaverExpr)
+target_link_libraries(AssignmentTest PRIVATE kleaverExpr kleaverSolver)