about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2019-03-27 11:33:07 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-07-01 15:52:40 +0100
commitf56c7aa2a7200ece5d074651b9839eb917f910f5 (patch)
treecd4224cc8fb731efdec0b37a1890ab10eb5070da /include
parentd591cba305cb86ee8c520b7ff427651d8f9e0f31 (diff)
downloadklee-f56c7aa2a7200ece5d074651b9839eb917f910f5.tar.gz
Move constraint implementation from header to cpp files
Diffstat (limited to 'include')
-rw-r--r--include/klee/Expr/Constraints.h25
1 files changed, 8 insertions, 17 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;