12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H 13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H 57 void output(std::ostream &str)
const;
77 typedef std::multimap<goto_programt::targett, statet>
transitionst;
78 typedef std::pair<transitionst::iterator, transitionst::iterator>
116 typedef std::multimap<goto_programt::targett, state_pairt>
sym_mapt;
161 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_TRACE_AUTOMATON_H
void get_transitions(sym_mapt &transitions)
void epsilon_closure(state_sett &s)
std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
std::multimap< goto_programt::targett, statet > transitionst
bool in_alphabet(goto_programt::targett t)
void output(std::ostream &str) const
std::vector< transitionst > transition_tablet
statet find_dstate(state_sett &s)
void swap(automatont &that)
void accept_states(state_sett &states)
std::pair< statet, statet > state_pairt
void pop_unmarked_dstate(state_sett &s)
statet add_dstate(state_sett &s)
void add_trans(statet s, goto_programt::targett a, statet t)
void add_dtrans(state_sett &s, goto_programt::targett a, state_sett &t)
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
instructionst::iterator targett
bool is_accepting(statet s)
instructionst instructions
The list of instructions in the goto program.
std::list< path_nodet > patht
std::size_t count_transitions()
void build_alphabet(goto_programt &program)
void add_path(patht &path)
std::set< statet > state_sett
static const statet no_state
goto_programt & goto_program
A generic container class for the GOTO intermediate representation of one function.
std::vector< state_sett > unmarked_dstates
std::multimap< goto_programt::targett, state_pairt > sym_mapt
std::set< goto_programt::targett > alphabett
std::map< state_sett, statet > state_mapt
trace_automatont(goto_programt &_goto_program)
void reverse(goto_programt::targett epsilon)
void move(statet s, goto_programt::targett a, state_sett &t)
transition_tablet transitions
goto_programt::targett epsilon
void set_accepting(statet s)