Go to the documentation of this file.
12 #ifndef CPROVER_SOLVERS_LOWERING_FUNCTIONS_H
13 #define CPROVER_SOLVERS_LOWERING_FUNCTIONS_H
60 #endif // CPROVER_SOLVERS_LOWERING_FUNCTIONS_H
virtual void post_process()
function_mapt function_map
Base class for all expressions.
exprt arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2)
Decision Procedure Interface.
applicationst applications
functionst(decision_proceduret &_decision_procedure)
std::set< function_application_exprt > applicationst
void record(const function_application_exprt &function_application)
Application of (mathematical) function.
decision_proceduret & decision_procedure
std::vector< exprt > operandst
virtual void add_function_constraints()
std::map< exprt, function_infot > function_mapt
API to expression classes for 'mathematical' expressions.