27 if(truth && cond.
id() == ID_lt && expr.
id() == ID_lt)
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())
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())
79 if(expr.
type().
id() == ID_bool)
98 bool no_change =
true;
117 bool no_change =
true;
136 bool no_change =
true;
149 bool tno_change =
true;
150 bool fno_change =
true;
152 if(cond.
id() == ID_and)
157 else if(cond.
id() == ID_or)
173 return tno_change && fno_change;
178 bool no_change =
true;
185 if(expr.
id() == ID_and)
190 for(exprt::operandst::iterator it1 = operands.begin();
191 it1 != operands.end();
194 for(exprt::operandst::iterator it2 = operands.begin();
195 it2 != operands.end();
208 no_change = tmp && no_change;
220 bool no_change =
true;
224 if(r_cond.has_changed())
241 if(cond.
id() == ID_not)
244 truevalue.
swap(falsevalue);
248 #ifdef USE_LOCAL_REPLACE_MAP
252 if(cond.
id() == ID_and)
256 if(it->id() == ID_not)
257 local_replace_map.insert(std::make_pair(it->op0(),
false_exprt()));
259 local_replace_map.insert(std::make_pair(*it,
true_exprt()));
263 local_replace_map.insert(std::make_pair(cond,
true_exprt()));
266 if(r_truevalue.has_changed())
268 truevalue = r_truevalue.expr;
272 local_replace_map = map_before;
275 if(cond.
id() == ID_or)
279 if(it->id() == ID_not)
280 local_replace_map.insert(std::make_pair(it->op0(),
true_exprt()));
282 local_replace_map.insert(std::make_pair(*it,
false_exprt()));
286 local_replace_map.insert(std::make_pair(cond,
false_exprt()));
289 if(r_falsevalue.has_changed())
291 falsevalue = r_falsevalue.expr;
295 local_replace_map.
swap(map_before);
298 if(r_truevalue.has_changed())
300 truevalue = r_truevalue.expr;
304 if(r_falsevalue.has_changed())
306 falsevalue = r_falsevalue.expr;
314 if(r_truevalue.has_changed())
316 truevalue = r_truevalue.expr;
320 if(r_falsevalue.has_changed())
322 falsevalue = r_falsevalue.expr;
382 if(truevalue == falsevalue)
387 ((truevalue.
id() == ID_struct && falsevalue.
id() == ID_struct) ||
388 (truevalue.
id() == ID_array && falsevalue.
id() == ID_array)) &&
391 exprt cond_copy = cond;
392 exprt falsevalue_copy = falsevalue;
393 exprt truevalue_copy = truevalue;
397 auto new_expr = truevalue;
400 for(
const auto &pair : range_true.zip(range_false))
402 new_expr.operands().push_back(
406 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)
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.
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
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.