12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H 79 std::map<exprt, int> &values,
80 std::set<std::pair<expr_listt, exprt>> &coefficients,
87 std::set<std::pair<expr_listt, exprt>> &coefficients,
101 std::map<exprt, polynomialt> polynomials,
109 std::map<exprt, polynomialt> &polynomials,
110 std::map<exprt, exprt> &stashed,
116 std::map<exprt, polynomialt> polynomials,
130 typedef std::vector<polynomial_array_assignmentt>
135 std::map<exprt, polynomialt> &polynomials,
144 std::map<exprt, polynomialt> &polynomials,
149 std::map<exprt, polynomialt> &polynomials,
166 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H std::vector< expr_pairt > expr_pairst
void ensure_no_overflows(goto_programt &program)
exprt precondition(patht &path)
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
Goto Programs with Functions.
std::vector< polynomialt > polynomialst
expr_sett find_modified(goto_programt::instructionst &body)
void assert_for_values(scratch_programt &program, std::map< exprt, int > &values, std::set< std::pair< expr_listt, exprt >> &coefficients, int num_unwindings, goto_programt::instructionst &loop_body, exprt &target, overflow_instrumentert &overflow)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
std::list< instructiont > instructionst
const goto_functionst & goto_functions
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
std::unordered_set< exprt, irep_hash > expr_sett
virtual bool accelerate(patht &loop, path_acceleratort &accelerator)
std::list< path_nodet > patht
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
message_handlert & message_handler
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
A generic container class for the GOTO intermediate representation of one function.
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
Base class for all expressions.
std::pair< exprt, exprt > expr_pairt
std::map< exprt, exprt > substitutiont
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
acceleration_utilst utils
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
symbol_tablet & symbol_table