From 88362a1c3adbc98832e6560bf3cfb49fec50fa0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 16:32:43 +0530 Subject: [PATCH] fix bugs in sequence extraction from NFA Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 879aa2144..fce29426c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -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(); }