27 else if(expr.
id()==ID_not)
29 else if(expr.
id()==ID_and ||
35 "logical and, or, and xor expressions have at least two operands");
41 return expr.
id()==ID_and ? (op0&op1) :
42 (expr.
id()==ID_or ? (op0|op1) : (op0^op1));
44 else if(expr.
id()==ID_implies)
53 else if(expr.
id()==ID_equal &&
64 else if(expr.
id()==ID_if)
72 return ((!cond)|t_case)&(cond|f_case);
76 std::pair<expr_mapt::iterator, bool> entry=
85 node_map.insert(std::make_pair(entry.first->second.var(),
89 return entry.first->second;
108 node_mapt::const_iterator entry=
node_map.find(
r.var());
110 const exprt &n_expr=entry->second;
112 if(
r.low().is_false())
114 if(
r.high().is_true())
119 else if(
r.high().is_false())
121 if(
r.low().is_true())
126 else if(
r.low().is_true())
128 else if(
r.high().is_true())
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Deprecated expression utility functions.
bool is_false() const
Return whether the expression is a constant representing false.
const mini_bddt & False() const
The trinary if-then-else operator.
typet & type()
Return the type of the expression.
#define CHECK_RETURN(CONDITION)
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an 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.
#define PRECONDITION(CONDITION)
mini_bddt from_expr_rec(const exprt &expr)
The Boolean constant false.
bool is_constant() const
Return whether the expression is a constant.
void from_expr(const exprt &expr)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an 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 an exprt to an not_exprt.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions