CBMC
threeval.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_THREEVAL_H
11 #define CPROVER_UTIL_THREEVAL_H
12 
13 #include <iosfwd>
14 
15 //
16 // three valued logic
17 //
18 
19 class tvt
20 {
21 public:
22  // NOLINTNEXTLINE(readability/identifiers)
23  enum class tv_enumt : unsigned char { TV_FALSE, TV_UNKNOWN, TV_TRUE };
24 
25  bool is_true() const { return value==tv_enumt::TV_TRUE; }
26  bool is_false() const { return value==tv_enumt::TV_FALSE; }
27  bool is_unknown() const { return value==tv_enumt::TV_UNKNOWN; }
28  bool is_known() const
29  {
31  }
32 
33  static inline tvt unknown()
34  {
35  return tvt(tv_enumt::TV_UNKNOWN);
36  }
37 
38  const char *to_string() const;
39 
41  {
42  return value;
43  }
44 
45  tvt():value(tv_enumt::TV_UNKNOWN)
46  {
47  }
48 
49  explicit tvt(bool b):value(b?tv_enumt::TV_TRUE:tv_enumt::TV_FALSE)
50  {
51  }
52 
53  explicit tvt(tv_enumt v):value(v)
54  {
55  }
56 
57  bool operator==(const tvt other) const
58  {
59  return value==other.value;
60  }
61 
62  bool operator!=(const tvt other) const
63  {
64  return value!=other.value;
65  }
66 
67  tvt operator&&(const tvt other) const
68  {
69  if(is_false() || other.is_false())
70  return tvt(false);
71  if(is_true() && other.is_true())
72  return tvt(true);
73 
74  return unknown();
75  }
76 
77  tvt operator||(const tvt other) const
78  {
79  if(is_true() || other.is_true())
80  return tvt(true);
81  if(is_false() && other.is_false())
82  return tvt(false);
83 
84  return unknown();
85  }
86 
87  tvt operator!() const
88  {
89  if(is_unknown())
90  return unknown();
91  if(is_true())
92  return tvt(false);
93 
94  return tvt(true);
95  }
96 
97 protected:
99 };
100 
101 std::ostream &operator << (std::ostream &out, const tvt &a);
102 
103 #endif // CPROVER_UTIL_THREEVAL_H
Definition: threeval.h:20
tvt operator&&(const tvt other) const
Definition: threeval.h:67
tv_enumt value
Definition: threeval.h:98
tvt()
Definition: threeval.h:45
bool is_known() const
Definition: threeval.h:28
tvt(bool b)
Definition: threeval.h:49
bool is_unknown() const
Definition: threeval.h:27
bool operator!=(const tvt other) const
Definition: threeval.h:62
const char * to_string() const
Definition: threeval.cpp:13
bool operator==(const tvt other) const
Definition: threeval.h:57
tvt operator!() const
Definition: threeval.h:87
tvt operator||(const tvt other) const
Definition: threeval.h:77
bool is_false() const
Definition: threeval.h:26
bool is_true() const
Definition: threeval.h:25
static tvt unknown()
Definition: threeval.h:33
tv_enumt get_value() const
Definition: threeval.h:40
tvt(tv_enumt v)
Definition: threeval.h:53
tv_enumt
Definition: threeval.h:23
std::ostream & operator<<(std::ostream &out, const tvt &a)
Definition: threeval.cpp:24