1 //===-- Constraints.h -------------------------------------------*- C++ -*-===// 2 // 3 // The KLEE Symbolic Virtual Machine 4 // 5 // This file is distributed under the University of Illinois Open Source 6 // License. See LICENSE.TXT for details. 7 // 8 //===----------------------------------------------------------------------===// 9 10 #ifndef KLEE_CONSTRAINTS_H 11 #define KLEE_CONSTRAINTS_H 12 13 #include "klee/Expr/Expr.h" 14 15 namespace klee { 16 17 /// Resembles a set of constraints that can be passed around 18 /// 19 class ConstraintSet { 20 friend class ConstraintManager; 21 22 public: 23 using constraints_ty = std::vector<ref<Expr>>; 24 using iterator = constraints_ty::iterator; 25 using const_iterator = constraints_ty::const_iterator; 26 27 using constraint_iterator = const_iterator; 28 29 bool empty() const; 30 constraint_iterator begin() const; 31 constraint_iterator end() const; 32 size_t size() const noexcept; 33 ConstraintSet(constraints_ty cs)34 explicit ConstraintSet(constraints_ty cs) : constraints(std::move(cs)) {} 35 ConstraintSet() = default; 36 37 void push_back(const ref<Expr> &e); 38 39 bool operator==(const ConstraintSet &b) const { 40 return constraints == b.constraints; 41 } 42 43 private: 44 constraints_ty constraints; 45 }; 46 47 class ExprVisitor; 48 49 /// Manages constraints, e.g. optimisation 50 class ConstraintManager { 51 public: 52 /// Create constraint manager that modifies constraints 53 /// \param constraints 54 explicit ConstraintManager(ConstraintSet &constraints); 55 56 /// Simplify expression expr based on constraints 57 /// \param constraints set of constraints used for simplification 58 /// \param expr to simplify 59 /// \return simplified expression 60 static ref<Expr> simplifyExpr(const ConstraintSet &constraints, 61 const ref<Expr> &expr); 62 63 /// Add constraint to the referenced constraint set 64 /// \param constraint 65 void addConstraint(const ref<Expr> &constraint); 66 67 private: 68 /// Rewrite set of constraints using the visitor 69 /// \param visitor constraint rewriter 70 /// \return true iff any constraint has been changed 71 bool rewriteConstraints(ExprVisitor &visitor); 72 73 /// Add constraint to the set of constraints 74 void addConstraintInternal(const ref<Expr> &constraint); 75 76 ConstraintSet &constraints; 77 }; 78 79 } // namespace klee 80 81 #endif /* KLEE_CONSTRAINTS_H */