12 #ifndef CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H 13 #define CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H 59 #endif // CPROVER_SOLVERS_FLATTENING_FUNCTIONS_H application of (mathematical) function
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
functionst(prop_convt &_prop_conv)
function_mapt function_map
std::set< function_application_exprt > applicationst
API to expression classes.
std::vector< exprt > operandst
virtual void add_function_constraints()
void record(const function_application_exprt &function_application)
Base class for all expressions.
applicationst applications
std::map< exprt, function_infot > function_mapt
virtual void post_process()