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
18
20
22#include "path_enumerator.h"
23#include "sat_path_enumerator.h"
24
25
27{
28public:
30 message_handlert &message_handler,
31 symbol_tablet &_symbol_table,
32 goto_functionst &_goto_functions,
33 goto_programt &_goto_program,
35 goto_programt::targett _loop_header,
36 int _path_limit,
38 : symbol_table(_symbol_table),
39 goto_functions(_goto_functions),
40 goto_program(_goto_program),
41 loop(_loop),
42 loop_header(_loop_header),
45 message_handler,
49 path_limit(_path_limit),
51 message_handler,
55 loop,
58 {
59 }
60
61 bool accelerate(path_acceleratort &accelerator);
62
63protected:
72
73 std::unique_ptr<path_enumeratort> path_enumerator;
74};
75
76#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.
STL namespace.
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