Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
33 typedef std::unordered_map<exprt, exprt, irep_hash>
expr_mapt;
68 std::set<std::pair<expr_listt, exprt> > &coefficients,
77 std::map<exprt, polynomialt> &polynomials,
78 std::map<exprt, exprt> &stashed,
99 typedef std::vector<polynomial_array_assignmentt>
103 std::map<exprt, polynomialt> &polynomials,
111 std::map<exprt, polynomialt> &polynomials,
116 std::map<exprt, polynomialt> &polynomials,
121 std::map<exprt, polynomialt> &polynomials,
159 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
symbol_tablet & symbol_table
std::vector< expr_pairt > expr_pairst
The type of an expression, extends irept.
symbolt fresh_symbol(std::string base, typet type)
void push_nondet(exprt &expr)
std::list< exprt > expr_listt
std::list< instructiont > instructionst
const goto_functionst & goto_functions
message_handlert & message_handler
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
Base class for all expressions.
void find_modified(const patht &path, expr_sett &modified)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
acceleration_utilst(symbol_tablet &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions, exprt &_loop_counter)
exprt precondition(patht &path)
std::unordered_set< exprt, irep_hash > expr_sett
void ensure_no_overflows(scratch_programt &program)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
std::map< exprt, exprt > substitutiont
A collection of goto functions.
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path)
std::list< path_nodet > patht
std::pair< exprt, exprt > expr_pairt
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
std::vector< polynomialt > polynomialst
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
acceleration_utilst(symbol_tablet &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions)
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
bool assign_array(const exprt &lhs, const exprt &rhs, scratch_programt &program)
std::set< goto_programt::targett > natural_loopt
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)