Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
86 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_SAT_PATH_ENUMERATOR_H
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::map< exprt, bool > distinguish_valuest
void find_distinguishing_points()
goto_programt::targett loop_header
std::map< goto_programt::targett, exprt > distinguish_mapt
Base class for all expressions.
goto_functionst & goto_functions
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void build_path(scratch_programt &scratch_program, patht &path)
std::list< exprt > distinguishers
std::unordered_set< exprt, irep_hash > expr_sett
std::list< distinguish_valuest > accelerated_paths
natural_loops_mutablet::natural_loopt & loop
message_handlert & message_handler
A collection of goto functions.
std::list< path_nodet > patht
goto_programt & goto_program
void record_path(scratch_programt &scratch_program)
A generic container class for the GOTO intermediate representation of one function.
distinguish_mapt distinguishing_points
acceleration_utilst utils
symbol_tablet & symbol_table
instructionst::iterator targett
std::set< goto_programt::targett > natural_loopt