mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

#5593

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-10-13 17:50:56 -07:00
parent fd77f0c111
commit 7b341313d5
1 changed files with 34 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/smt/theory_array_full.cpp
View file

@ -707,6 +707,38 @@ namespace smt {
} }
else if (!has_large_domain(store_app)) { else if (!has_large_domain(store_app)) {
// //
// let A = store(B, i, v)
//
// Add:
// default(A) = A[epsilon]
// default(B) = B[epsilon]
//
//
expr_ref_vector args1(m), args2(m);
args1.push_back(store_app->get_arg(0));
args2.push_back(store_app);
for (unsigned i = 1; i + 1 < num_args; ++i) {
expr* arg = store_app->get_arg(i);
sort* srt = arg->get_sort();
auto ep = mk_epsilon(srt);
args1.push_back(ep.first);
args2.push_back(ep.first);
}
app_ref sel1(m), sel2(m);
sel1 = mk_select(args1);
sel2 = mk_select(args2);
ctx.internalize(def1, false);
ctx.internalize(def2, false);
is_new = try_assign_eq(def1, sel1) || try_assign_eq(def2, sel2);
return is_new;
#if 0
//
// This is incorrect, issue #5593.
//
// let A = store(B, i, v) // let A = store(B, i, v)
// //
// Add: // Add:
@ -731,7 +763,9 @@ namespace smt {
app_ref sel1(m), sel2(m); app_ref sel1(m), sel2(m);
sel1 = mk_select(args1); sel1 = mk_select(args1);
sel2 = mk_select(args2); sel2 = mk_select(args2);
std::cout << "small domain " << sel1 << " " << sel2 << "\n";
is_new = try_assign_eq(sel1, sel2); is_new = try_assign_eq(sel1, sel2);
#endif
} }
ctx.internalize(def1, false); ctx.internalize(def1, false);