CBMC
Public Member Functions | Protected Attributes | List of all members
enumerating_loop_accelerationt Class Reference

#include <enumerating_loop_acceleration.h>

+ Collaboration diagram for enumerating_loop_accelerationt:

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, guard_managert &guard_manager)
 
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
 
guard_managert & guard_manager
 
polynomial_acceleratort polynomial_accelerator
 
int path_limit
 
std::unique_ptr< path_enumeratort > path_enumerator
 

Detailed Description

Definition at line 26 of file enumerating_loop_acceleration.h.

Constructor & Destructor Documentation

◆ enumerating_loop_accelerationt()

enumerating_loop_accelerationt::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 
)
inline

Definition at line 29 of file enumerating_loop_acceleration.h.

Member Function Documentation

◆ accelerate()

bool enumerating_loop_accelerationt::accelerate ( path_acceleratort &  accelerator)

Definition at line 16 of file enumerating_loop_acceleration.cpp.

Member Data Documentation

◆ goto_functions

goto_functionst& enumerating_loop_accelerationt::goto_functions
protected

Definition at line 65 of file enumerating_loop_acceleration.h.

◆ goto_program

goto_programt& enumerating_loop_accelerationt::goto_program
protected

Definition at line 66 of file enumerating_loop_acceleration.h.

◆ guard_manager

guard_managert& enumerating_loop_accelerationt::guard_manager
protected

Definition at line 69 of file enumerating_loop_acceleration.h.

◆ loop

natural_loops_mutablet::natural_loopt& enumerating_loop_accelerationt::loop
protected

Definition at line 67 of file enumerating_loop_acceleration.h.

◆ loop_header

goto_programt::targett enumerating_loop_accelerationt::loop_header
protected

Definition at line 68 of file enumerating_loop_acceleration.h.

◆ path_enumerator

std::unique_ptr<path_enumeratort> enumerating_loop_accelerationt::path_enumerator
protected

Definition at line 73 of file enumerating_loop_acceleration.h.

◆ path_limit

int enumerating_loop_accelerationt::path_limit
protected

Definition at line 71 of file enumerating_loop_acceleration.h.

◆ polynomial_accelerator

polynomial_acceleratort enumerating_loop_accelerationt::polynomial_accelerator
protected

Definition at line 70 of file enumerating_loop_acceleration.h.

◆ symbol_table

symbol_tablet& enumerating_loop_accelerationt::symbol_table
protected

Definition at line 64 of file enumerating_loop_acceleration.h.

The documentation for this class was generated from the following files: