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 */