12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H 87 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H message_handlert & message_handler
goto_functionst & goto_functions
acceleration_utilst utils
std::list< exprt > distinguishers
Goto Programs with Functions.
std::set< goto_programt::targett > natural_loopt
distinguish_mapt distinguishing_points
void build_path(scratch_programt &scratch_program, patht &path)
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)
std::list< distinguish_valuest > accelerated_paths
natural_loops_mutablet::natural_loopt & loop
std::unordered_set< exprt, irep_hash > expr_sett
instructionst::iterator targett
void record_path(scratch_programt &scratch_program)
std::list< path_nodet > patht
A generic container class for the GOTO intermediate representation of one function.
symbol_tablet & symbol_table
std::map< exprt, bool > distinguish_valuest
Base class for all expressions.
void find_distinguishing_points()
goto_programt::targett loop_header
std::map< goto_programt::targett, exprt > distinguish_mapt
Compute natural loops in a goto_function.
goto_programt & goto_program