cprover
|
#include <enumerating_loop_acceleration.h>
Public Member Functions | |
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) | |
virtual bool | accelerate (path_acceleratort &accelerator) |
Protected Attributes | |
symbol_tablet & | symbol_table |
goto_functionst & | goto_functions |
goto_programt & | goto_program |
natural_loops_mutablet::natural_loopt & | loop |
goto_programt::targett | loop_header |
polynomial_acceleratort | polynomial_accelerator |
int | path_limit |
std::unique_ptr< path_enumeratort > | path_enumerator |
Definition at line 30 of file enumerating_loop_acceleration.h.
|
inline |
Definition at line 33 of file enumerating_loop_acceleration.h.
|
virtual |
Implements loop_accelerationt.
Definition at line 16 of file enumerating_loop_acceleration.cpp.
References polynomial_acceleratort::accelerate(), goto_program, goto_programt::output_instruction(), path_acceleratort::path, path_enumerator, path_limit, polynomial_accelerator, and symbol_table.
|
protected |
Definition at line 63 of file enumerating_loop_acceleration.h.
|
protected |
Definition at line 64 of file enumerating_loop_acceleration.h.
Referenced by accelerate().
|
protected |
Definition at line 65 of file enumerating_loop_acceleration.h.
|
protected |
Definition at line 66 of file enumerating_loop_acceleration.h.
|
protected |
Definition at line 70 of file enumerating_loop_acceleration.h.
Referenced by accelerate().
|
protected |
Definition at line 68 of file enumerating_loop_acceleration.h.
Referenced by accelerate().
|
protected |
Definition at line 67 of file enumerating_loop_acceleration.h.
Referenced by accelerate().
|
protected |
Definition at line 62 of file enumerating_loop_acceleration.h.
Referenced by accelerate().