diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 03cab284a..78ad6d544 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -636,6 +636,7 @@ public: } family_id get_family_id() const { return m_fid; } + family_id get_char_family_id() const { return ch.get_family_id(); } }; inline std::ostream& operator<<(std::ostream& out, seq_util::rex::pp const & p) { return p.display(out); } diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 25700126b..4e40fd13d 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -72,7 +72,7 @@ namespace sls { register_plugin(alloc(array_plugin, *this)); else if (fid == datatype_util(m).get_family_id()) register_plugin(alloc(datatype_plugin, *this)); - else if (fid == seq_util(m).get_family_id()) + else if (fid == seq_util(m).get_family_id() || fid == seq_util(m).get_char_family_id()) register_plugin(alloc(seq_plugin, *this)); else verbose_stream() << "did not find plugin for " << fid << "\n"; diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 8313d22de..70d639965 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -116,7 +116,7 @@ namespace sls { { m_fid = seq.get_family_id(); sls_params p(c.get_params()); - m_str_update_strategy = p.str_update_strategy() == 0 ? EDIT_CHAR : EDIT_SUBSTR; + m_str_update_strategy = (edit_distance_strategy)p.str_update_strategy(); } void seq_plugin::propagate_literal(sat::literal lit) { @@ -681,11 +681,17 @@ namespace sls { return d[n][m]; } - void seq_plugin::add_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars) { + void seq_plugin::add_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars, unsigned diff) { if (m_str_update_strategy == EDIT_CHAR) add_char_edit_updates(w, val, val_other, chars); - else + else if (m_str_update_strategy == EDIT_SUBSTR) add_substr_edit_updates(w, val, val_other, chars); + else { + if (diff < 3) + add_char_edit_updates(w, val, val_other, chars); + else + add_substr_edit_updates(w, val, val_other, chars); + } } void seq_plugin::add_substr_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars) { @@ -1012,6 +1018,9 @@ namespace sls { b_chars.insert(ch); b += strval0(y); } + + // std::cout << "Repair down " << mk_pp(eq, m) << ": \"" << a << "\" = \"" << b << "\"" << std::endl; + if (a == b) return update(eq->get_arg(0), a) && update(eq->get_arg(1), b); @@ -1019,8 +1028,8 @@ namespace sls { //verbose_stream() << "solve: " << diff << " " << a << " " << b << "\n"; - add_edit_updates(L, a, b, b_chars); - add_edit_updates(R, b, a, a_chars); + add_edit_updates(L, a, b, b_chars, diff); + add_edit_updates(R, b, a, a_chars, diff); for (auto& [x, s, score] : m_str_updates) { a.reset(); @@ -1577,9 +1586,9 @@ namespace sls { for (auto ch : value0) chars.insert(ch); - add_edit_updates(es, value, value0, chars); - unsigned diff = edit_distance(value, value0); + add_edit_updates(es, value, value0, chars, diff); + for (auto& [x, s, score] : m_str_updates) { value.reset(); for (auto z : es) { diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index 7c7fc16ff..ae53cc3ac 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -43,8 +43,9 @@ namespace sls { }; enum edit_distance_strategy { - EDIT_CHAR, - EDIT_SUBSTR, + EDIT_CHAR = 0, + EDIT_SUBSTR = 1, + EDIT_COMBINED = 2, }; seq_util seq; @@ -127,7 +128,7 @@ namespace sls { void init_string_instance(ptr_vector const& es, string_instance& a); unsigned edit_distance_with_updates(string_instance const& a, string_instance const& b); unsigned edit_distance(zstring const& a, zstring const& b); - void add_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars); + void add_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars, unsigned diff); void add_char_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars); void add_substr_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars); diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg index 7ac16479e..1c7c0e0e5 100644 --- a/src/params/sls_params.pyg +++ b/src/params/sls_params.pyg @@ -29,5 +29,5 @@ def_module_params('sls', ('bv_use_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'), ('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'), ('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'), - ('str_update_strategy', UINT, 1, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update') + ('str_update_strategy', UINT, 2, 'string update candidate selection: 0 - single character based update, 1 - subsequence based update, 2 - combined') ))