mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

Commented out debug output

Browse source
This commit is contained in:
CEisenhofer 2024-12-30 19:35:49 +01:00
parent 809267258d
commit c468ff4f97
2 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -879,6 +879,12 @@ namespace sls {
return u[n][m]; return u[n][m];
} }
int seq_plugin::add_str_update(expr* e, zstring const& val, double score) {
zstring new_v = trunc_pad_to_fit(get_eval(e).min_length, get_eval(e).max_length, val);
m_str_updates.push_back({ e, new_v, score });
return new_v.length() == val.length() ? 0 : (new_v.length() > val.length() ? 1 : -1);
}
zstring seq_plugin::trunc_pad_to_fit(unsigned min_length, unsigned max_length, zstring const& s) { zstring seq_plugin::trunc_pad_to_fit(unsigned min_length, unsigned max_length, zstring const& s) {
if (s.length() > max_length) if (s.length() > max_length)
return s.extract(0, max_length); return s.extract(0, max_length);
@ -1708,7 +1714,7 @@ namespace sls {
} }
} }
std::cout << "No candidate found" << std::endl; // std::cout << "No candidate found" << std::endl;
return false; return false;
} }

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

@ -131,6 +131,7 @@ namespace sls {
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);
int add_str_update(expr* e, zstring const& val, double score);
zstring trunc_pad_to_fit(unsigned min_length, unsigned max_length, zstring const& s); zstring trunc_pad_to_fit(unsigned min_length, unsigned max_length, zstring const& s);
// regex functionality // regex functionality