12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H 82 patht &inserted_path);
100 trace_automatont::sym_mapt::iterator p,
101 trace_automatont::sym_mapt::iterator end,
121 typedef std::map<goto_programt::targett, goto_programt::targetst>
135 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
The type of an expression, extends irept.
void insert_automaton(trace_automatont &automaton)
acceleratet(goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, bool _use_z3)
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
natural_loops_mutablet natural_loops
static const int accelerate_limit
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
goto_functionst & goto_functions
bool contains_nested_loops(goto_programt::targett &loop_header)
std::list< subsumed_patht > subsumed_pathst
Goto Programs with Functions.
message_handlert & message_handler
std::set< goto_programt::targett > natural_loopt
int accelerate_loop(goto_programt::targett &loop_header)
void set_dirty_vars(path_acceleratort &accelerator)
symbol_tablet & symbol_table
instructionst::iterator targett
void extend_path(goto_programt::targett &t, goto_programt::targett &loop_header, natural_loops_mutablet::natural_loopt &loop, patht &prefix, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
std::list< path_nodet > patht
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool is_underapproximate(path_acceleratort &accelerator)
std::list< patht > pathst
A collection of goto functions.
void find_paths(goto_programt::targett &loop_header, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
std::set< statet > state_sett
symbolt make_symbol(std::string name, typet type)
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
A generic container class for the GOTO intermediate representation of one function.
std::map< goto_programt::targett, goto_programt::targetst > overflow_mapt
void decl(symbol_exprt &sym, goto_programt::targett t)
void accelerate_functions(goto_modelt &, message_handlert &message_handler, bool use_z3)
bool accelerate_path(patht &path, path_acceleratort &accelerator)
Base class for all expressions.
overflow_mapt overflow_locs
void build_state_machine(trace_automatont::sym_mapt::iterator p, trace_automatont::sym_mapt::iterator end, state_sett &accept_states, symbol_exprt state, symbol_exprt next_state, scratch_programt &state_machine)
Expression to hold a symbol (variable)
Compute natural loops in a goto_function.
acceleration_utilst utils
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
std::unordered_map< exprt, exprt, irep_hash > expr_mapt