cprover
|
#include <sat_path_enumerator.h>
Public Member Functions | |
sat_path_enumeratort (symbol_tablet &_symbol_table, goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header) | |
bool | next (patht &path) |
![]() | |
virtual | ~path_enumeratort () |
Protected Types | |
typedef std::map< goto_programt::targett, exprt > | 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) |
Definition at line 34 of file sat_path_enumerator.h.
|
protected |
Definition at line 72 of file sat_path_enumerator.h.
|
protected |
Definition at line 73 of file sat_path_enumerator.h.
|
inline |
Definition at line 37 of file sat_path_enumerator.h.
References build_fixed(), and find_distinguishing_points().
|
protected |
Definition at line 214 of file sat_path_enumerator.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSUME, goto_program_templatet< codeT, guardT >::copy_from(), distinguishers, distinguishing_points, fixed, Forall_goto_program_instructions, acceleration_utilst::fresh_symbol(), goto_program, goto_program_templatet< codeT, guardT >::insert_after(), goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::instructions, loop, loop_header, remove_skip(), SKIP, symbolt::symbol_expr(), symbol_table, goto_program_templatet< codeT, guardT >::update(), and utils.
Referenced by sat_path_enumeratort().
|
protected |
Definition at line 135 of file sat_path_enumerator.cpp.
References distinguishing_points, scratch_programt::eval(), goto_program_templatet< codeT, guardT >::get_successors(), goto_program, exprt::is_true(), loop, loop_header, and next().
Referenced by next().
|
protected |
Definition at line 110 of file sat_path_enumerator.cpp.
References distinguishers, distinguishing_points, acceleration_utilst::fresh_symbol(), goto_program_templatet< codeT, guardT >::get_successors(), goto_program, loop, symbolt::symbol_expr(), and utils.
Referenced by sat_path_enumeratort().
|
virtual |
Implements path_enumeratort.
Definition at line 49 of file sat_path_enumerator.cpp.
References accelerated_paths, goto_program_templatet< codeT, guardT >::add_instruction(), scratch_programt::append(), ASSERT, scratch_programt::assume(), build_path(), scratch_programt::check_sat(), fixed, record_path(), irept::swap(), and symbol_table.
Referenced by build_path().
|
protected |
Definition at line 359 of file sat_path_enumerator.cpp.
References accelerated_paths, distinguishers, scratch_programt::eval(), and exprt::is_true().
Referenced by next().
|
protected |
Definition at line 81 of file sat_path_enumerator.h.
Referenced by next(), and record_path().
|
protected |
Definition at line 78 of file sat_path_enumerator.h.
Referenced by build_fixed(), find_distinguishing_points(), and record_path().
|
protected |
Definition at line 77 of file sat_path_enumerator.h.
Referenced by build_fixed(), build_path(), and find_distinguishing_points().
|
protected |
Definition at line 80 of file sat_path_enumerator.h.
Referenced by build_fixed(), and next().
|
protected |
Definition at line 67 of file sat_path_enumerator.h.
|
protected |
Definition at line 68 of file sat_path_enumerator.h.
Referenced by build_fixed(), build_path(), and find_distinguishing_points().
|
protected |
Definition at line 69 of file sat_path_enumerator.h.
Referenced by build_fixed(), build_path(), and find_distinguishing_points().
|
protected |
Definition at line 76 of file sat_path_enumerator.h.
|
protected |
Definition at line 70 of file sat_path_enumerator.h.
Referenced by build_fixed(), and build_path().
|
protected |
Definition at line 79 of file sat_path_enumerator.h.
|
protected |
Definition at line 66 of file sat_path_enumerator.h.
|
protected |
Definition at line 65 of file sat_path_enumerator.h.
Referenced by build_fixed(), and next().
|
protected |
Definition at line 75 of file sat_path_enumerator.h.
Referenced by build_fixed(), and find_distinguishing_points().