mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

#5454 again

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-18 13:32:46 -07:00
parent 2492278a4b
commit adcdd11afc
1 changed files with 8 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/sat/smt/array_axioms.cpp
View file

@ -120,9 +120,15 @@ namespace array {
app* select = r.select->get_app(); app* select = r.select->get_app();
SASSERT(a.is_select(select)); SASSERT(a.is_select(select));
SASSERT(can_beta_reduce(r.n)); SASSERT(can_beta_reduce(r.n));
TRACE("array", display(tout << "select-axiom: ", r) << "\n";);
if (get_config().m_array_delay_exp_axiom && r.select->get_arg(0)->get_root() != r.n->get_root() && !r.is_delayed() && m_enable_delay) { bool should_delay =
get_config().m_array_delay_exp_axiom &&
r.select->get_arg(0)->get_root() != r.n->get_root() &&
!r.is_delayed() && m_enable_delay;
TRACE("array", display(tout << "select-axiom: " << (should_delay ? "delay " : ""), r) << "\n";);
if (should_delay) {
IF_VERBOSE(11, verbose_stream() << "delay: " << mk_bounded_pp(child, m) << " " << mk_bounded_pp(select, m) << "\n"); IF_VERBOSE(11, verbose_stream() << "delay: " << mk_bounded_pp(child, m) << " " << mk_bounded_pp(select, m) << "\n");
ctx.push(reset_new(*this, idx)); ctx.push(reset_new(*this, idx));
r.set_delayed(); r.set_delayed();
@ -176,8 +182,6 @@ namespace array {
unsigned num_args = select->get_num_args(); unsigned num_args = select->get_num_args();
expr* arg = select->get_arg(0); expr* arg = select->get_arg(0);
if (false && arg != store && !can_beta_reduce(arg) && expr2enode(arg)->get_root() == expr2enode(store)->get_root())
return false;
bool has_diff = false; bool has_diff = false;
for (unsigned i = 1; i < num_args; i++) for (unsigned i = 1; i < num_args; i++)
has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root(); has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
@ -209,9 +213,6 @@ namespace array {
tout << "select-store " << ctx.bpp(s2) << " " << ctx.bpp(s2->get_root()) << "\n";); tout << "select-store " << ctx.bpp(s2) << " " << ctx.bpp(s2->get_root()) << "\n";);
if (s1->get_root() == s2->get_root())
return new_prop;
sat::literal sel_eq = sat::null_literal; sat::literal sel_eq = sat::null_literal;
auto init_sel_eq = [&]() { auto init_sel_eq = [&]() {
if (sel_eq != sat::null_literal) if (sel_eq != sat::null_literal)