mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

include epsilon closure in initial state set, streamline final configuration computation #1224

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-28 13:47:19 -07:00
parent 0ebb917268
commit feac705cb8
1 changed files with 4 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/math/automata/symbolic_automata_def.h
View file

@ -298,21 +298,16 @@ symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_accepta
unsigned p_state_id = 0; // next state identifier unsigned p_state_id = 0; // next state identifier
TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";); TRACE("seq", tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);
// adds non-final states of a to final if flipping and and final otherwise // adds non-final states of a to final if flipping and final otherwise
unsigned_vector init_states; unsigned_vector init_states;
a.get_epsilon_closure(a.init(), init_states); a.get_epsilon_closure(a.init(), init_states);
bool found_final = false;
for (unsigned s : init_states) { for (unsigned s : init_states) {
if (a.is_final_state(s)) { set.insert(s);
found_final = true;
break;
}
} }
if (found_final != flip_acceptance) { if (a.is_final_configuration(set) != flip_acceptance) {
new_final_states.push_back(p_state_id); new_final_states.push_back(p_state_id);
} }
set.insert(a.init()); // Initial state as aset
s2id.insert(set, p_state_id++); // the index to the initial state is 0 s2id.insert(set, p_state_id++); // the index to the initial state is 0
id2s.push_back(set); id2s.push_back(set);