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 
16 
17 #include <analyses/natural_loops.h>
18 
19 #include "loop_acceleration.h"
20 #include "polynomial_accelerator.h"
21 #include "path_enumerator.h"
22 #include "all_paths_enumerator.h"
23 #include "sat_path_enumerator.h"
24 
25 
27 {
28 public:
30  symbol_tablet &_symbol_table,
31  goto_functionst &_goto_functions,
32  goto_programt &_goto_program,
34  goto_programt::targett _loop_header,
35  int _path_limit):
36  symbol_table(_symbol_table),
37  goto_functions(_goto_functions),
38  goto_program(_goto_program),
39  loop(_loop),
40  loop_header(_loop_header),
42  path_limit(_path_limit)
43  {
44  // path_enumerator = new all_paths_enumeratort(goto_program, loop,
45  // loop_header);
48  }
49 
51  {
52  delete path_enumerator;
53  }
54 
55  virtual bool accelerate(path_acceleratort &accelerator);
56 
57 protected:
65 
67 };
68 
69 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
natural_loops_mutablet::natural_loopt & loop
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.
enumerating_loop_accelerationt(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)
The symbol table.
Definition: symbol_table.h:52
virtual bool accelerate(path_acceleratort &accelerator)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Compute natural loops in a goto_function.
Loop Acceleration.
Loop Acceleration.
Concrete Goto Program.