12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H 49 exprt &_loop_counter):
74 std::map<exprt, int> &values,
75 std::set<std::pair<expr_listt, exprt>> &coefficients,
82 std::set<std::pair<expr_listt, exprt>> &coefficients,
96 std::map<exprt, polynomialt> polynomials,
104 std::map<exprt, polynomialt> &polynomials,
105 std::map<exprt, exprt> &stashed,
111 std::map<exprt, polynomialt> polynomials,
125 typedef std::vector<polynomial_array_assignmentt>
130 std::map<exprt, polynomialt> &polynomials,
139 std::map<exprt, polynomialt> &polynomials,
144 std::map<exprt, polynomialt> &polynomials,
161 #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)
std::list< instructiont > instructionst
polynomial_acceleratort(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
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)
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)
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 specialization of goto_program_templatet over goto programs in which instructions have codet type...
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)
polynomial_acceleratort(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
symbol_tablet & symbol_table