zcov: / include/klee/Constraints.h

	Files: 1 Branches Taken: 0.0% 0 / 0 Generated: 2009-05-17 22:47 Branches Executed: 0.0% 0 / 0 Line Coverage: 100.0% 9 / 9

	Programs: 21 Runs 10844

       1                 : //===- Constraints.h - --*- C++ -*-===//
       2                 : 
       3                 : #ifndef KLEE_CONSTRAINTS_H
       4                 : #define KLEE_CONSTRAINTS_H
       5                 : 
       6                 : #include "klee/Expr.h"
       7                 : 
       8                 : // FIXME: Currently we use ConstraintManager for two things: to pass
       9                 : // sets of constraints around, and to optimize constraints. We should
      10                 : // move the first usage into a separate data structure
      11                 : // (ConstraintSet?) which ConstraintManager could embed if it likes.
      12                 : namespace klee {
      13                 : 
      14                 : class ExprVisitor;
      15                 :   
      16            24667: class ConstraintManager {
      17                 : public:
      18                 :   typedef std::vector< ref<Expr> > constraints_ty;
      19                 :   typedef constraints_ty::iterator iterator;
      20                 :   typedef constraints_ty::const_iterator const_iterator;
      21                 : 
      22             1190:   ConstraintManager() {}
      23                 : 
      24                 :   // create from constraints with no optimization
      25                 :   explicit
      26             3130:   ConstraintManager(const std::vector< ref<Expr> > &_constraints) :
      27             6278:     constraints(_constraints) {}
      28                 : 
      29            34088:   ConstraintManager(const ConstraintManager &cs) : constraints(cs.constraints) {}
      30                 : 
      31                 :   typedef std::vector< ref<Expr> >::const_iterator constraint_iterator;
      32                 : 
      33                 :   // given a constraint which is known to be valid, attempt to 
      34                 :   // simplify the existing constraint set
      35                 :   void simplifyForValidConstraint(ref<Expr> e);
      36                 : 
      37                 :   ref<Expr> simplifyExpr(ref<Expr> e) const;
      38                 : 
      39                 :   void addConstraint(ref<Expr> e);
      40                 :   
      41                 :   bool empty() const {
      42              128:     return constraints.empty();
      43                 :   }
      44                 :   ref<Expr> back() const {
      45                 :     return constraints.back();
      46                 :   }
      47                 :   constraint_iterator begin() const {
      48            19450:     return constraints.begin();
      49                 :   }
      50                 :   constraint_iterator end() const {
      51            46991:     return constraints.end();
      52                 :   }
      53                 :   size_t size() const {
      54                 :     return constraints.size();
      55                 :   }
      56                 : 
      57                 :   bool operator==(const ConstraintManager &other) const {
      58             8332:     return constraints == other.constraints;
      59                 :   }
      60                 :   
      61                 : private:
      62                 :   std::vector< ref<Expr> > constraints;
      63                 : 
      64                 :   // returns true iff the constraints were modified
      65                 :   bool rewriteConstraints(ExprVisitor &visitor);
      66                 : 
      67                 :   void addConstraintInternal(ref<Expr> e);
      68                 : };
      69                 : 
      70                 : }
      71                 : 
      72                 : #endif /* KLEE_CONSTRAINTS_H */