12#ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
13#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
82 std::map<exprt, int> &values,
83 std::set<std::pair<expr_listt, exprt>> &coefficients,
90 std::set<std::pair<expr_listt, exprt>> &coefficients,
104 std::map<exprt, polynomialt> polynomials,
112 std::map<exprt, polynomialt> &polynomials,
113 std::map<exprt, exprt> &stashed,
119 std::map<exprt, polynomialt> polynomials,
133 typedef std::vector<polynomial_array_assignmentt>
138 std::map<exprt, polynomialt> &polynomials,
146 std::map<exprt, polynomialt> &polynomials,
151 std::map<exprt, polynomialt> &polynomials,
Base class for all expressions.
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
std::list< instructiont > instructionst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
acceleration_utilst utils
std::vector< expr_pairt > expr_pairst
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)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
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, exprt &_loop_counter, guard_managert &guard_manager)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
std::pair< exprt, exprt > expr_pairt
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
bool accelerate(patht &loop, path_acceleratort &accelerator)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
symbol_tablet & symbol_table
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
const goto_functionst & goto_functions
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, guard_managert &guard_manager)
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
guard_managert & guard_manager
exprt precondition(patht &path)
void ensure_no_overflows(goto_programt &program)
message_handlert & message_handler
std::unordered_set< exprt, irep_hash > expr_sett
std::list< path_nodet > patht
std::vector< polynomialt > polynomialst
std::map< exprt, exprt > substitutiont
expr_sett find_modified(goto_programt::instructionst &body)
This is unused by this implementation of guards, but can be used by other implementations of the same...