mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-28 14:08:55 +00:00
Code Activity

Trying hybrid eq-repair strategy

Browse source
This commit is contained in:
CEisenhofer 2025-01-21 10:52:03 +01:00
parent 78b77b9d1e
commit 791ad83e4e
5 changed files with 23 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/seq_decl_plugin.h
View file

@ -636,6 +636,7 @@ public:
} }
family_id get_family_id() const { return m_fid; } 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); } inline std::ostream& operator<<(std::ostream& out, seq_util::rex::pp const & p) { return p.display(out); }

2
src/ast/sls/sls_context.cpp
View file

@ -72,7 +72,7 @@ namespace sls {
register_plugin(alloc(array_plugin, *this)); register_plugin(alloc(array_plugin, *this));
else if (fid == datatype_util(m).get_family_id()) else if (fid == datatype_util(m).get_family_id())
register_plugin(alloc(datatype_plugin, *this)); 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)); register_plugin(alloc(seq_plugin, *this));
else else
verbose_stream() << "did not find plugin for " << fid << "\n"; verbose_stream() << "did not find plugin for " << fid << "\n";

23
src/ast/sls/sls_seq_plugin.cpp
View file

@ -116,7 +116,7 @@ namespace sls {
{ {
m_fid = seq.get_family_id(); m_fid = seq.get_family_id();
sls_params p(c.get_params()); 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) { void seq_plugin::propagate_literal(sat::literal lit) {
@ -681,11 +681,17 @@ namespace sls {
return d[n][m]; return d[n][m];
} }
void seq_plugin::add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) { void seq_plugin::add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars, unsigned diff) {
if (m_str_update_strategy == EDIT_CHAR) if (m_str_update_strategy == EDIT_CHAR)
add_char_edit_updates(w, val, val_other, chars); 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); 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<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) { void seq_plugin::add_substr_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
@ -1012,6 +1018,9 @@ namespace sls {
b_chars.insert(ch); b_chars.insert(ch);
b += strval0(y); b += strval0(y);
} }
// std::cout << "Repair down " << mk_pp(eq, m) << ": \"" << a << "\" = \"" << b << "\"" << std::endl;
if (a == b) if (a == b)
return update(eq->get_arg(0), a) && update(eq->get_arg(1), 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"; //verbose_stream() << "solve: " << diff << " " << a << " " << b << "\n";
add_edit_updates(L, a, b, b_chars); add_edit_updates(L, a, b, b_chars, diff);
add_edit_updates(R, b, a, a_chars); add_edit_updates(R, b, a, a_chars, diff);
for (auto& [x, s, score] : m_str_updates) { for (auto& [x, s, score] : m_str_updates) {
a.reset(); a.reset();
@ -1577,9 +1586,9 @@ namespace sls {
for (auto ch : value0) for (auto ch : value0)
chars.insert(ch); chars.insert(ch);
add_edit_updates(es, value, value0, chars);
unsigned diff = edit_distance(value, value0); unsigned diff = edit_distance(value, value0);
add_edit_updates(es, value, value0, chars, diff);
for (auto& [x, s, score] : m_str_updates) { for (auto& [x, s, score] : m_str_updates) {
value.reset(); value.reset();
for (auto z : es) { for (auto z : es) {

7
src/ast/sls/sls_seq_plugin.h
View file

@ -43,8 +43,9 @@ namespace sls {
}; };
enum edit_distance_strategy { enum edit_distance_strategy {
EDIT_CHAR, EDIT_CHAR = 0,
EDIT_SUBSTR, EDIT_SUBSTR = 1,
EDIT_COMBINED = 2,
}; };
seq_util seq; seq_util seq;
@ -127,7 +128,7 @@ namespace sls {
void init_string_instance(ptr_vector<expr> const& es, string_instance& a); void init_string_instance(ptr_vector<expr> const& es, string_instance& a);
unsigned edit_distance_with_updates(string_instance const& a, string_instance const& b); unsigned edit_distance_with_updates(string_instance const& a, string_instance const& b);
unsigned edit_distance(zstring const& a, zstring const& b); unsigned edit_distance(zstring const& a, zstring const& b);
void add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars); void add_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars, unsigned diff);
void add_char_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars); void add_char_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);
void add_substr_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars); void add_substr_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);

2
src/params/sls_params.pyg
View file

@ -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_top_level_assertions', BOOL, True, 'use top-level assertions for BV lookahead solver'),
('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'), ('bv_use_lookahead', BOOL, True, 'use lookahead solver for BV'),
('bv_allow_rotation', BOOL, True, 'allow model rotation when repairing literal assignment'), ('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')
)) ))