22 assert(expr.
type().
id()==ID_bool);
26 else if(expr.
id()==ID_not)
28 else if(expr.
id()==ID_and ||
38 return expr.
id()==ID_and ? (op0&op1) :
39 (expr.
id()==ID_or ? (op0|op1) : (op0^op1));
41 else if(expr.
id()==ID_implies)
50 else if(expr.
id()==ID_equal &&
61 else if(expr.
id()==ID_iff)
70 else if(expr.
id()==ID_if)
78 return ((!cond)|t_case)&(cond|f_case);
82 std::pair<expr_mapt::iterator, bool> entry=
91 node_map.insert(std::make_pair(entry.first->second.var(),
95 return entry.first->second;
114 node_mapt::const_iterator entry=
node_map.find(
r.var());
116 const exprt &n_expr=entry->second;
118 if(
r.low().is_false())
120 if(
r.high().is_true())
125 else if(
r.high().is_false())
127 if(
r.low().is_true())
132 else if(
r.low().is_true())
134 else if(
r.high().is_true())
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Deprecated expression utility functions.
const mini_bddt & False() const
The trinary if-then-else operator.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast a generic exprt to a implies_exprt.
Conversion between exprt and miniBDD.
const irep_idt & id() const
The boolean constant true.
bool is_initialized() const
API to expression classes.
mini_bddt from_expr_rec(const exprt &expr)
The boolean constant false.
void from_expr(const exprt &expr)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
mini_bddt Var(const std::string &label)
const mini_bddt & True() const
Base class for all expressions.
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions