cprover
Loading...
Searching...
No Matches
sat_path_enumerator.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_SAT_PATH_ENUMERATOR_H
13#define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
14
15#include <map>
16
17#include <util/symbol_table.h>
18
20
22
23#include "path_enumerator.h"
24#include "path.h"
25#include "cone_of_influence.h"
26#include "acceleration_utils.h"
27
29{
30public:
52
53 bool next(patht &path);
54
55protected:
58
60 void build_fixed();
61
63
70
71 typedef std::map<goto_programt::targett, exprt> distinguish_mapt;
72 typedef std::map<exprt, bool> distinguish_valuest;
73
78 std::list<exprt> distinguishers;
81 std::list<distinguish_valuest> accelerated_paths;
82};
83
84#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
Loop Acceleration.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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 namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
guard_managert & guard_manager
acceleration_utilst utils
distinguish_mapt distinguishing_points
message_handlert & message_handler
goto_programt::targett loop_header
void build_path(scratch_programt &scratch_program, patht &path)
goto_functionst & goto_functions
std::list< distinguish_valuest > accelerated_paths
goto_programt & goto_program
void record_path(scratch_programt &scratch_program)
std::map< exprt, bool > distinguish_valuest
std::map< goto_programt::targett, exprt > distinguish_mapt
natural_loops_mutablet::natural_loopt & loop
std::list< exprt > distinguishers
sat_path_enumeratort(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)
symbol_tablet & symbol_table
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
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
Author: Diffblue Ltd.