cprover
polynomial_accelerator.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_POLYNOMIAL_ACCELERATOR_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
14 
15 #include <map>
16 #include <set>
17 
18 #include <util/symbol_table.h>
19 
22 
23 #include "scratch_program.h"
24 #include "polynomial.h"
25 #include "path.h"
26 #include "accelerator.h"
27 #include "path_acceleration.h"
28 #include "acceleration_utils.h"
29 #include "cone_of_influence.h"
30 #include "overflow_instrumenter.h"
31 
33 {
34 public:
36  const symbol_tablet &_symbol_table,
37  const goto_functionst &_goto_functions):
38  symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
40  goto_functions(_goto_functions),
42  {
44  }
45 
47  const symbol_tablet &_symbol_table,
48  const goto_functionst &_goto_functions,
49  exprt &_loop_counter):
50  symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
52  goto_functions(_goto_functions),
54  loop_counter(_loop_counter)
55  {
56  }
57 
58  virtual bool accelerate(patht &loop, path_acceleratort &accelerator);
59 
60  bool fit_polynomial(
62  exprt &target,
63  polynomialt &polynomial);
64 
65 protected:
67  goto_programt::instructionst &sliced_body,
68  exprt &target,
69  expr_sett &influence,
70  polynomialt &polynomial);
71 
72  void assert_for_values(
73  scratch_programt &program,
74  std::map<exprt, int> &values,
75  std::set<std::pair<expr_listt, exprt>> &coefficients,
76  int num_unwindings,
78  exprt &target,
79  overflow_instrumentert &overflow);
80  void extract_polynomial(
81  scratch_programt &program,
82  std::set<std::pair<expr_listt, exprt>> &coefficients,
83  polynomialt &polynomial);
84  void cone_of_influence(
86  exprt &target,
88  expr_sett &influence);
89 
90  bool fit_const(
92  exprt &target,
93  polynomialt &polynomial);
94 
95  bool check_inductive(
96  std::map<exprt, polynomialt> polynomials,
98  void stash_variables(
99  scratch_programt &program,
100  expr_sett modified,
101  substitutiont &substitution);
102  void stash_polynomials(
103  scratch_programt &program,
104  std::map<exprt, polynomialt> &polynomials,
105  std::map<exprt, exprt> &stashed,
107 
108  exprt precondition(patht &path);
109 
110  bool do_assumptions(
111  std::map<exprt, polynomialt> polynomials,
112  patht &body,
113  exprt &guard);
114 
115  typedef std::pair<exprt, exprt> expr_pairt;
116  typedef std::vector<expr_pairt> expr_pairst;
117 
119  {
124 
125  typedef std::vector<polynomial_array_assignmentt>
127 
128  bool do_arrays(
129  goto_programt::instructionst &loop_body,
130  std::map<exprt, polynomialt> &polynomials,
132  substitutiont &substitution,
133  scratch_programt &program);
135  goto_programt::instructionst &loop_body,
136  expr_sett &arrays_written);
138  expr_pairst &array_assignments,
139  std::map<exprt, polynomialt> &polynomials,
140  polynomial_array_assignmentst &array_polynomials,
141  polynomialst &nondet_indices);
142  bool expr2poly(
143  exprt &expr,
144  std::map<exprt, polynomialt> &polynomials,
145  polynomialt &poly);
146 
147  void ensure_no_overflows(goto_programt &program);
148 
150  const namespacet ns;
153 
155 
157 };
158 
160 
161 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
std::vector< expr_pairt > expr_pairst
void ensure_no_overflows(goto_programt &program)
Loop Acceleration.
polynomial_acceleratort(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
Goto Programs with Functions.
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
expr_sett find_modified(goto_programt::instructionst &body)
void assert_for_values(scratch_programt &program, std::map< exprt, int > &values, std::set< std::pair< expr_listt, exprt >> &coefficients, int num_unwindings, goto_programt::instructionst &loop_body, exprt &target, overflow_instrumentert &overflow)
Loop Acceleration.
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
const goto_functionst & goto_functions
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
std::unordered_set< exprt, irep_hash > expr_sett
The NIL expression.
Definition: std_expr.h:3764
virtual bool accelerate(patht &loop, path_acceleratort &accelerator)
Loop Acceleration.
std::list< path_nodet > patht
Definition: path.h:45
The symbol table.
Definition: symbol_table.h:52
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Loop Acceleration.
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
Symbol table.
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
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.
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
Loop Acceleration.
Base class for all expressions.
Definition: expr.h:46
std::pair< exprt, exprt > expr_pairt
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
polynomial_acceleratort(const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
Concrete Goto Program.
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)