12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H 31 typedef std::unordered_map<exprt, exprt, irep_hash>
expr_mapt;
38 exprt &_loop_counter) :
56 std::set<std::pair<expr_listt, exprt> > &coefficients,
65 std::map<exprt, polynomialt> &polynomials,
66 std::map<exprt, exprt> &stashed,
87 typedef std::vector<polynomial_array_assignmentt>
91 std::map<exprt, polynomialt> &polynomials,
100 std::map<exprt, polynomialt> &polynomials,
105 std::map<exprt, polynomialt> &polynomials,
110 std::map<exprt, polynomialt> &polynomials,
152 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H The type of an expression.
acceleration_utilst(symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
std::pair< exprt, exprt > expr_pairt
std::list< instructiont > instructionst
exprt precondition(patht &path)
Goto Programs with Functions.
std::set< goto_programt::targett > natural_loopt
std::vector< polynomialt > polynomialst
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
instructionst::const_iterator const_targett
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
void ensure_no_overflows(scratch_programt &program)
std::vector< expr_pairt > expr_pairst
std::unordered_set< exprt, irep_hash > expr_sett
symbolt fresh_symbol(std::string base, typet type)
bool assign_array(const exprt &lhs, const exprt &rhs, const exprt &loop_counter, scratch_programt &program)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
std::list< path_nodet > patht
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
const goto_functionst & goto_functions
void find_modified(const patht &path, expr_sett &modified)
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
acceleration_utilst(symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
Base class for all expressions.
std::map< exprt, exprt > substitutiont
void push_nondet(exprt &expr)
symbol_tablet & symbol_table
Compute natural loops in a goto_function.
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)