CBMC
simplify_expr_if.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "simplify_expr_class.h"
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.is_boolean())
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  for(const auto &op : cond.operands())
109  {
110  if(expr == op)
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  for(const auto &op : cond.operands())
128  {
129  if(expr == op)
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  const if_exprt &expr,
217  simplify_exprt::resultt<> truevalue,
218  simplify_exprt::resultt<> falsevalue)
219 {
220  if(
221  !cond.has_changed() && !truevalue.has_changed() &&
222  !falsevalue.has_changed())
223  {
226  }
227  else
228  {
229  if_exprt result = expr;
230  if(cond.has_changed())
231  result.cond() = std::move(cond.expr);
232  if(truevalue.has_changed())
233  result.true_case() = std::move(truevalue.expr);
234  if(falsevalue.has_changed())
235  result.false_case() = std::move(falsevalue.expr);
236  return result;
237  }
238 }
239 
242 {
243  const exprt &cond = expr.cond();
244  const exprt &truevalue = expr.true_case();
245  const exprt &falsevalue = expr.false_case();
246 
247  // we first want to look at the condition
248  auto r_cond = simplify_rec(cond);
249 
250  // 1 ? a : b -> a and 0 ? a : b -> b
251  if(r_cond.expr.is_constant())
252  {
253  return changed(
254  simplify_rec(r_cond.expr.is_true() ? truevalue : falsevalue));
255  }
256 
257  if(do_simplify_if)
258  {
259  bool swap_branches = false;
260 
261  if(r_cond.expr.id() == ID_not)
262  {
263  r_cond = changed(to_not_expr(r_cond.expr).op());
264  swap_branches = true;
265  }
266 
267 #ifdef USE_LOCAL_REPLACE_MAP
268  replace_mapt map_before(local_replace_map);
269 
270  // a ? b : c --> a ? b[a/true] : c
271  if(r_cond.expr.id() == ID_and)
272  {
273  for(const auto &op : r_cond.expr.operands())
274  {
275  if(op.id() == ID_not)
276  local_replace_map.insert(std::make_pair(op.op0(), false_exprt()));
277  else
278  local_replace_map.insert(std::make_pair(op, true_exprt()));
279  }
280  }
281  else
282  local_replace_map.insert(std::make_pair(r_cond.expr, true_exprt()));
283 
284  auto r_truevalue = simplify_rec(swap_branches ? falsevalue : truevalue);
285 
286  local_replace_map = map_before;
287 
288  // a ? b : c --> a ? b : c[a/false]
289  if(r_cond.expr.id() == ID_or)
290  {
291  for(const auto &op : r_cond.expr.operands())
292  {
293  if(op.id() == ID_not)
294  local_replace_map.insert(std::make_pair(op.op0(), true_exprt()));
295  else
296  local_replace_map.insert(std::make_pair(op, false_exprt()));
297  }
298  }
299  else
300  local_replace_map.insert(std::make_pair(r_cond.expr, false_exprt()));
301 
302  auto r_falsevalue = simplify_rec(swap_branches ? truevalue : falsevalue);
303 
304  local_replace_map.swap(map_before);
305 
306  if(swap_branches)
307  {
308  // tell build_if_expr to replace truevalue and falsevalue
309  r_truevalue.expr_changed = CHANGED;
310  r_falsevalue.expr_changed = CHANGED;
311  }
312  return build_if_expr(expr, r_cond, r_truevalue, r_falsevalue);
313 #else
314  if(!swap_branches)
315  {
316  return build_if_expr(
317  expr, r_cond, simplify_rec(truevalue), simplify_rec(falsevalue));
318  }
319  else
320  {
321  return build_if_expr(
322  expr,
323  r_cond,
324  changed(simplify_rec(falsevalue)),
325  changed(simplify_rec(truevalue)));
326  }
327 #endif
328  }
329  else
330  {
331  return build_if_expr(
332  expr, r_cond, simplify_rec(truevalue), simplify_rec(falsevalue));
333  }
334 }
335 
337 {
338  const exprt &cond = expr.cond();
339  const exprt &truevalue = expr.true_case();
340  const exprt &falsevalue = expr.false_case();
341 
342  if(do_simplify_if)
343  {
344 #if 0
345  no_change = simplify_if_cond(cond) && no_change;
346  no_change = simplify_if_branch(truevalue, falsevalue, cond) && no_change;
347 #endif
348 
349  if(expr.type() == bool_typet())
350  {
351  // a?b:c <-> (a && b) || (!a && c)
352 
353  if(truevalue.is_true() && falsevalue.is_false())
354  {
355  // a?1:0 <-> a
356  return cond;
357  }
358  else if(truevalue.is_false() && falsevalue.is_true())
359  {
360  // a?0:1 <-> !a
361  return changed(simplify_not(not_exprt(cond)));
362  }
363  else if(falsevalue.is_false())
364  {
365  // a?b:0 <-> a AND b
366  return changed(simplify_boolean(and_exprt(cond, truevalue)));
367  }
368  else if(falsevalue.is_true())
369  {
370  // a?b:1 <-> !a OR b
371  return changed(
372  simplify_boolean(or_exprt(simplify_not(not_exprt(cond)), truevalue)));
373  }
374  else if(truevalue.is_true())
375  {
376  // a?1:b <-> a||(!a && b) <-> a OR b
377  return changed(simplify_boolean(or_exprt(cond, falsevalue)));
378  }
379  else if(truevalue.is_false())
380  {
381  // a?0:b <-> !a && b
382  return changed(simplify_boolean(
383  and_exprt(simplify_not(not_exprt(cond)), falsevalue)));
384  }
385  }
386  }
387 
388  if(truevalue == falsevalue)
389  return truevalue;
390 
391  // this pushes the if-then-else into struct and array constructors
392  if(
393  ((truevalue.id() == ID_struct && falsevalue.id() == ID_struct) ||
394  (truevalue.id() == ID_array && falsevalue.id() == ID_array)) &&
395  truevalue.operands().size() == falsevalue.operands().size())
396  {
397  exprt cond_copy = cond;
398  exprt falsevalue_copy = falsevalue;
399  exprt truevalue_copy = truevalue;
400 
401  auto range_false = make_range(falsevalue_copy.operands());
402  auto range_true = make_range(truevalue_copy.operands());
403  auto new_expr = truevalue;
404  new_expr.operands().clear();
405 
406  for(const auto &pair : range_true.zip(range_false))
407  {
408  new_expr.operands().push_back(
409  simplify_if(if_exprt(cond_copy, pair.first, pair.second)));
410  }
411 
412  return std::move(new_expr);
413  }
414 
415  return unchanged(expr);
416 }
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:20
Boolean AND.
Definition: std_expr.h:2125
The Boolean type.
Definition: std_types.h:36
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
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
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3082
The trinary if-then-else operator.
Definition: std_expr.h:2380
exprt & true_case()
Definition: std_expr.h:2407
exprt & false_case()
Definition: std_expr.h:2417
exprt & cond()
Definition: std_expr.h:2397
const irep_idt & id() const
Definition: irep.h:388
Boolean negation.
Definition: std_expr.h:2337
Boolean OR.
Definition: std_expr.h:2233
bool simplify_if_conj(exprt &expr, const exprt &cond)
bool simplify_if_disj(exprt &expr, const exprt &cond)
static resultt changed(resultt<> result)
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)
resultt simplify_if_preorder(const if_exprt &expr)
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
The Boolean constant true.
Definition: std_expr.h:3073
const exprt & op() const
Definition: std_expr.h:391
#define Forall_operands(it, expr)
Definition: expr.h:27
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:522
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
static simplify_exprt::resultt build_if_expr(const if_exprt &expr, simplify_exprt::resultt<> cond, simplify_exprt::resultt<> truevalue, simplify_exprt::resultt<> falsevalue)
BigInt mp_integer
Definition: smt_terms.h:17
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2362
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:895