28 if(truth && cond.
id() == ID_lt && expr.
id() == ID_lt)
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())
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())
80 if(expr.
type().
id() == ID_bool)
99 bool no_change =
true;
118 bool no_change =
true;
137 bool no_change =
true;
150 bool tno_change =
true;
151 bool fno_change =
true;
153 if(cond.
id() == ID_and)
158 else if(cond.
id() == ID_or)
174 return tno_change && fno_change;
179 bool no_change =
true;
186 if(expr.
id() == ID_and)
191 for(exprt::operandst::iterator it1 = operands.begin();
192 it1 != operands.end();
195 for(exprt::operandst::iterator it2 = operands.begin();
196 it2 != operands.end();
209 no_change = tmp && no_change;
221 bool no_change =
true;
225 if(r_cond.has_changed())
242 if(cond.
id() == ID_not)
245 truevalue.
swap(falsevalue);
249 #ifdef USE_LOCAL_REPLACE_MAP
253 if(cond.
id() == ID_and)
257 if(it->id() == ID_not)
258 local_replace_map.insert(std::make_pair(it->op0(),
false_exprt()));
260 local_replace_map.insert(std::make_pair(*it,
true_exprt()));
264 local_replace_map.insert(std::make_pair(cond,
true_exprt()));
267 if(r_truevalue.has_changed())
269 truevalue = r_truevalue.expr;
273 local_replace_map = map_before;
276 if(cond.
id() == ID_or)
280 if(it->id() == ID_not)
281 local_replace_map.insert(std::make_pair(it->op0(),
true_exprt()));
283 local_replace_map.insert(std::make_pair(*it,
false_exprt()));
287 local_replace_map.insert(std::make_pair(cond,
false_exprt()));
290 if(r_falsevalue.has_changed())
292 falsevalue = r_falsevalue.expr;
296 local_replace_map.
swap(map_before);
299 if(r_truevalue.has_changed())
301 truevalue = r_truevalue.expr;
305 if(r_falsevalue.has_changed())
307 falsevalue = r_falsevalue.expr;
315 if(r_truevalue.has_changed())
317 truevalue = r_truevalue.expr;
321 if(r_falsevalue.has_changed())
323 falsevalue = r_falsevalue.expr;
383 if(truevalue == falsevalue)
388 ((truevalue.
id() == ID_struct && falsevalue.
id() == ID_struct) ||
389 (truevalue.
id() == ID_array && falsevalue.
id() == ID_array)) &&
392 exprt cond_copy = cond;
393 exprt falsevalue_copy = falsevalue;
394 exprt truevalue_copy = truevalue;
398 auto new_expr = truevalue;
401 for(
const auto &pair : range_true.zip(range_false))
403 new_expr.operands().push_back(
407 return std::move(new_expr);