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