cprover
Loading...
Searching...
No Matches
disjunctive_polynomial_acceleration.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_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
21
23
24#include "path.h"
25#include "cone_of_influence.h"
26#include "acceleration_utils.h"
27
29
31{
32public:
35 symbol_tablet &_symbol_table,
36 goto_functionst &_goto_functions,
37 goto_programt &_goto_program,
39 goto_programt::targett _loop_header,
42 symbol_table(_symbol_table),
44 goto_functions(_goto_functions),
45 goto_program(_goto_program),
47 loop(_loop),
48 loop_header(_loop_header),
50 {
55 }
56
57 bool accelerate(path_acceleratort &accelerator);
58
59 bool fit_polynomial(
60 exprt &target,
61 polynomialt &polynomial,
62 patht &path);
63
64 bool find_path(patht &path);
65
66protected:
68
70 scratch_programt &program,
71 std::map<exprt, exprt> &values,
72 std::set<std::pair<expr_listt, exprt> > &coefficients,
73 int num_unwindings,
74 goto_programt &loop_body,
75 exprt &target);
76 void cone_of_influence(const exprt &target, expr_sett &cone);
77
79
80 void build_path(scratch_programt &scratch_program, patht &path);
81 void build_fixed();
82
83 void record_path(scratch_programt &scratch_program);
84
85 bool depends_on_array(const exprt &e, exprt &array);
86
94
95 typedef std::map<goto_programt::targett, exprt> distinguish_mapt;
96 typedef std::map<exprt, bool> distinguish_valuest;
97
101 std::list<symbol_exprt> distinguishers;
104 std::list<distinguish_valuest> accelerated_paths;
105};
106
107// NOLINTNEXTLINE(whitespace/line_length)
108#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H
Loop Acceleration.
void find_modified(const patht &path, expr_sett &modified)
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)
natural_loops_mutablet::natural_loopt & loop
void record_path(scratch_programt &scratch_program)
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
disjunctive_polynomial_accelerationt(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, guard_managert &guard_manager)
void cone_of_influence(const exprt &target, expr_sett &cone)
void build_path(scratch_programt &scratch_program, patht &path)
std::map< goto_programt::targett, exprt > distinguish_mapt
Base class for all expressions.
Definition expr.h:54
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
A loop, specified as a set of instructions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:2874
The symbol table.
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.
Compute natural loops in a goto_function.
Loop Acceleration.
std::list< path_nodet > patht
Definition path.h:44
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20
Author: Diffblue Ltd.