klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Constraints.h
Go to the documentation of this file.
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.h"
14 
15 // FIXME: Currently we use ConstraintManager for two things: to pass
16 // sets of constraints around, and to optimize constraints. We should
17 // move the first usage into a separate data structure
18 // (ConstraintSet?) which ConstraintManager could embed if it likes.
19 namespace klee {
20 
21 class ExprVisitor;
22 
24 public:
25  typedef std::vector< ref<Expr> > constraints_ty;
26  typedef constraints_ty::iterator iterator;
27  typedef constraints_ty::const_iterator const_iterator;
28 
30 
31  // create from constraints with no optimization
32  explicit
33  ConstraintManager(const std::vector< ref<Expr> > &_constraints) :
34  constraints(_constraints) {}
35 
37 
38  typedef std::vector< ref<Expr> >::const_iterator constraint_iterator;
39 
40  // given a constraint which is known to be valid, attempt to
41  // simplify the existing constraint set
43 
45 
46  void addConstraint(ref<Expr> e);
47 
48  bool empty() const {
49  return constraints.empty();
50  }
51  ref<Expr> back() const {
52  return constraints.back();
53  }
55  return constraints.begin();
56  }
58  return constraints.end();
59  }
60  size_t size() const {
61  return constraints.size();
62  }
63 
64  bool operator==(const ConstraintManager &other) const {
65  return constraints == other.constraints;
66  }
67 
68 private:
69  std::vector< ref<Expr> > constraints;
70 
71  // returns true iff the constraints were modified
72  bool rewriteConstraints(ExprVisitor &visitor);
73 
75 };
76 
77 }
78 
79 #endif /* KLEE_CONSTRAINTS_H */
constraint_iterator end() const
Definition: Constraints.h:57
bool rewriteConstraints(ExprVisitor &visitor)
Definition: Constraints.cpp:70
ConstraintManager(const ConstraintManager &cs)
Definition: Constraints.h:36
void addConstraint(ref< Expr > e)
constraints_ty::const_iterator const_iterator
Definition: Constraints.h:27
void addConstraintInternal(ref< Expr > e)
size_t size() const
Definition: Constraints.h:60
ConstraintManager(const std::vector< ref< Expr > > &_constraints)
Definition: Constraints.h:33
bool operator==(const ConstraintManager &other) const
Definition: Constraints.h:64
bool empty() const
Definition: Constraints.h:48
std::vector< ref< Expr > > constraints
Definition: Constraints.h:69
constraint_iterator begin() const
Definition: Constraints.h:54
std::vector< ref< Expr > > constraints_ty
Definition: Constraints.h:25
void simplifyForValidConstraint(ref< Expr > e)
Definition: Constraints.cpp:91
ref< Expr > simplifyExpr(ref< Expr > e) const
Definition: Constraints.cpp:95
ref< Expr > back() const
Definition: Constraints.h:51
std::vector< ref< Expr > >::const_iterator constraint_iterator
Definition: Constraints.h:38
constraints_ty::iterator iterator
Definition: Constraints.h:26