cprover
Loading...
Searching...
No Matches
simplify_expr_if.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10
11#include "arith_tools.h"
12#include "range.h"
13#include "std_expr.h"
14
16 exprt &expr,
17 const exprt &cond,
18 bool truth,
19 bool &new_truth)
20{
21 if(expr == cond)
22 {
23 new_truth = truth;
24 return false;
25 }
26
27 if(truth && cond.id() == ID_lt && expr.id() == ID_lt)
28 {
29 const auto &cond_lt = to_binary_relation_expr(cond);
30 const auto &expr_lt = to_binary_relation_expr(expr);
31
32 if(
33 cond_lt.op0() == expr_lt.op0() && cond_lt.op1().is_constant() &&
34 expr_lt.op1().is_constant() &&
35 cond_lt.op1().type() == expr_lt.op1().type())
36 {
37 mp_integer i1, i2;
38
39 if(
40 !to_integer(to_constant_expr(cond_lt.op1()), i1) &&
41 !to_integer(to_constant_expr(expr_lt.op1()), i2))
42 {
43 if(i1 >= i2)
44 {
45 new_truth = true;
46 return false;
47 }
48 }
49 }
50
51 if(
52 cond_lt.op1() == expr_lt.op1() && cond_lt.op0().is_constant() &&
53 expr_lt.op0().is_constant() &&
54 cond_lt.op0().type() == expr_lt.op0().type())
55 {
56 mp_integer i1, i2;
57
58 if(
59 !to_integer(to_constant_expr(cond_lt.op0()), i1) &&
60 !to_integer(to_constant_expr(expr_lt.op0()), i2))
61 {
62 if(i1 <= i2)
63 {
64 new_truth = true;
65 return false;
66 }
67 }
68 }
69 }
70
71 return true;
72}
73
75 exprt &expr,
76 const exprt &cond,
77 bool truth)
78{
79 if(expr.type().id() == ID_bool)
80 {
81 bool new_truth;
82
83 if(!simplify_if_implies(expr, cond, truth, new_truth))
84 {
85 if(new_truth)
86 {
87 expr = true_exprt();
88 return false;
89 }
90 else
91 {
92 expr = false_exprt();
93 return false;
94 }
95 }
96 }
97
98 bool no_change = true;
99
100 Forall_operands(it, expr)
101 no_change = simplify_if_recursive(*it, cond, truth) && no_change;
102
103 return no_change;
104}
105
107{
108 forall_operands(it, cond)
109 {
110 if(expr == *it)
111 {
112 expr = true_exprt();
113 return false;
114 }
115 }
116
117 bool no_change = true;
118
119 Forall_operands(it, expr)
120 no_change = simplify_if_conj(*it, cond) && no_change;
121
122 return no_change;
123}
124
126{
127 forall_operands(it, cond)
128 {
129 if(expr == *it)
130 {
131 expr = false_exprt();
132 return false;
133 }
134 }
135
136 bool no_change = true;
137
138 Forall_operands(it, expr)
139 no_change = simplify_if_disj(*it, cond) && no_change;
140
141 return no_change;
142}
143
145 exprt &trueexpr,
146 exprt &falseexpr,
147 const exprt &cond)
148{
149 bool tno_change = true;
150 bool fno_change = true;
151
152 if(cond.id() == ID_and)
153 {
154 tno_change = simplify_if_conj(trueexpr, cond) && tno_change;
155 fno_change = simplify_if_recursive(falseexpr, cond, false) && fno_change;
156 }
157 else if(cond.id() == ID_or)
158 {
159 tno_change = simplify_if_recursive(trueexpr, cond, true) && tno_change;
160 fno_change = simplify_if_disj(falseexpr, cond) && fno_change;
161 }
162 else
163 {
164 tno_change = simplify_if_recursive(trueexpr, cond, true) && tno_change;
165 fno_change = simplify_if_recursive(falseexpr, cond, false) && fno_change;
166 }
167
168 if(!tno_change)
169 trueexpr = simplify_rec(trueexpr); // recursive call
170 if(!fno_change)
171 falseexpr = simplify_rec(falseexpr); // recursive call
172
173 return tno_change && fno_change;
174}
175
177{
178 bool no_change = true;
179 bool tmp = false;
180
181 while(!tmp)
182 {
183 tmp = true;
184
185 if(expr.id() == ID_and)
186 {
187 if(expr.has_operands())
188 {
189 exprt::operandst &operands = expr.operands();
190 for(exprt::operandst::iterator it1 = operands.begin();
191 it1 != operands.end();
192 it1++)
193 {
194 for(exprt::operandst::iterator it2 = operands.begin();
195 it2 != operands.end();
196 it2++)
197 {
198 if(it1 != it2)
199 tmp = simplify_if_recursive(*it1, *it2, true) && tmp;
200 }
201 }
202 }
203 }
204
205 if(!tmp)
206 expr = simplify_rec(expr); // recursive call
207
208 no_change = tmp && no_change;
209 }
210
211 return no_change;
212}
213
215{
216 exprt &cond = expr.cond();
217 exprt &truevalue = expr.true_case();
218 exprt &falsevalue = expr.false_case();
219
220 bool no_change = true;
221
222 // we first want to look at the condition
223 auto r_cond = simplify_rec(cond);
224 if(r_cond.has_changed())
225 {
226 cond = r_cond.expr;
227 no_change = false;
228 }
229
230 // 1 ? a : b -> a and 0 ? a : b -> b
231 if(cond.is_constant())
232 {
233 exprt tmp = cond.is_true() ? truevalue : falsevalue;
234 tmp = simplify_rec(tmp);
235 expr.swap(tmp);
236 return false;
237 }
238
240 {
241 if(cond.id() == ID_not)
242 {
243 cond = to_not_expr(cond).op();
244 truevalue.swap(falsevalue);
245 no_change = false;
246 }
247
248#ifdef USE_LOCAL_REPLACE_MAP
249 replace_mapt map_before(local_replace_map);
250
251 // a ? b : c --> a ? b[a/true] : c
252 if(cond.id() == ID_and)
253 {
254 forall_operands(it, cond)
255 {
256 if(it->id() == ID_not)
257 local_replace_map.insert(std::make_pair(it->op0(), false_exprt()));
258 else
259 local_replace_map.insert(std::make_pair(*it, true_exprt()));
260 }
261 }
262 else
263 local_replace_map.insert(std::make_pair(cond, true_exprt()));
264
265 auto r_truevalue = simplify_rec(truevalue);
266 if(r_truevalue.has_changed())
267 {
268 truevalue = r_truevalue.expr;
269 no_change = false;
270 }
271
272 local_replace_map = map_before;
273
274 // a ? b : c --> a ? b : c[a/false]
275 if(cond.id() == ID_or)
276 {
277 forall_operands(it, cond)
278 {
279 if(it->id() == ID_not)
280 local_replace_map.insert(std::make_pair(it->op0(), true_exprt()));
281 else
282 local_replace_map.insert(std::make_pair(*it, false_exprt()));
283 }
284 }
285 else
286 local_replace_map.insert(std::make_pair(cond, false_exprt()));
287
288 auto r_falsevalue = simplify_rec(falsevalue);
289 if(r_falsevalue.has_changed())
290 {
291 falsevalue = r_falsevalue.expr;
292 no_change = false;
293 }
294
295 local_replace_map.swap(map_before);
296#else
297 auto r_truevalue = simplify_rec(truevalue);
298 if(r_truevalue.has_changed())
299 {
300 truevalue = r_truevalue.expr;
301 no_change = false;
302 }
303 auto r_falsevalue = simplify_rec(falsevalue);
304 if(r_falsevalue.has_changed())
305 {
306 falsevalue = r_falsevalue.expr;
307 no_change = false;
308 }
309#endif
310 }
311 else
312 {
313 auto r_truevalue = simplify_rec(truevalue);
314 if(r_truevalue.has_changed())
315 {
316 truevalue = r_truevalue.expr;
317 no_change = false;
318 }
319 auto r_falsevalue = simplify_rec(falsevalue);
320 if(r_falsevalue.has_changed())
321 {
322 falsevalue = r_falsevalue.expr;
323 no_change = false;
324 }
325 }
326
327 return no_change;
328}
329
331{
332 const exprt &cond = expr.cond();
333 const exprt &truevalue = expr.true_case();
334 const exprt &falsevalue = expr.false_case();
335
337 {
338#if 0
339 no_change = simplify_if_cond(cond) && no_change;
340 no_change = simplify_if_branch(truevalue, falsevalue, cond) && no_change;
341#endif
342
343 if(expr.type() == bool_typet())
344 {
345 // a?b:c <-> (a && b) || (!a && c)
346
347 if(truevalue.is_true() && falsevalue.is_false())
348 {
349 // a?1:0 <-> a
350 return cond;
351 }
352 else if(truevalue.is_false() && falsevalue.is_true())
353 {
354 // a?0:1 <-> !a
355 return changed(simplify_not(not_exprt(cond)));
356 }
357 else if(falsevalue.is_false())
358 {
359 // a?b:0 <-> a AND b
360 return changed(simplify_boolean(and_exprt(cond, truevalue)));
361 }
362 else if(falsevalue.is_true())
363 {
364 // a?b:1 <-> !a OR b
365 return changed(
366 simplify_boolean(or_exprt(simplify_not(not_exprt(cond)), truevalue)));
367 }
368 else if(truevalue.is_true())
369 {
370 // a?1:b <-> a||(!a && b) <-> a OR b
371 return changed(simplify_boolean(or_exprt(cond, falsevalue)));
372 }
373 else if(truevalue.is_false())
374 {
375 // a?0:b <-> !a && b
377 and_exprt(simplify_not(not_exprt(cond)), falsevalue)));
378 }
379 }
380 }
381
382 if(truevalue == falsevalue)
383 return truevalue;
384
385 // this pushes the if-then-else into struct and array constructors
386 if(
387 ((truevalue.id() == ID_struct && falsevalue.id() == ID_struct) ||
388 (truevalue.id() == ID_array && falsevalue.id() == ID_array)) &&
389 truevalue.operands().size() == falsevalue.operands().size())
390 {
391 exprt cond_copy = cond;
392 exprt falsevalue_copy = falsevalue;
393 exprt truevalue_copy = truevalue;
394
395 auto range_false = make_range(falsevalue_copy.operands());
396 auto range_true = make_range(truevalue_copy.operands());
397 auto new_expr = truevalue;
398 new_expr.operands().clear();
399
400 for(const auto &pair : range_true.zip(range_false))
401 {
402 new_expr.operands().push_back(
403 simplify_if(if_exprt(cond_copy, pair.first, pair.second)));
404 }
405
406 return std::move(new_expr);
407 }
408
409 return unchanged(expr);
410}
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
Boolean AND.
Definition: std_expr.h:1974
The Boolean type.
Definition: std_types.h:36
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
The Boolean constant false.
Definition: std_expr.h:2865
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
Boolean negation.
Definition: std_expr.h:2181
Boolean OR.
Definition: std_expr.h:2082
bool simplify_if_conj(exprt &expr, const exprt &cond)
bool simplify_if_disj(exprt &expr, const exprt &cond)
static resultt changed(resultt<> result)
bool simplify_if_preorder(if_exprt &expr)
resultt simplify_if(const if_exprt &)
bool simplify_if_recursive(exprt &expr, const exprt &cond, bool truth)
resultt simplify_rec(const exprt &)
bool simplify_if_cond(exprt &expr)
resultt simplify_boolean(const exprt &)
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
resultt simplify_not(const not_exprt &)
static resultt unchanged(exprt expr)
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
The Boolean constant true.
Definition: std_expr.h:2856
const exprt & op() const
Definition: std_expr.h:293
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
BigInt mp_integer
Definition: smt_terms.h:12
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206