cprover
disjunctive_polynomial_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_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_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 "scratch_program.h"
26 #include "polynomial.h"
27 #include "path.h"
28 #include "accelerator.h"
29 #include "loop_acceleration.h"
30 #include "cone_of_influence.h"
31 #include "acceleration_utils.h"
32 
34 {
35 public:
37  symbol_tablet &_symbol_table,
38  goto_functionst &_goto_functions,
39  goto_programt &_goto_program,
41  goto_programt::targett _loop_header):
42  symbol_table(_symbol_table),
44  goto_functions(_goto_functions),
45  goto_program(_goto_program),
46  loop(_loop),
47  loop_header(_loop_header),
49  {
52  build_fixed();
54  }
55 
56  virtual bool accelerate(path_acceleratort &accelerator);
57 
58  bool fit_polynomial(
59  exprt &target,
60  polynomialt &polynomial,
61  patht &path);
62 
63  bool find_path(patht &path);
64 
65 protected:
66  void assert_for_values(
67  scratch_programt &program,
68  std::map<exprt, exprt> &values,
69  std::set<std::pair<expr_listt, exprt> > &coefficients,
70  int num_unwindings,
71  goto_programt &loop_body,
72  exprt &target);
73  void cone_of_influence(const exprt &target, expr_sett &cone);
74 
76 
77  void build_path(scratch_programt &scratch_program, patht &path);
78  void build_fixed();
79 
80  void record_path(scratch_programt &scratch_program);
81 
82  bool depends_on_array(const exprt &e, exprt &array);
83 
90 
91  typedef std::map<goto_programt::targett, exprt> distinguish_mapt;
92  typedef std::map<exprt, bool> distinguish_valuest;
93 
97  std::list<exprt> distinguishers;
100  std::list<distinguish_valuest> accelerated_paths;
101 };
102 
103 // NOLINTNEXTLINE(whitespace/line_length)
104 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H
void build_path(scratch_programt &scratch_program, patht &path)
Goto Programs with Functions.
void record_path(scratch_programt &scratch_program)
void assert_for_values(scratch_programt &program, std::map< exprt, exprt > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt &loop_body, exprt &target)
Loop Acceleration.
disjunctive_polynomial_accelerationt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header)
virtual bool accelerate(path_acceleratort &accelerator)
std::unordered_set< exprt, irep_hash > expr_sett
The NIL expression.
Definition: std_expr.h:3764
std::list< path_nodet > patht
Definition: path.h:45
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void find_modified(const patht &path, expr_sett &modified)
Loop Acceleration.
Symbol table.
std::map< goto_programt::targett, exprt > distinguish_mapt
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.
Base class for all expressions.
Definition: expr.h:46
natural_loops_mutablet::natural_loopt & loop
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
void cone_of_influence(const exprt &target, expr_sett &cone)
Compute natural loops in a goto_function.
Loop Acceleration.
Concrete Goto Program.