18 function_application);
34 conjuncts.reserve(o1.size());
36 for(std::size_t i = 0; i < o1.size(); i++)
51 for(std::set<function_application_exprt>::const_iterator it1 =
56 for(std::set<function_application_exprt>::const_iterator it2 =
61 exprt arguments_equal_expr =
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
Base class for all expressions.
std::vector< exprt > operandst
Application of (mathematical) function.
function_mapt function_map
virtual void add_function_constraints()
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
void record(const function_application_exprt &function_application)
decision_proceduret & decision_procedure
static exprt conditional_cast(const exprt &expr, const typet &type)
Decision Procedure Interface.
static exprt implication(exprt lhs, exprt rhs)
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
applicationst applications