33 "logical and, or, and xor expressions have at least two operands");
50 return n_lhs.bdd_or(rhs);
73 std::pair<expr_mapt::iterator, bool> entry =
83 return entry.first->second;
98 b.add_to_operands(std::move(
a));
109 std::unordered_map<bdd_nodet::idt, exprt> &cache)
const
113 if(
r.is_complement())
128 if(
r.else_branch().is_constant())
130 if(
r.then_branch().is_constant())
132 if(
r.else_branch().is_complement())
138 if(
r.else_branch().is_complement())
147 else if(
r.then_branch().is_constant())
149 if(
r.then_branch().is_complement())
173 std::unordered_map<bdd_nodet::idt, exprt> cache;
static exprt make_or(exprt a, exprt b)
Disjunction of two expressions.
Conversion between exprt and miniBDD.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
std::vector< exprt > node_map
Mapping from BDD variables to expressions: the expression at index i of node_map corresponds to the i...
exprt as_expr(const bddt &root) const
bddt from_expr_rec(const exprt &expr)
bddt from_expr(const exprt &expr)
bdd_nodet bdd_node(const bddt &bdd) const
bddt bdd_variable(bdd_nodet::indext index)
Low level access to the structure of the BDD, read-only.
Logical operations on BDDs.
bddt bdd_xor(const bddt &other) const
static bddt bdd_ite(const bddt &i, const bddt &t, const bddt &e)
bddt bdd_or(const bddt &other) const
bddt bdd_and(const bddt &other) const
Base class for all expressions.
bool is_boolean() const
Return whether the expression represents a Boolean.
bool is_false() const
Return whether the expression is a constant representing false.
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
The Boolean constant true.
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
const implies_exprt & to_implies_expr(const exprt &expr)
Cast an exprt to a implies_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.