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
77
78#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ENUMERATING_LOOP_ACCELERATION_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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.
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