mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Renamed function

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 09:44:28 +01:00
parent c1c6276ae2
commit 85c5feb0b2
2 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -673,7 +673,7 @@ namespace sls {
}
void seq_plugin::add_edit_updates2(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) {
// all consecutive subsequences of val_other
map<zstring, bool, zstring_hash_proc, default_eq<zstring>> map;
vector<zstring> subseqs;
@ -701,7 +701,7 @@ namespace sls {
}
}
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_step_edit_updates(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars) {
for (auto x : w) {
if (is_value(x))
continue;
@ -991,8 +991,11 @@ 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_step_edit_updates(L, a, b, b_chars);
// add_step_edit_updates(R, b, a, a_chars);
add_substr_edit_updates(L, a, b, b_chars);
add_substr_edit_updates(R, b, a, a_chars);
for (auto& [x, s, score] : m_str_updates) {
a.reset();
@ -1522,8 +1525,8 @@ namespace sls {
for (auto ch : value0)
chars.insert(ch);
// add_edit_updates(es, value, value0, chars);
add_edit_updates2(es, value, value0, chars);
// add_step_edit_updates(es, value, value0, chars);
add_substr_edit_updates(es, value, value0, chars);
unsigned diff = edit_distance(value, value0);
for (auto& [x, s, score] : m_str_updates) {

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

@ -121,8 +121,8 @@ namespace sls {
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(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_updates2(ptr_vector<expr> const& w, zstring const& val, zstring const& val_other, uint_set const& chars);
void add_step_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);
// regex functionality