cprover
Loading...
Searching...
No Matches
enumerating_loop_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_ENUMERATING_LOOP_ACCELERATION_H
13#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
14
15#include <memory>
16
17#include <util/make_unique.h>
18
20
22
24#include "path_enumerator.h"
25#include "sat_path_enumerator.h"
26
27
29{
30public:
32 message_handlert &message_handler,
33 symbol_tablet &_symbol_table,
34 goto_functionst &_goto_functions,
35 goto_programt &_goto_program,
37 goto_programt::targett _loop_header,
38 int _path_limit,
40 : symbol_table(_symbol_table),
41 goto_functions(_goto_functions),
42 goto_program(_goto_program),
43 loop(_loop),
44 loop_header(_loop_header),
47 message_handler,
51 path_limit(_path_limit),
53 message_handler,
57 loop,
60 {
61 }
62
63 bool accelerate(path_acceleratort &accelerator);
64
65protected:
74
75 std::unique_ptr<path_enumeratort> path_enumerator;
76};
77
78#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
enumerating_loop_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, int _path_limit, guard_managert &guard_manager)
std::unique_ptr< path_enumeratort > path_enumerator
bool accelerate(path_acceleratort &accelerator)
natural_loops_mutablet::natural_loopt & loop
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.
The symbol table.
Concrete Goto Program.
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition make_unique.h:19
Compute natural loops in a goto_function.
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20