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