cprover
sat_path_enumerator.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_SAT_PATH_ENUMERATOR_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
14 
15 #include <map>
16 #include <set>
17 
18 #include <util/symbol_table.h>
19 
22 
23 #include <analyses/natural_loops.h>
24 
25 #include "path_enumerator.h"
26 #include "scratch_program.h"
27 #include "polynomial.h"
28 #include "path.h"
29 #include "accelerator.h"
30 #include "loop_acceleration.h"
31 #include "cone_of_influence.h"
32 #include "acceleration_utils.h"
33 
35 {
36 public:
38  symbol_tablet &_symbol_table,
39  goto_functionst &_goto_functions,
40  goto_programt &_goto_program,
42  goto_programt::targett _loop_header):
43  symbol_table(_symbol_table),
45  goto_functions(_goto_functions),
46  goto_program(_goto_program),
47  loop(_loop),
48  loop_header(_loop_header),
50  {
52  build_fixed();
53  }
54 
55  bool next(patht &path);
56 
57 protected:
59 
60  void build_path(scratch_programt &scratch_program, patht &path);
61  void build_fixed();
62 
63  void record_path(scratch_programt &scratch_program);
64 
71 
72  typedef std::map<goto_programt::targett, exprt> distinguish_mapt;
73  typedef std::map<exprt, bool> distinguish_valuest;
74 
78  std::list<exprt> distinguishers;
81  std::list<distinguish_valuest> accelerated_paths;
82 };
83 
84 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
goto_functionst & goto_functions
acceleration_utilst utils
std::list< exprt > distinguishers
Goto Programs with Functions.
std::set< T > natural_loopt
Definition: natural_loops.h:28
distinguish_mapt distinguishing_points
void build_path(scratch_programt &scratch_program, patht &path)
std::list< distinguish_valuest > accelerated_paths
Loop Acceleration.
natural_loops_mutablet::natural_loopt & loop
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
void record_path(scratch_programt &scratch_program)
std::list< path_nodet > patht
Definition: path.h:45
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
sat_path_enumeratort(symbol_tablet &_symbol_table, goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header)
Loop Acceleration.
Symbol table.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
symbol_tablet & symbol_table
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.
std::map< exprt, bool > distinguish_valuest
Base class for all expressions.
Definition: expr.h:46
goto_programt::targett loop_header
std::map< goto_programt::targett, exprt > distinguish_mapt
Compute natural loops in a goto_function.
Loop Acceleration.
Concrete Goto Program.
goto_programt & goto_program