CBMC
Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
sat_path_enumeratort Class Reference

#include <sat_path_enumerator.h>

+ Inheritance diagram for sat_path_enumeratort:
+ Collaboration diagram for sat_path_enumeratort:

Public Member Functions

 sat_path_enumeratort (message_handlert &message_handler, symbol_table_baset &_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)
 
bool next (patht &path)
 
- Public Member Functions inherited from path_enumeratort
virtual ~path_enumeratort ()
 

Protected Types

typedef std::map< goto_programt::targett, exprt, goto_programt::target_less_than > distinguish_mapt
 
typedef std::map< exprt, bool > distinguish_valuest
 

Protected Member Functions

void find_distinguishing_points ()
 
void build_path (scratch_programt &scratch_program, patht &path)
 
void build_fixed ()
 
void record_path (scratch_programt &scratch_program)
 

Protected Attributes

message_handlert & message_handler
 
symbol_table_baset & symbol_table
 
namespacet ns
 
goto_functionst & goto_functions
 
goto_programt & goto_program
 
natural_loops_mutablet::natural_loopt & loop
 
goto_programt::targett loop_header
 
acceleration_utilst utils
 
guard_managert & guard_manager
 
exprt loop_counter
 
distinguish_mapt distinguishing_points
 
std::list< exprt > distinguishers
 
expr_sett modified
 
goto_programt fixed
 
std::list< distinguish_valuest > accelerated_paths
 

Detailed Description

Definition at line 26 of file sat_path_enumerator.h.

Member Typedef Documentation

◆ distinguish_mapt

typedef std:: map<goto_programt::targett, exprt, goto_programt::target_less_than> sat_path_enumeratort::distinguish_mapt
protected

Definition at line 71 of file sat_path_enumerator.h.

◆ distinguish_valuest

typedef std::map<exprt, bool> sat_path_enumeratort::distinguish_valuest
protected

Definition at line 72 of file sat_path_enumerator.h.

Constructor & Destructor Documentation

◆ sat_path_enumeratort()

sat_path_enumeratort::sat_path_enumeratort ( message_handlert &  message_handler,
symbol_table_baset &  _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 
)
inline

Definition at line 29 of file sat_path_enumerator.h.

Member Function Documentation

◆ build_fixed()

void sat_path_enumeratort::build_fixed ( )
protected

Definition at line 187 of file sat_path_enumerator.cpp.

◆ build_path()

void sat_path_enumeratort::build_path ( scratch_programt &  scratch_program,
patht &  path 
)
protected

Definition at line 109 of file sat_path_enumerator.cpp.

◆ find_distinguishing_points()

void sat_path_enumeratort::find_distinguishing_points ( )
protected

Definition at line 84 of file sat_path_enumerator.cpp.

◆ next()

bool sat_path_enumeratort::next ( patht &  path)
virtual

Implements path_enumeratort.

Definition at line 23 of file sat_path_enumerator.cpp.

◆ record_path()

void sat_path_enumeratort::record_path ( scratch_programt &  scratch_program)
protected

Definition at line 333 of file sat_path_enumerator.cpp.

Member Data Documentation

◆ accelerated_paths

std::list<distinguish_valuest> sat_path_enumeratort::accelerated_paths
protected

Definition at line 81 of file sat_path_enumerator.h.

◆ distinguishers

std::list<exprt> sat_path_enumeratort::distinguishers
protected

Definition at line 78 of file sat_path_enumerator.h.

◆ distinguishing_points

distinguish_mapt sat_path_enumeratort::distinguishing_points
protected

Definition at line 77 of file sat_path_enumerator.h.

◆ fixed

goto_programt sat_path_enumeratort::fixed
protected

Definition at line 80 of file sat_path_enumerator.h.

◆ goto_functions

goto_functionst& sat_path_enumeratort::goto_functions
protected

Definition at line 64 of file sat_path_enumerator.h.

◆ goto_program

goto_programt& sat_path_enumeratort::goto_program
protected

Definition at line 65 of file sat_path_enumerator.h.

◆ guard_manager

guard_managert& sat_path_enumeratort::guard_manager
protected

Definition at line 75 of file sat_path_enumerator.h.

◆ loop

natural_loops_mutablet::natural_loopt& sat_path_enumeratort::loop
protected

Definition at line 66 of file sat_path_enumerator.h.

◆ loop_counter

exprt sat_path_enumeratort::loop_counter
protected

Definition at line 76 of file sat_path_enumerator.h.

◆ loop_header

goto_programt::targett sat_path_enumeratort::loop_header
protected

Definition at line 67 of file sat_path_enumerator.h.

◆ message_handler

message_handlert& sat_path_enumeratort::message_handler
protected

Definition at line 54 of file sat_path_enumerator.h.

◆ modified

expr_sett sat_path_enumeratort::modified
protected

Definition at line 79 of file sat_path_enumerator.h.

◆ ns

namespacet sat_path_enumeratort::ns
protected

Definition at line 63 of file sat_path_enumerator.h.

◆ symbol_table

symbol_table_baset& sat_path_enumeratort::symbol_table
protected

Definition at line 62 of file sat_path_enumerator.h.

◆ utils

acceleration_utilst sat_path_enumeratort::utils
protected

Definition at line 74 of file sat_path_enumerator.h.

The documentation for this class was generated from the following files: