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 "loop_acceleration.h"
24 #include "polynomial_accelerator.h"
25 #include "path_enumerator.h"
26 #include "all_paths_enumerator.h"
27 #include "sat_path_enumerator.h"
28 
29 
31 {
32 public:
35  symbol_tablet &_symbol_table,
36  goto_functionst &_goto_functions,
37  goto_programt &_goto_program,
39  goto_programt::targett _loop_header,
40  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),
47  path_limit(_path_limit),
54  loop,
55  loop_header))
56  {
57  }
58 
59  virtual bool accelerate(path_acceleratort &accelerator);
60 
61 protected:
69 
70  std::unique_ptr<path_enumeratort> path_enumerator;
71 };
72 
73 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
std::unique_ptr< path_enumeratort > path_enumerator
natural_loops_mutablet::natural_loopt & loop
Loop Acceleration.
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)
Loop Acceleration.
instructionst::iterator targett
Definition: goto_program.h:397
Loop Acceleration.
The symbol table.
Definition: symbol_table.h:19
virtual bool accelerate(path_acceleratort &accelerator)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
Compute natural loops in a goto_function.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
Loop Acceleration.
Loop Acceleration.
Concrete Goto Program.