Skip to content

Commit

Permalink
Merge pull request #398 from VeriFIT/refactor_string_solving_operations
Browse files Browse the repository at this point in the history 
Refactor string solving operations
  • Loading branch information
@koniksedy @Adda0
koniksedy authored and Adda0 committed Dec 2, 2024
2 parents b9e780b + e5a81da commit 880d99b
Show file tree
Hide file tree
Showing 8 changed files with 108 additions and 106 deletions.
2 changes: 1 addition & 1 deletion include/mata/nfa/algorithms.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -129,7 +129,7 @@ Nfa product(const Nfa& lhs, const Nfa& rhs, const std::function<bool(State,State
* Supports epsilon symbols when @p use_epsilon is set to true.
* @param[in] lhs First automaton to concatenate.
* @param[in] rhs Second automaton to concatenate.
* @param[in] epsilon Epsilon to be used co concatenation (provided @p use_epsilon is true)
* @param[in] epsilon Epsilon to be used for concatenation (provided @p use_epsilon is true)
* @param[in] use_epsilon Whether to concatenate over epsilon symbol.
* @param[out] lhs_state_renaming Map mapping lhs states to result states.
* @param[out] rhs_state_renaming Map mapping rhs states to result states.
Expand Down
4 changes: 1 addition & 3 deletions include/mata/nfa/delta.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,9 +118,7 @@ public:
using super::empty, super::size;
using super::to_vector;
// dangerous, breaks the sortedness invariant
using super::emplace_back;
// dangerous, breaks the sortedness invariant
using super::push_back;
using super::push_back, super::emplace_back;
// is adding non-const version as well ok?
using super::front;
using super::back;
Expand Down
2 changes: 1 addition & 1 deletion include/mata/nft/algorithms.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ Nft product(const Nft& lhs, const Nft& rhs, const std::function<bool(State,State
* Supports epsilon symbols when @p use_epsilon is set to true.
* @param[in] lhs First automaton to concatenate.
* @param[in] rhs Second automaton to concatenate.
* @param[in] epsilon Epsilon to be used co concatenation (provided @p use_epsilon is true)
* @param[in] epsilon Epsilon to be used for concatenation (provided @p use_epsilon is true)
* @param[in] use_epsilon Whether to concatenate over epsilon symbol.
* @param[out] lhs_state_renaming Map mapping lhs states to result states.
* @param[out] rhs_state_renaming Map mapping rhs states to result states.
Expand Down
4 changes: 2 additions & 2 deletions include/mata/nft/strings.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,9 +21,9 @@ enum class ReplaceMode {
};

/**
* Create identity transducer over the @p alphabet with @p level_cnt levels.
* Create identity transducer over the @p alphabet with @p num_of_levels levels.
*/
Nft create_identity(mata::Alphabet* alphabet, Level level_cnt = 2);
Nft create_identity(mata::Alphabet* alphabet, size_t num_of_levels = 2);

/**
* Create identity input/output transducer with 2 levels over the @p alphabet with @p level_cnt levels with single
Expand Down
63 changes: 36 additions & 27 deletions src/nft/nft.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -311,13 +311,14 @@ State Nft::insert_word(const State source, const Word &word, const State target)
const size_t num_of_states_orig{ num_of_states() };
assert(source < num_of_states_orig);
assert(target < num_of_states_orig);
assert(levels[source] == levels[target]);

const State first_new_state = num_of_states_orig;
const State word_tgt = Nfa::insert_word(source, word, target);
const size_t num_of_states_after = num_of_states();
const Level src_lvl = levels[source];

Level lvl = (num_of_levels == 1 ) ? src_lvl : (src_lvl + 1);
Level lvl = (num_of_levels == 1 ) ? src_lvl : (src_lvl + 1) % static_cast<Level>(num_of_levels);
State state{ first_new_state };
for (; state < num_of_states_after; state++, lvl = (lvl + 1) % static_cast<Level>(num_of_levels)){
add_state_with_level(state, lvl);
Expand All @@ -328,31 +329,29 @@ State Nft::insert_word(const State source, const Word &word, const State target)
return word_tgt;
}

State Nft::insert_word(const State source, const Word &word) { return insert_word(source, word, add_state()); }
State Nft::insert_word(const State source, const Word& word) {
assert(source < levels.size());
return insert_word(source, word, add_state_with_level(levels[source]));
}

State Nft::insert_word_by_parts(const State source, const std::vector<Word> &word_parts_on_levels, const State target) {
assert(0 < num_of_levels);
assert(word_parts_on_levels.size() == num_of_levels);
assert(source < num_of_states());
assert(target < num_of_states());
assert(levels[source] == 0);
assert(levels[target] == 0);
assert(source < levels.size());
assert(target < levels.size());
assert(levels[source] == levels[target]);
const Level from_to_level{ levels[source] };

if (num_of_levels == 1) {
return Nft::insert_word(source, word_parts_on_levels[0], target);
}

size_t max_word_part_len = std::max_element(
word_parts_on_levels.begin(),
word_parts_on_levels.end(),
[](const Word& a, const Word& b) { return a.size() < b.size(); }
)->size();
assert(0 < max_word_part_len);
size_t word_total_len = num_of_levels * max_word_part_len;

std::vector<mata::Word::const_iterator> word_part_it_v(num_of_levels);
for (Level lvl{ 0 }; lvl < num_of_levels; lvl++) {
for (Level lvl{ from_to_level }, i{ 0 }; i < static_cast<Level>(num_of_levels); ++i) {
word_part_it_v[lvl] = word_parts_on_levels[lvl].begin();
lvl = (lvl + 1) % static_cast<Level>(num_of_levels);
}

// This function retrieves the next symbol from a word part at a specified level and advances the corresponding iterator.
Expand All @@ -365,28 +364,36 @@ State Nft::insert_word_by_parts(const State source, const std::vector<Word> &wor
};

// Add transition source --> inner_state.
Level inner_lvl = (num_of_levels == 1 ) ? 0 : 1;
Level inner_lvl = (num_of_levels == 1 ) ? 0 : (from_to_level + 1) % static_cast<Level>(num_of_levels);
State inner_state = add_state_with_level(inner_lvl);
delta.add(source, get_next_symbol(0), inner_state);
delta.add(source, get_next_symbol(from_to_level), inner_state);

// Add transition inner_state --> inner_state
State prev_state = inner_state;
Level prev_lvl = inner_lvl;
for (size_t symbol_idx{ 1 }; symbol_idx < word_total_len - 1; symbol_idx++) {
inner_lvl = (prev_lvl + 1) % static_cast<Level>(num_of_levels);
inner_state = add_state_with_level(inner_lvl);
delta.add(prev_state, get_next_symbol(prev_lvl), inner_state);
prev_state = inner_state;
prev_lvl = inner_lvl;
const size_t max_word_part_len = std::max_element(
word_parts_on_levels.begin(),
word_parts_on_levels.end(),
[](const Word& a, const Word& b) { return a.size() < b.size(); }
)->size();
const size_t word_total_len = num_of_levels * max_word_part_len;
if (word_total_len != 0) {
for (size_t symbol_idx{ 1 }; symbol_idx < word_total_len - 1; symbol_idx++) {
inner_lvl = (prev_lvl + 1) % static_cast<Level>(num_of_levels);
inner_state = add_state_with_level(inner_lvl);
delta.add(prev_state, get_next_symbol(prev_lvl), inner_state);
prev_state = inner_state;
prev_lvl = inner_lvl;
}
}

// Add transition inner_state --> target.
delta.add(prev_state, get_next_symbol(prev_lvl), target);
return target;
}

State Nft::insert_word_by_parts(const State source, const std::vector<Word> &word_parts_on_levels) {
return insert_word_by_parts(source, word_parts_on_levels, add_state());
assert(source < levels.size());
return insert_word_by_parts(source, word_parts_on_levels, add_state_with_level(levels[source]));
}

void Nft::insert_identity(const State state, const std::vector<Symbol> &symbols, const JumpMode jump_mode) {
Expand All @@ -397,11 +404,13 @@ void Nft::insert_identity(const State state, const std::vector<Symbol> &symbols,

void Nft::insert_identity(const State state, const Symbol symbol, const JumpMode jump_mode) {
// TODO(nft): Evaluate the performance difference between adding a jump transition and inserting a transition for each level.
if (jump_mode == JumpMode::RepeatSymbol) {
delta.add(state, symbol, state);
} else {
// FIXME(nft): Allow symbol jump transitions?
// if (jump_mode == JumpMode::RepeatSymbol) {
// delta.add(state, symbol, state);
// insert_word(state, Word(num_of_levels, symbol), state);
// } else {
insert_word(state, Word(num_of_levels, symbol), state);
}
// }
}

void Nft::clear() {
Expand Down
83 changes: 17 additions & 66 deletions src/nft/strings.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,11 +65,7 @@ namespace {
case ReplaceMode::Single: {
State state_lvl0{ nft.add_state_with_level(0) };
nft.delta.add(state_lvl1, replacement, state_lvl0);
for (const Symbol symbol: alphabet_symbols) {
state_lvl1 = nft.add_state_with_level(1);
nft.delta.add(state_lvl0, symbol, state_lvl1);
nft.delta.add(state_lvl1, symbol, state_lvl0);
}
nft.insert_identity(state_lvl0, alphabet_symbols.to_vector());
state_lvl1 = nft.add_state_with_level(1);
nft.delta.add(state_lvl0, end_marker, state_lvl1);
nft.delta.add(state_lvl1, EPSILON, *nft.final.begin());
Expand Down Expand Up @@ -185,37 +181,13 @@ namespace {
}
}

Nft mata::nft::strings::create_identity(mata::Alphabet* alphabet, Level level_cnt) {
if (level_cnt == 0) { throw std::runtime_error("NFT must have at least one level"); }
Nft mata::nft::strings::create_identity(mata::Alphabet* alphabet, const size_t num_of_levels) {
if (num_of_levels == 0) { throw std::runtime_error("NFT must have at least one level"); }
const auto alphabet_symbols{ alphabet->get_alphabet_symbols() };
const size_t additional_states_per_symbol_num{ level_cnt - 1 };
const size_t additional_states_per_symbol_num{ num_of_levels - 1 };
const size_t num_of_states{ alphabet_symbols.size() * additional_states_per_symbol_num + 1 };
Levels levels(num_of_states);
levels[0] = 0;
Level level{ 1 };
for (State state{ 1 }; state < num_of_states; ++state) {
levels[state] = level;
const Level new_level{ level + 1 };
level = new_level < level_cnt ? new_level : 1;
}
Nft nft{ num_of_states, { 0 }, { 0 }, std::move(levels), level_cnt, alphabet };
State state{ 0 };
State new_state;

for (const Symbol symbol: alphabet_symbols) {
level = 0;
new_state = 0;
for (; level < additional_states_per_symbol_num; ++level) {
new_state = state + 1;
if (level == 0) {
nft.delta.add(0, symbol, new_state);
} else {
nft.delta.add(state, symbol, new_state);
}
++state;
}
nft.delta.add(new_state, symbol, 0);
}
Nft nft{ num_of_states, { 0 }, { 0 }, {}, num_of_levels, alphabet };
nft.insert_identity(0, alphabet_symbols.to_vector());
return nft;
}

Expand Down Expand Up @@ -253,11 +225,7 @@ Nft nft::strings::create_identity_with_single_symbol_replace(Alphabet* alphabet,
nft.delta.add(state_lvl1,
replacement_it == replacement_end ? EPSILON : *replacement_it,
after_replace_state);
for (const Symbol symbol: alphabet->get_alphabet_symbols()) {
state_lvl1 = nft.add_state_with_level(1);
nft.delta.add(after_replace_state, symbol, state_lvl1);
nft.delta.add(state_lvl1, symbol, after_replace_state);
}
nft.insert_identity(after_replace_state, alphabet->get_alphabet_symbols().to_vector());
nft.final.insert(after_replace_state);
break;
}
Expand Down Expand Up @@ -408,12 +376,12 @@ nfa::Nfa ReluctantReplace::reluctant_nfa_with_marker(nfa::Nfa nfa, const Symbol
StatePost& initial{ nfa_avoid_removing_next_begin_marker.delta.mutable_state_post(0) };
const utils::OrdVector<Symbol> alphabet_symbols{ alphabet->get_alphabet_symbols() };
for (const Symbol symbol: alphabet_symbols) {
initial.push_back({ symbol, 0 });
initial.emplace_back(symbol, 0);
}
StatePost& marker_state{ nfa_avoid_removing_next_begin_marker.delta.mutable_state_post(1) };
nfa_avoid_removing_next_begin_marker.delta.add(0, marker, 1);
for (const Symbol symbol: alphabet_symbols) {
marker_state.push_back({ symbol, 0 });
marker_state.emplace_back(symbol, 0);
}
nfa_avoid_removing_next_begin_marker.delta.add(1, marker, 1);
// TODO(nft): Leaves a non-terminating begin_marker transitions in a form of a lasso from final states.
Expand Down Expand Up @@ -462,39 +430,22 @@ Nft ReluctantReplace::reluctant_leftmost_nft(nfa::Nfa nfa, Alphabet* alphabet, S
}
nft_reluctant_leftmost.levels[curr_state] = 1;
// Output the replacement.
for (const Symbol symbol: replacement) {
nft_reluctant_leftmost.delta.add(curr_state, symbol, curr_state + 1);
nft_reluctant_leftmost.delta.add(curr_state + 1, EPSILON, curr_state + 2);
nft_reluctant_leftmost.levels[curr_state + 1] = 0;
nft_reluctant_leftmost.levels[curr_state + 2] = 1;
curr_state += 2;
}
nft_reluctant_leftmost.delta.add(curr_state, EPSILON, curr_state + 1);
nft_reluctant_leftmost.levels[curr_state + 1] = 0;
nft_reluctant_leftmost.final.insert(curr_state + 1);
++curr_state;
curr_state = nft_reluctant_leftmost.insert_word_by_parts(curr_state, { {}, replacement });
State next_state{ nft_reluctant_leftmost.add_state_with_level(0) };
nft_reluctant_leftmost.delta.add(curr_state, EPSILON, next_state);
nft_reluctant_leftmost.final.insert(next_state);
nft_reluctant_leftmost.final.clear();
switch (replace_mode) {
case ReplaceMode::All: {
nft_reluctant_leftmost.delta.add(curr_state, EPSILON, initial);
nft_reluctant_leftmost.delta.add(next_state, EPSILON, initial);
break;
};
case ReplaceMode::Single: {
nft_reluctant_leftmost.levels.resize(nft_reluctant_leftmost.levels.size() + alphabet_symbols.size() + 1);
const State final{ curr_state };
const State final{ next_state };
nft_reluctant_leftmost.final.insert(final);
++curr_state;
for (const Symbol symbol: alphabet_symbols) {
nft_reluctant_leftmost.delta.add(final, symbol, curr_state);
nft_reluctant_leftmost.delta.add(curr_state, symbol, final);
nft_reluctant_leftmost.levels[curr_state] = 1;
++curr_state;
}

nft_reluctant_leftmost.delta.add(final, begin_marker, curr_state);
nft_reluctant_leftmost.delta.add(curr_state, EPSILON, final);
nft_reluctant_leftmost.levels[curr_state] = 1;
++curr_state;
nft_reluctant_leftmost.insert_identity(final, alphabet_symbols.to_vector());
nft_reluctant_leftmost.insert_word_by_parts(final, { { begin_marker }, { EPSILON } }, final);
break;
};
default: {
Expand Down
44 changes: 44 additions & 0 deletions tests/nft/nft.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4838,4 +4838,48 @@ TEST_CASE("mata::nft::Nft::insert_word_by_parts()") {
}
}
}

SECTION("begin insertion from levels != 0") {
SECTION("from level 1") {
nft = Nft{};
nft.num_of_levels = 3;
const State state_lvl1{ nft.add_state_with_level(1) };
const State target{ nft.insert_word_by_parts(state_lvl1, { { 'a', 'b', 'c' }, { 'd', 'e' }, { 'f' } }) };
CHECK(nft.levels[target] == 1);
expected = Nft{};
expected.num_of_levels = 3;
expected.delta.add(1, 'a', 2);
expected.delta.add(2, 'd', 3);
expected.delta.add(3, 'f', 4);
expected.delta.add(4, 'b', 5);
expected.delta.add(5, 'e', 6);
expected.delta.add(6, EPSILON, 7);
expected.delta.add(7, 'c', 8);
expected.delta.add(8, EPSILON, 9);
expected.delta.add(9, EPSILON, 10);
expected.levels = { 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1 };
CHECK(are_equivalent(nft, expected));
}

SECTION("from level 2") {
nft = Nft{};
nft.num_of_levels = 3;
const State state_lvl2{ nft.add_state_with_level(2) };
const State target{ nft.insert_word_by_parts(state_lvl2, { { 'a', 'b', 'c' }, { 'd', 'e' }, { 'f' } }) };
CHECK(nft.levels[target] == 2);
expected = Nft{};
expected.num_of_levels = 3;
expected.delta.add(1, 'a', 2);
expected.delta.add(2, 'd', 3);
expected.delta.add(3, 'f', 4);
expected.delta.add(4, 'b', 5);
expected.delta.add(5, 'e', 6);
expected.delta.add(6, EPSILON, 7);
expected.delta.add(7, 'c', 8);
expected.delta.add(8, EPSILON, 9);
expected.delta.add(9, EPSILON, 10);
expected.levels = { 0, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2 };
CHECK(are_equivalent(nft, expected));
}
}
}
12 changes: 6 additions & 6 deletions tests/nft/strings.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ TEST_CASE("nft::create_identity()") {
nft.levels[7] = 1;
nft.levels[8] = 2;
Nft nft_identity{ create_identity(&alphabet, 3) };
CHECK(nft_identity.is_identical(nft));
CHECK(nft::are_equivalent(nft_identity, nft));
}

SECTION("identity nft no symbols") {
Expand All @@ -69,7 +69,7 @@ TEST_CASE("nft::create_identity()") {
nft.levels.resize(1);
nft.levels[0] = 0;
Nft nft_identity{ create_identity(&alphabet, 3) };
CHECK(nft_identity.is_identical(nft));
CHECK(nft::are_equivalent(nft_identity, nft));
}

SECTION("identity nft one symbol") {
Expand All @@ -82,9 +82,9 @@ TEST_CASE("nft::create_identity()") {
nft.delta.add(0, 0, 1);
nft.delta.add(1, 0, 0);
Nft nft_identity{ create_identity(&alphabet, 2) };
CHECK(nft_identity.is_identical(nft));
CHECK(nft::are_equivalent(nft_identity, nft));
nft_identity = create_identity(&alphabet);
CHECK(nft_identity.is_identical(nft));
CHECK(nft::are_equivalent(nft_identity, nft));
}

SECTION("small identity nft one level") {
Expand All @@ -98,7 +98,7 @@ TEST_CASE("nft::create_identity()") {
nft.levels.resize(1);
nft.levels[0] = 0;
Nft nft_identity{ create_identity(&alphabet, 1) };
CHECK(nft_identity.is_identical(nft));
CHECK(nft::are_equivalent(nft_identity, nft));
}
}

Expand Down Expand Up @@ -551,7 +551,7 @@ TEST_CASE("mata::nft::strings::reluctant_leftmost_nft()") {
SECTION("single 'a+b+c' replaced with '' (empty string)") {
nft = reluctant_replace.reluctant_leftmost_nft("a+b+c", &alphabet, BEGIN_MARKER, Word{}, ReplaceMode::Single);
expected = nft::builder::parse_from_mata(std::string(
"@NFT-explicit\n%Alphabet-auto\n%Initial q14\n%Final q20 q14\n%Levels q0:0 q1:1 q2:0 q3:1 q4:1 q5:1 q6:0 q7:1 q8:1 q9:1 q10:0 q11:1 q12:0 q13:1 q14:0 q15:1 q16:1 q17:1 q18:1 q19:1 q20:0 q21:1 q22:1 q23:1 q24:1\n%LevelsCnt 2\nq0 97 q1\nq0 4294967195 q3\nq1 4294967295 q2\nq2 97 q4\nq2 98 q5\nq2 4294967195 q7\nq3 4294967295 q0\nq4 4294967295 q2\nq5 4294967295 q6\nq6 98 q8\nq6 99 q9\nq6 4294967195 q11\nq7 4294967295 q2\nq8 4294967295 q6\nq9 4294967295 q10\nq10 4294967295 q19\nq11 4294967295 q6\nq12 4294967195 q13\nq13 4294967295 q12\nq14 97 q15\nq14 98 q16\nq14 99 q17\nq14 4294967195 q18\nq15 97 q14\nq16 98 q14\nq17 99 q14\nq18 4294967295 q0\nq19 4294967295 q20\nq20 97 q21\nq20 98 q22\nq20 99 q23\nq20 4294967195 q24\nq21 97 q20\nq22 98 q20\nq23 99 q20\nq24 4294967295 q20\n"
"@NFT-explicit\n%Alphabet-auto\n%Initial q14\n%Final q22 q14\n%Levels q0:0 q1:1 q2:0 q3:1 q4:1 q5:1 q6:0 q7:1 q8:1 q9:1 q10:0 q11:1 q12:0 q13:1 q14:0 q15:1 q16:1 q17:1 q18:1 q19:1 q20:1 q21:0 q22:0 q23:1 q24:1 q25:1 q26:1\n%LevelsCnt 2\nq0 97 q1\nq0 4294967195 q3\nq1 4294967295 q2\nq2 97 q4\nq2 98 q5\nq2 4294967195 q7\nq3 4294967295 q0\nq4 4294967295 q2\nq5 4294967295 q6\nq6 98 q8\nq6 99 q9\nq6 4294967195 q11\nq7 4294967295 q2\nq8 4294967295 q6\nq9 4294967295 q10\nq10 4294967295 q19\nq11 4294967295 q6\nq12 4294967195 q13\nq13 4294967295 q12\nq14 97 q15\nq14 98 q16\nq14 99 q17\nq14 4294967195 q18\nq15 97 q14\nq16 98 q14\nq17 99 q14\nq18 4294967295 q0\nq19 4294967295 q21\nq20 4294967295 q22\nq21 4294967295 q20\nq22 97 q23\nq22 98 q24\nq22 99 q25\nq22 4294967195 q26\nq23 97 q22\nq24 98 q22\nq25 99 q22\nq26 4294967295 q22\n"
));
CHECK(nft::are_equivalent(nft, expected));
CHECK(nft.is_tuple_in_lang({ Word{ BEGIN_MARKER, 'a', BEGIN_MARKER, 'a', BEGIN_MARKER, 'a', 'b', 'b', 'c', 'c', 'b', 'a', 'c' }, Word{ 'c', 'b', 'a', 'c' } }));
Expand Down

0 comments on commit 880d99b

Please sign in to comment.