mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix bugs in sequence extraction from NFA

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-15 16:32:43 +05:30
parent 14c19fe928
commit 88362a1c3a
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/seq_rewriter.cpp
View file

@ -731,8 +731,14 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
unsigned state = aut.init();
uint_set visited;
eautomaton::moves mvs;
aut.get_moves_from(state, mvs, true);
while (!aut.is_final_state(state)) {
unsigned_vector states;
aut.get_epsilon_closure(state, states);
bool has_final = false;
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
has_final = aut.is_final_state(states[i]);
}
aut.get_moves_from(state, mvs, true);
while (!has_final) {
if (mvs.size() != 1) {
return false;
}
@ -751,6 +757,12 @@ bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
state = mvs[0].dst();
mvs.reset();
aut.get_moves_from(state, mvs, true);
states.reset();
has_final = false;
aut.get_epsilon_closure(state, states);
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
has_final = aut.is_final_state(states[i]);
}
}
return mvs.empty();
}