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
83 std::map<exprt, int> &values,
84 std::set<std::pair<expr_listt, exprt>> &coefficients,
91 std::set<std::pair<expr_listt, exprt>> &coefficients,
105 std::map<exprt, polynomialt> polynomials,
113 std::map<exprt, polynomialt> &polynomials,
114 std::map<exprt, exprt> &stashed,
120 std::map<exprt, polynomialt> polynomials,
134 typedef std::vector<polynomial_array_assignmentt>
139 std::map<exprt, polynomialt> &polynomials,
147 std::map<exprt, polynomialt> &polynomials,
152 std::map<exprt, polynomialt> &polynomials,
170 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
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...
This is unused by this implementation of guards, but can be used by other implementations of the same...
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, guard_managert &guard_manager)
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
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter, guard_managert &guard_manager)
std::map< exprt, exprt > substitutiont
A collection of goto functions.
std::list< path_nodet > patht
std::vector< polynomialt > polynomialst
Goto Programs with Functions.
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)
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
acceleration_utilst utils
guard_managert & guard_manager