Go to the documentation of this file.
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,
143 std::map<exprt, polynomialt> &polynomials,
148 std::map<exprt, polynomialt> &polynomials,
165 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
message_handlert & message_handler
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
std::vector< expr_pairt > expr_pairst
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
std::list< instructiont > instructionst
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
Base class for all expressions.
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
symbol_tablet & symbol_table
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
bool accelerate(patht &loop, path_acceleratort &accelerator)
exprt precondition(patht &path)
void ensure_no_overflows(goto_programt &program)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
std::unordered_set< exprt, irep_hash > expr_sett
const goto_functionst & goto_functions
std::map< exprt, exprt > substitutiont
A collection of goto functions.
std::list< path_nodet > patht
std::vector< polynomialt > polynomialst
std::pair< exprt, exprt > expr_pairt
A generic container class for the GOTO intermediate representation of one function.
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
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)
expr_sett find_modified(goto_programt::instructionst &body)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
acceleration_utilst utils