cprover
guard.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Guard Data Structure
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_GUARD_H
13 #define CPROVER_UTIL_GUARD_H
14 
15 #include <iosfwd>
16 
17 #include "expr.h"
18 
19 class guardt:public exprt
20 {
21 public:
23  {
24  make_true();
25  }
26 
27  guardt &operator=(const exprt &e)
28  {
29  *this=static_cast<const guardt&>(e);
30 
31  return *this;
32  }
33 
34  void add(const exprt &expr);
35 
36  void append(const guardt &guard)
37  {
38  add(guard);
39  }
40 
41  // exprt as_expr(guard_listt::const_iterator it) const;
42 
43  exprt as_expr() const
44  {
45  return *this;
46  }
47 
48  void guard_expr(exprt &dest) const;
49 
50 #if 0
51  bool empty() const { return guard_list.empty(); }
52  bool is_true() const { return empty(); }
53  bool is_false() const;
54 
55  void make_true()
56  {
57  guard_list.clear();
58  }
59 
60  void make_false();
61 #endif
62 
63  friend guardt &operator -= (guardt &g1, const guardt &g2);
64  friend guardt &operator |= (guardt &g1, const guardt &g2);
65 
66 #if 0
67  void swap(guardt &g)
68  {
69  guard_list.swap(g.guard_list);
70  }
71 
72  size_type size() const
73  {
74  return guard_list.size();
75  }
76 
77  void resize(size_type s)
78  {
79  guard_list.resize(s);
80  }
81 
82  const guard_listt &get_guard_list() const
83  {
84  return guard_list;
85  }
86 
87 protected:
88  guard_listt guard_list;
89 #endif
90 };
91 
92 #endif // CPROVER_UTIL_GUARD_H
exprt as_expr() const
Definition: guard.h:43
friend guardt & operator-=(guardt &g1, const guardt &g2)
Definition: guard.cpp:93
void guard_expr(exprt &dest) const
Definition: guard.cpp:19
void append(const guardt &guard)
Definition: guard.h:36
bool is_false() const
Definition: expr.cpp:131
bool is_true() const
Definition: expr.cpp:124
Definition: guard.h:19
unsignedbv_typet size_type()
Definition: c_types.cpp:58
void make_true()
Definition: expr.cpp:144
friend guardt & operator|=(guardt &g1, const guardt &g2)
Definition: guard.cpp:122
Base class for all expressions.
Definition: expr.h:42
void make_false()
Definition: expr.cpp:150
void swap(irept &irep)
Definition: irep.h:231
guardt & operator=(const exprt &e)
Definition: guard.h:27
void add(const exprt &expr)
Definition: guard.cpp:64
guardt()
Definition: guard.h:22