cprover
Loading...
Searching...
No Matches
polynomial_accelerator.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: 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
19
20#include "polynomial.h"
21#include "path.h"
22#include "acceleration_utils.h"
23#include "cone_of_influence.h"
24
27
29{
30public:
45
48 const symbol_table_baset &_symbol_table,
49 const goto_functionst &_goto_functions,
50 exprt &_loop_counter,
53 symbol_table(const_cast<symbol_table_baset &>(_symbol_table)),
55 goto_functions(_goto_functions),
58 loop_counter(_loop_counter)
59 {
60 }
61
62 bool accelerate(patht &loop, path_acceleratort &accelerator);
63
64 bool fit_polynomial(
66 exprt &target,
67 polynomialt &polynomial);
68
69protected:
71
74 exprt &target,
75 expr_sett &influence,
76 polynomialt &polynomial);
77
79 scratch_programt &program,
80 std::map<exprt, int> &values,
81 std::set<std::pair<expr_listt, exprt>> &coefficients,
82 int num_unwindings,
84 exprt &target,
85 overflow_instrumentert &overflow);
87 scratch_programt &program,
88 std::set<std::pair<expr_listt, exprt>> &coefficients,
89 polynomialt &polynomial);
92 exprt &target,
94 expr_sett &influence);
95
96 bool fit_const(
98 exprt &target,
99 polynomialt &polynomial);
100
101 bool check_inductive(
102 std::map<exprt, polynomialt> polynomials,
105 scratch_programt &program,
106 std::map<exprt, polynomialt> &polynomials,
107 std::map<exprt, exprt> &stashed,
109
110 exprt precondition(patht &path);
111
113 std::map<exprt, polynomialt> polynomials,
114 patht &body,
115 exprt &guard);
116
117 typedef std::pair<exprt, exprt> expr_pairt;
118 typedef std::vector<expr_pairt> expr_pairst;
119
126
127 typedef std::vector<polynomial_array_assignmentt>
129
132 std::map<exprt, polynomialt> &polynomials,
133 substitutiont &substitution,
134 scratch_programt &program);
137 expr_sett &arrays_written);
139 expr_pairst &array_assignments,
140 std::map<exprt, polynomialt> &polynomials,
141 polynomial_array_assignmentst &array_polynomials,
142 polynomialst &nondet_indices);
144 exprt &expr,
145 std::map<exprt, polynomialt> &polynomials,
146 polynomialt &poly);
147
149
155
157
159};
160
162
163#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
Loop Acceleration.
static exprt guard(const exprt::operandst &guards, exprt cond)
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
std::list< instructiont > instructionst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
The NIL expression.
Definition std_expr.h:3086
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
std::vector< expr_pairt > expr_pairst
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)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
polynomial_acceleratort(message_handlert &message_handler, const symbol_table_baset &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter, guard_managert &guard_manager)
symbol_table_baset & symbol_table
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
std::pair< exprt, exprt > expr_pairt
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
bool accelerate(patht &loop, path_acceleratort &accelerator)
polynomial_acceleratort(message_handlert &message_handler, const symbol_table_baset &_symbol_table, const goto_functionst &_goto_functions, guard_managert &guard_manager)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
const goto_functionst & goto_functions
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, substitutiont &substitution, scratch_programt &program)
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
void ensure_no_overflows(goto_programt &program)
message_handlert & message_handler
The symbol table base class interface.
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.
guard_expr_managert guard_managert
Definition guard.h:28
Loop Acceleration.
std::list< path_nodet > patht
Definition path.h:44
Loop Acceleration.
std::vector< polynomialt > polynomialst
Definition polynomial.h:63
std::map< exprt, exprt > substitutiont
Definition polynomial.h:39
expr_sett find_modified(goto_programt::instructionst &body)