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
The symbol table.
Concrete Goto Program.
guard_expr_managert guard_managert
Definition guard.h:28
STL namespace.
Compute natural loops in a goto_function.
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.