CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
guard_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "guard_expr.h"
13
14#include <util/expr_util.h>
15#include <util/invariant.h>
16#include <util/std_expr.h>
17
19{
20 if(is_true())
21 {
22 // do nothing
23 return expr;
24 }
25 else
26 {
27 if(expr.is_false())
28 {
29 return boolean_negate(as_expr());
30 }
31 else
32 {
33 return implies_exprt{as_expr(), expr};
34 }
35 }
36}
37
38void guard_exprt::add(const exprt &expr)
39{
41
42 if(is_false() || expr.is_true())
43 return;
44 else if(is_true() || expr.is_false())
45 {
46 this->expr = expr;
47
48 return;
49 }
50 else if(this->expr.id() != ID_and)
51 {
52 and_exprt a({this->expr});
53 this->expr = a;
54 }
55
56 exprt::operandst &op = this->expr.operands();
57
58 if(expr.id() == ID_and)
59 op.insert(op.end(), expr.operands().begin(), expr.operands().end());
60 else
61 op.push_back(expr);
62}
63
65{
66 if(g1.expr.id() != ID_and)
67 {
68 if(g2.expr.id() != ID_and)
69 {
70 if(g1.expr == g2.expr)
71 g1.expr = true_exprt{};
72 }
73 else
74 {
75 for(const auto &op : g2.expr.operands())
76 {
77 if(g1.expr == op)
78 {
79 g1.expr = true_exprt{};
80 break;
81 }
82 }
83 }
84
85 return g1;
86 }
87
88 if(g2.expr.id() != ID_and)
89 {
90 exprt::operandst &op1 = g1.expr.operands();
91 for(exprt::operandst::iterator it = op1.begin(); it != op1.end(); ++it)
92 {
93 if(g1.expr == g2.expr)
94 {
95 op1.erase(it);
96 break;
97 }
98 }
99
100 return g1;
101 }
102
103 exprt g2_sorted = g2.as_expr();
104
105 exprt::operandst &op1 = g1.expr.operands();
106 const exprt::operandst &op2 = g2_sorted.operands();
107
108 exprt::operandst::iterator it1 = op1.begin();
109 for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
110 ++it2)
111 {
112 if(it1 != op1.end() && *it1 == *it2)
113 it1 = op1.erase(it1);
114 else
115 break;
116 }
117
118 g1.expr = conjunction(op1);
119
120 return g1;
121}
122
124{
125 if(is_true() || is_false() || other_guard.is_true() || other_guard.is_false())
126 return true;
127 if(expr.id() == ID_and && other_guard.expr.id() == ID_and)
128 return true;
129 if(other_guard.expr == boolean_negate(expr))
130 return true;
131 return false;
132}
133
135{
136 if(g2.is_false() || g1.is_true())
137 return g1;
138 if(g1.is_false() || g2.is_true())
139 {
140 g1.expr = g2.expr;
141 return g1;
142 }
143
144 if(g1.expr.id() != ID_and || g2.expr.id() != ID_and)
145 {
146 exprt tmp(boolean_negate(g2.as_expr()));
147
148 if(tmp == g1.as_expr())
149 g1.expr = true_exprt();
150 else
151 g1.expr = or_exprt(g1.as_expr(), g2.as_expr());
152
153 // TODO: make simplify more capable and apply here
154
155 return g1;
156 }
157
158 // find common prefix
159 exprt g2_sorted = g2.as_expr();
160
161 exprt::operandst &op1 = g1.expr.operands();
162 const exprt::operandst &op2 = g2_sorted.operands();
163
165 n_op1.reserve(op1.size());
166 n_op2.reserve(op2.size());
167
168 exprt::operandst::iterator it1 = op1.begin();
169 for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end();
170 ++it2)
171 {
172 while(it1 != op1.end() && *it1 < *it2)
173 {
174 n_op1.push_back(*it1);
175 it1 = op1.erase(it1);
176 }
177 if(it1 != op1.end() && *it1 == *it2)
178 ++it1;
179 else
180 n_op2.push_back(*it2);
181 }
182 while(it1 != op1.end())
183 {
184 n_op1.push_back(*it1);
185 it1 = op1.erase(it1);
186 }
187
188 if(n_op2.empty())
189 return g1;
190
191 // end of common prefix
194
195 g1.expr = conjunction(op1);
196
198
199 if(tmp != and_expr1)
200 {
201 if(and_expr1.is_true() || and_expr2.is_true())
202 {
203 }
204 else
205 // TODO: make simplify more capable and apply here
207 }
208
209 return g1;
210}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
operandst & operands()
Definition expr.h:94
void add(const exprt &expr)
bool is_true() const
Definition guard_expr.h:60
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
exprt as_expr() const
Definition guard_expr.h:46
bool is_false() const
Definition guard_expr.h:65
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
Boolean implication.
Definition std_expr.h:2225
const irep_idt & id() const
Definition irep.h:388
Boolean OR.
Definition std_expr.h:2270
The Boolean constant true.
Definition std_expr.h:3190
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
guard_exprt & operator|=(guard_exprt &g1, const guard_exprt &g2)
guard_exprt & operator-=(guard_exprt &g1, const guard_exprt &g2)
Guard Data Structure.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:83
API to expression classes.