mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

fix #7461

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-09 16:57:17 -08:00
parent 8f5658b77d
commit e8c2360043
3 changed files with 34 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -697,18 +697,18 @@ namespace sls {
u[i][j] = d[i - 1][j - 1];
}
if (d[i - 1][j] == u[i][j] && !a_is_value[i - 1]) {
add_string_update(side::left, op::del, i - 1, 0);
add_string_update(side::left, op::add, j - 1, i - 1);
add_string_update(side_t::left, op_t::del, i - 1, 0);
add_string_update(side_t::left, op_t::add, j - 1, i - 1);
}
if (d[i][j - 1] == u[i][j] && !b_is_value[j - 1]) {
add_string_update(side::right, op::del, j - 1, 0);
add_string_update(side::right, op::add, i - 1, j - 1);
add_string_update(side_t::right, op_t::del, j - 1, 0);
add_string_update(side_t::right, op_t::add, i - 1, j - 1);
}
if (d[i - 1][j - 1] == u[i][j] && !a_is_value[i - 1])
add_string_update(side::left, op::copy, j - 1, i - 1);
add_string_update(side_t::left, op_t::copy, j - 1, i - 1);
if (d[i - 1][j - 1] == u[i][j] && !b_is_value[j - 1])
add_string_update(side::right, op::copy, i - 1, j - 1);
add_string_update(side_t::right, op_t::copy, i - 1, j - 1);
}
}
@ -833,20 +833,20 @@ namespace sls {
#if 1
for (auto const& [side, op, i, j] : m_string_updates) {
switch (op) {
case op::del:
if (side == side::left)
case op_t::del:
if (side == side_t::left)
verbose_stream() << "del " << a[i] << " @ " << i << " left\n";
else
verbose_stream() << "del " << b[i] << " @ " << i << " right\n";
break;
case op::add:
if (side == side::left)
case op_t::add:
if (side == side_t::left)
verbose_stream() << "add " << b[i] << " @ " << j << " left\n";
else
verbose_stream() << "add " << a[i] << " @ " << j << " right\n";
break;
case op::copy:
if (side == side::left)
case op_t::copy:
if (side == side_t::left)
verbose_stream() << "copy " << b[i] << " @ " << j << " left\n";
else
verbose_stream() << "copy " << a[i] << " @ " << j << " right\n";
@ -855,7 +855,7 @@ namespace sls {
}
#endif
for (auto& [side, op, i, j] : m_string_updates) {
if (op == op::del && side == side::left) {
if (op == op_t::del && side == side_t::left) {
for (auto x : L) {
auto const& value = strval0(x);
@ -868,7 +868,7 @@ namespace sls {
}
}
}
else if (op == op::del && side == side::right) {
else if (op == op_t::del && side == side_t::right) {
for (auto x : R) {
auto const& value = strval0(x);
if (i >= value.length())
@ -880,7 +880,7 @@ namespace sls {
}
}
}
else if (op == op::add && side == side::left) {
else if (op == op_t::add && side == side_t::left) {
for (auto x : L) {
auto const& value = strval0(x);
//verbose_stream() << "add " << j << " " << value << " " << value.length() << " " << is_value(x) << "\n";
@ -894,7 +894,7 @@ namespace sls {
break;
}
}
else if (op == op::add && side == side::right) {
else if (op == op_t::add && side == side_t::right) {
for (auto x : R) {
auto const& value = strval0(x);
//verbose_stream() << "add " << j << " " << value << " " << value.length() << " " << is_value(x) << "\n";
@ -908,7 +908,7 @@ namespace sls {
break;
}
}
else if (op == op::copy && side == side::left) {
else if (op == op_t::copy && side == side_t::left) {
for (auto x : L) {
auto const& value = strval0(x);
if (j >= value.length())
@ -920,7 +920,7 @@ namespace sls {
}
}
}
else if (op == op::copy && side == side::right) {
else if (op == op_t::copy && side == side_t::right) {
for (auto x : R) {
auto const& value = strval0(x);
if (j >= value.length())

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

@ -92,19 +92,19 @@ namespace sls {
void repair_up_str_itos(app* e);
void repair_up_str_stoi(app* e);
enum op {
enum op_t {
add, del, copy
};
enum side {
enum side_t {
left, right
};
struct string_update {
side side;
op op;
side_t side;
op_t op;
unsigned i, j;
};
svector<string_update> m_string_updates;
void add_string_update(side side, op op, unsigned i, unsigned j) { m_string_updates.push_back({ side, op, i, j }); }
void add_string_update(side_t side, op_t op, unsigned i, unsigned j) { m_string_updates.push_back({ side, op, i, j }); }
unsigned edit_distance_with_updates(zstring const& a, bool_vector const& a_is_value, zstring const& b, bool_vector const& b_is_value);
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);

11
src/shell/main.cpp
View file

@ -123,6 +123,13 @@ void display_usage() {
std::cout << " module_name.param_name=value for setting module parameters.\n";
std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n";
}
static bool validate_is_ulong(char const* s) {
for (; *s; ++s)
if (*s < '0' || *s > '9')
return false;
return true;
}
static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) {
long timeout = 0;
@ -220,6 +227,8 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv)
else if (strcmp(opt_name, "v") == 0) {
if (!opt_arg)
error("option argument (-v:level) is missing.");
if (!validate_is_ulong(opt_arg))
error("invalid argument for -v option, it must be a non-negative integer.");
long lvl = strtol(opt_arg, nullptr, 10);
set_verbosity_level(lvl);
}
@ -229,6 +238,8 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv)
else if (strcmp(opt_name, "T") == 0) {
if (!opt_arg)
error("option argument (-T:timeout) is missing.");
if (!validate_is_ulong(opt_arg))
error("invalid argument for -T option, it must be a non-negative integer.");
timeout = strtol(opt_arg, nullptr, 10);
}
else if (strcmp(opt_name, "t") == 0) {