cprover
enumerating_loop_acceleration.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
14 
15 #include <memory>
16 
17 #include <util/make_unique.h>
18 
20 
21 #include <analyses/natural_loops.h>
22 
23 #include "polynomial_accelerator.h"
24 #include "path_enumerator.h"
25 #include "all_paths_enumerator.h"
26 #include "sat_path_enumerator.h"
27 
28 
30 {
31 public:
33  message_handlert &message_handler,
34  symbol_tablet &_symbol_table,
35  goto_functionst &_goto_functions,
36  goto_programt &_goto_program,
38  goto_programt::targett _loop_header,
39  int _path_limit,
41  : symbol_table(_symbol_table),
42  goto_functions(_goto_functions),
43  goto_program(_goto_program),
44  loop(_loop),
45  loop_header(_loop_header),
48  message_handler,
52  path_limit(_path_limit),
54  message_handler,
58  loop,
61  {
62  }
63 
64  bool accelerate(path_acceleratort &accelerator);
65 
66 protected:
75 
76  std::unique_ptr<path_enumeratort> path_enumerator;
77 };
78 
79 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
enumerating_loop_accelerationt::symbol_table
symbol_tablet & symbol_table
Definition: enumerating_loop_acceleration.h:67
path_enumerator.h
Loop Acceleration.
sat_path_enumeratort
Definition: sat_path_enumerator.h:34
enumerating_loop_accelerationt::loop
natural_loops_mutablet::natural_loopt & loop
Definition: enumerating_loop_acceleration.h:70
enumerating_loop_accelerationt::path_enumerator
std::unique_ptr< path_enumeratort > path_enumerator
Definition: enumerating_loop_acceleration.h:76
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
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)
Definition: enumerating_loop_acceleration.h:32
make_unique.h
enumerating_loop_accelerationt::goto_program
goto_programt & goto_program
Definition: enumerating_loop_acceleration.h:69
enumerating_loop_accelerationt::goto_functions
goto_functionst & goto_functions
Definition: enumerating_loop_acceleration.h:68
enumerating_loop_accelerationt::polynomial_accelerator
polynomial_acceleratort polynomial_accelerator
Definition: enumerating_loop_acceleration.h:73
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
path_acceleratort
Definition: accelerator.h:27
message_handlert
Definition: message.h:28
goto_program.h
Concrete Goto Program.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
sat_path_enumerator.h
Loop Acceleration.
enumerating_loop_accelerationt::path_limit
int path_limit
Definition: enumerating_loop_acceleration.h:74
enumerating_loop_accelerationt::loop_header
goto_programt::targett loop_header
Definition: enumerating_loop_acceleration.h:71
natural_loops.h
Compute natural loops in a goto_function.
polynomial_acceleratort
Definition: polynomial_accelerator.h:32
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
all_paths_enumerator.h
Loop Acceleration.
enumerating_loop_accelerationt::accelerate
bool accelerate(path_acceleratort &accelerator)
Definition: enumerating_loop_acceleration.cpp:16
polynomial_accelerator.h
Loop Acceleration.
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
enumerating_loop_accelerationt::guard_manager
guard_managert & guard_manager
Definition: enumerating_loop_acceleration.h:72
enumerating_loop_accelerationt
Definition: enumerating_loop_acceleration.h:30