Go to the documentation of this file.
17 function_application);
33 conjuncts.reserve(o1.size());
35 for(std::size_t i = 0; i < o1.size(); i++)
50 for(std::set<function_application_exprt>::const_iterator it1 =
55 for(std::set<function_application_exprt>::const_iterator it2 =
60 exprt arguments_equal_expr =
static exprt conditional_cast(const exprt &expr, const typet &type)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
function_mapt function_map
Base class for all expressions.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
applicationst applications
typet & type()
Return the type of the expression.
void record(const function_application_exprt &function_application)
#define PRECONDITION(CONDITION)
Application of (mathematical) function.
decision_proceduret & decision_procedure
std::vector< exprt > operandst
virtual void add_function_constraints()
API to expression classes.