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 "cone_of_influence.h"
31 #include "acceleration_utils.h"
32 
34 {
35 public:
38  symbol_tablet &_symbol_table,
39  goto_functionst &_goto_functions,
40  goto_programt &_goto_program,
42  goto_programt::targett _loop_header)
44  symbol_table(_symbol_table),
46  goto_functions(_goto_functions),
47  goto_program(_goto_program),
48  loop(_loop),
49  loop_header(_loop_header),
51  {
53  build_fixed();
54  }
55 
56  bool next(patht &path);
57 
58 protected:
61 
62  void build_path(scratch_programt &scratch_program, patht &path);
63  void build_fixed();
64 
65  void record_path(scratch_programt &scratch_program);
66 
73 
74  typedef std::map<goto_programt::targett, exprt> distinguish_mapt;
75  typedef std::map<exprt, bool> distinguish_valuest;
76 
80  std::list<exprt> distinguishers;
83  std::list<distinguish_valuest> accelerated_paths;
84 };
85 
86 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
sat_path_enumeratort::sat_path_enumeratort
sat_path_enumeratort(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)
Definition: sat_path_enumerator.h:36
path.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
acceleration_utilst
Definition: acceleration_utils.h:36
sat_path_enumeratort::distinguish_valuest
std::map< exprt, bool > distinguish_valuest
Definition: sat_path_enumerator.h:75
sat_path_enumeratort::find_distinguishing_points
void find_distinguishing_points()
Definition: sat_path_enumerator.cpp:109
path_enumerator.h
polynomial.h
sat_path_enumeratort::loop_header
goto_programt::targett loop_header
Definition: sat_path_enumerator.h:72
acceleration_utils.h
sat_path_enumeratort::distinguish_mapt
std::map< goto_programt::targett, exprt > distinguish_mapt
Definition: sat_path_enumerator.h:74
sat_path_enumeratort
Definition: sat_path_enumerator.h:33
exprt
Base class for all expressions.
Definition: expr.h:54
scratch_program.h
sat_path_enumeratort::next
bool next(patht &path)
Definition: sat_path_enumerator.cpp:48
sat_path_enumeratort::goto_functions
goto_functionst & goto_functions
Definition: sat_path_enumerator.h:69
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
path_enumeratort
Definition: path_enumerator.h:21
scratch_programt
Definition: scratch_program.h:36
sat_path_enumeratort::build_path
void build_path(scratch_programt &scratch_program, patht &path)
Definition: sat_path_enumerator.cpp:134
sat_path_enumeratort::distinguishers
std::list< exprt > distinguishers
Definition: sat_path_enumerator.h:80
expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: cone_of_influence.h:21
sat_path_enumeratort::accelerated_paths
std::list< distinguish_valuest > accelerated_paths
Definition: sat_path_enumerator.h:83
message_handlert
Definition: message.h:24
sat_path_enumeratort::fixed
goto_programt fixed
Definition: sat_path_enumerator.h:82
sat_path_enumeratort::loop
natural_loops_mutablet::natural_loopt & loop
Definition: sat_path_enumerator.h:71
goto_program.h
sat_path_enumeratort::message_handler
message_handlert & message_handler
Definition: sat_path_enumerator.h:59
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
sat_path_enumeratort::goto_program
goto_programt & goto_program
Definition: sat_path_enumerator.h:70
natural_loops.h
cone_of_influence.h
sat_path_enumeratort::record_path
void record_path(scratch_programt &scratch_program)
Definition: sat_path_enumerator.cpp:358
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
sat_path_enumeratort::modified
expr_sett modified
Definition: sat_path_enumerator.h:81
sat_path_enumeratort::build_fixed
void build_fixed()
Definition: sat_path_enumerator.cpp:213
sat_path_enumeratort::ns
namespacet ns
Definition: sat_path_enumerator.h:68
sat_path_enumeratort::distinguishing_points
distinguish_mapt distinguishing_points
Definition: sat_path_enumerator.h:79
sat_path_enumeratort::loop_counter
exprt loop_counter
Definition: sat_path_enumerator.h:78
symbol_table.h
Author: Diffblue Ltd.
sat_path_enumeratort::utils
acceleration_utilst utils
Definition: sat_path_enumerator.h:77
sat_path_enumeratort::symbol_table
symbol_tablet & symbol_table
Definition: sat_path_enumerator.h:67
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
natural_loops_templatet< goto_programt, goto_programt::targett >::natural_loopt
std::set< goto_programt::targett > natural_loopt
Definition: natural_loops.h:49