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 "std_expr.h"
18 
19 class guardt:public exprt
20 {
21 public:
23  {
24  *this = true_exprt();
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() const
42  {
43  return *this;
44  }
45 
46  void guard_expr(exprt &dest) const;
47 
48  friend guardt &operator -= (guardt &g1, const guardt &g2);
49  friend guardt &operator |= (guardt &g1, const guardt &g2);
50 };
51 
52 #endif // CPROVER_UTIL_GUARD_H
exprt as_expr() const
Definition: guard.h:41
void guard_expr(exprt &dest) const
Definition: guard.cpp:21
void append(const guardt &guard)
Definition: guard.h:36
Definition: guard.h:19
The Boolean constant true.
Definition: std_expr.h:4443
API to expression classes.
friend guardt & operator|=(guardt &g1, const guardt &g2)
Definition: guard.cpp:101
friend guardt & operator -=(guardt &g1, const guardt &g2)
Definition: guard.cpp:72
Base class for all expressions.
Definition: expr.h:54
guardt & operator=(const exprt &e)
Definition: guard.h:27
void add(const exprt &expr)
Definition: guard.cpp:43
guardt()
Definition: guard.h:22