From 2a7f2ab7f8fbd060c2a8dd7dfb9e3ca11504596f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Dec 2015 20:33:55 -0800 Subject: [PATCH] sequence automaton Signed-off-by: Nikolaj Bjorner --- src/math/automata/automaton.h | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/src/math/automata/automaton.h b/src/math/automata/automaton.h index e28db8fa0..7a224b5d4 100644 --- a/src/math/automata/automaton.h +++ b/src/math/automata/automaton.h @@ -94,9 +94,25 @@ public: } } + // create an automaton that accepts a sequence. + automaton(ptr_vector const& seq): + m_init(0), + m_is_epsilon_free(true), + m_is_deterministic(true) { + m_delta.resize(seq.size()+1, moves()); + m_delta_inv.resize(seq.size()+1, moves()); + for (unsigned i = 0; i < seq.size(); ++i) { + m_delta[i].push_back(move(i, i + 1, seq[i])); + m_delta[i + 1].push_back(move(i, i + 1, seq[i])); + } + m_final_states.push_back(seq.size()); + m_final_set.insert(seq.size()); + } + // The automaton with a single state that is also final. - automaton(T* t, unsigned s = 0): - m_init(s) { + automaton(T* t): + m_init(0) { + unsigned s = 0; m_delta.resize(s+1, moves()); m_delta_inv.resize(s+1, moves()); m_final_set.insert(s);