Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
79 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
symbol_tablet & symbol_table
natural_loops_mutablet::natural_loopt & loop
std::unique_ptr< path_enumeratort > path_enumerator
This is unused by this implementation of guards, but can be used by other implementations of the same...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
enumerating_loop_accelerationt(message_handlert &message_handler, symbol_tablet &_symbol_table, goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header, int _path_limit, guard_managert &guard_manager)
goto_programt & goto_program
goto_functionst & goto_functions
polynomial_acceleratort polynomial_accelerator
A loop, specified as a set of instructions.
A collection of goto functions.
goto_programt::targett loop_header
Compute natural loops in a goto_function.
A generic container class for the GOTO intermediate representation of one function.
bool accelerate(path_acceleratort &accelerator)
instructionst::iterator targett
guard_managert & guard_manager