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);
Base class for all expressions.
std::vector< exprt > operandst
bool has_operands() const
Return true if there is at least one operand.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
The Boolean constant false.
The trinary if-then-else operator.
const irep_idt & id() const
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)
bool simplify_if_branch(exprt &trueexpr, exprt &falseexpr, const exprt &cond)
resultt simplify_not(const not_exprt &)
static resultt unchanged(exprt expr)
resultt simplify_node(exprt)
bool simplify_if_implies(exprt &expr, const exprt &cond, bool truth, bool &new_truth)
The Boolean constant true.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
Deprecated expression utility functions.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.