mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 16:40:29 +00:00
Code Activity

fix rewriting of complemnt of ranges

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-20 11:07:52 -07:00
parent 881360db5a
commit 871b98169f
3 changed files with 30 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/ast/rewriter/seq_rewriter.cpp
View file

@ -4832,26 +4832,32 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
sort* srt = a->get_sort();
bool has_left = (lo_v > 0);
bool has_right = (hi_v < max_c);
auto empty_re = [&]() { return re().mk_empty(srt); };
auto full_re = [&]() { return re().mk_full_seq(srt); };
if (!has_left && !has_right) {
// [0, max_c]: complement is empty
result = re().mk_empty(srt);
result = empty_re();
return BR_DONE;
}
if (lo_v > hi_v) {
result = full_re();
return BR_DONE;
}
if (!has_left) {
// [0, b]: complement is [b+1, max]
result = re().mk_range(srt, hi_v + 1, max_c);
return BR_REWRITE1;
result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, hi_v + 1, max_c), full_re()));
return BR_DONE;
}
if (!has_right) {
// [a, max]: complement is [0, a-1]
result = re().mk_range(srt, 0u, lo_v - 1);
return BR_REWRITE1;
result = re().mk_union(empty_re(), re().mk_concat(re().mk_range(srt, 0u, lo_v - 1), full_re()));
return BR_DONE;
}
// General: [a, b] → [0, a-1] ∪ [b+1, max]
auto left = re().mk_range(srt, 0u, lo_v - 1);
auto right = re().mk_range(srt, hi_v + 1, max_c);
result = re().mk_union(left, right);
return BR_REWRITE1;
result = re().mk_union(empty_re(), re().mk_concat(re().mk_union(left, right), full_re()));
return BR_DONE;
}
return BR_FAILED;
}

16
src/smt/theory_array.cpp
View file

@ -396,15 +396,15 @@ namespace smt {
}
final_check_status theory_array::assert_delayed_axioms() {
if (!m_params.m_array_delay_exp_axiom)
return FC_DONE;
final_check_status r = FC_DONE;
unsigned num_vars = get_num_vars();
for (unsigned v = 0; v < num_vars; ++v) {
var_data * d = m_var_data[v];
if (d->m_prop_upward && instantiate_axiom2b_for(v))
r = FC_CONTINUE;
}
if (m_params.m_array_delay_exp_axiom) {
unsigned num_vars = get_num_vars();
for (unsigned v = 0; v < num_vars; ++v) {
var_data *d = m_var_data[v];
if (d->m_prop_upward && instantiate_axiom2b_for(v))
r = FC_CONTINUE;
}
}
return r;
}

20
src/smt/theory_array_base.cpp
View file

@ -67,7 +67,6 @@ namespace smt {
return mk_select(num_args, args);
}
app * theory_array_base::mk_store(unsigned num_args, expr * const * args) {
return m.mk_app(get_family_id(), OP_STORE, 0, nullptr, num_args, args);
}
@ -279,7 +278,7 @@ namespace smt {
SASSERT(n1->get_num_args() == n2->get_num_args());
unsigned n = n1->get_num_args();
// skipping first argument of the select.
for(unsigned i = 1; i < n; ++i) {
for (unsigned i = 1; i < n; ++i) {
if (n1->get_arg(i)->get_root() != n2->get_arg(i)->get_root()) {
return false;
}
@ -295,9 +294,8 @@ namespace smt {
enode * r1 = v1->get_root();
enode * r2 = v2->get_root();
if (r1->get_class_size() > r2->get_class_size()) {
std::swap(r1, r2);
}
if (r1->get_class_size() > r2->get_class_size())
std::swap(r1, r2);
m_array_value.reset();
// populate m_array_value if the select(a, i) parent terms of r1
@ -335,7 +333,7 @@ namespace smt {
return false; // axiom was already instantiated
if (already_diseq(n1, n2))
return false;
m_extensionality_todo.push_back(std::make_pair(n1, n2));
m_extensionality_todo.push_back({n1, n2});
return true;
}
@ -348,7 +346,7 @@ namespace smt {
enode * nodes[2] = { a1, a2 };
if (!ctx.add_fingerprint(this, 1, 2, nodes))
return; // axiom was already instantiated
m_congruent_todo.push_back(std::make_pair(a1, a2));
m_congruent_todo.push_back({a1, a2});
}
@ -581,11 +579,11 @@ namespace smt {
enode * n2 = get_enode(v2);
sort * s2 = n2->get_sort();
if (s1 == s2 && !ctx.is_diseq(n1, n2)) {
app * eq = mk_eq_atom(n1->get_expr(), n2->get_expr());
if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) {
app_ref eq = app_ref(mk_eq_atom(n1->get_expr(), n2->get_expr()), m);
if (!ctx.b_internalized(eq.get()) || !ctx.is_relevant(eq.get())) {
result++;
ctx.internalize(eq, true);
ctx.mark_as_relevant(eq);
ctx.mark_as_relevant(eq.get());
}
}
}
@ -850,7 +848,7 @@ namespace smt {
if (i < num_args) {
SASSERT(!parent_sel_set->contains(sel) || (*(parent_sel_set->find(sel)))->get_root() == sel->get_root());
parent_sel_set->insert(sel);
todo.push_back(std::make_pair(parent_root, sel));
todo.push_back({parent_root, sel});
}
}
}