mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
This commit is contained in:
parent
46f8b15c14
commit
fb75dac63f
|
@ -59,6 +59,7 @@ class bit_blaster : public bit_blaster_tpl<bit_blaster_cfg> {
|
|||
public:
|
||||
bit_blaster(ast_manager & m, bit_blaster_params const & params);
|
||||
bit_blaster_params const & get_params() const { return this->m_params; }
|
||||
void set_flat(bool f) { m_rw.set_flat(f); }
|
||||
};
|
||||
|
||||
|
||||
|
|
|
@ -1029,7 +1029,7 @@ namespace sat {
|
|||
return false;
|
||||
} while (m_qhead < m_trail.size());
|
||||
|
||||
if (m_ext && !is_probing())
|
||||
if (m_ext && (!is_probing() || at_base_lvl()))
|
||||
m_ext->unit_propagate();
|
||||
}
|
||||
if (m_inconsistent)
|
||||
|
|
|
@ -174,9 +174,13 @@ namespace array {
|
|||
SASSERT(store->get_num_args() == 1 + select->get_num_args());
|
||||
ptr_buffer<expr> sel1_args, sel2_args;
|
||||
unsigned num_args = select->get_num_args();
|
||||
|
||||
if (expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root())
|
||||
return false;
|
||||
|
||||
sel1_args.push_back(store);
|
||||
sel2_args.push_back(store->get_arg(0));
|
||||
|
||||
|
||||
bool has_diff = false;
|
||||
for (unsigned i = 1; i < num_args; i++)
|
||||
has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();
|
||||
|
@ -191,6 +195,7 @@ namespace array {
|
|||
expr_ref sel1(a.mk_select(sel1_args), m);
|
||||
expr_ref sel2(a.mk_select(sel2_args), m);
|
||||
expr_ref sel_eq_e(m.mk_eq(sel1, sel2), m);
|
||||
|
||||
euf::enode* s1 = e_internalize(sel1);
|
||||
euf::enode* s2 = e_internalize(sel2);
|
||||
TRACE("array",
|
||||
|
@ -200,9 +205,13 @@ namespace array {
|
|||
if (s1->get_root() == s2->get_root())
|
||||
return false;
|
||||
|
||||
sat::literal sel_eq = mk_literal(sel_eq_e);
|
||||
if (s().value(sel_eq) == l_true)
|
||||
return false;
|
||||
sat::literal sel_eq = sat::null_literal;
|
||||
auto init_sel_eq = [&]() {
|
||||
if (sel_eq != sat::null_literal)
|
||||
return true;
|
||||
sel_eq = mk_literal(sel_eq_e);
|
||||
return s().value(sel_eq) != l_true;
|
||||
};
|
||||
|
||||
bool new_prop = false;
|
||||
for (unsigned i = 1; i < num_args; i++) {
|
||||
|
@ -213,11 +222,17 @@ namespace array {
|
|||
if (r1 == r2)
|
||||
continue;
|
||||
if (m.are_distinct(r1->get_expr(), r2->get_expr())) {
|
||||
new_prop = true;
|
||||
add_clause(sel_eq);
|
||||
if (init_sel_eq() && add_clause(sel_eq))
|
||||
new_prop = true;
|
||||
break;
|
||||
}
|
||||
sat::literal idx_eq = eq_internalize(idx1, idx2);
|
||||
if (s().value(idx_eq) == l_true)
|
||||
continue;
|
||||
if (s().value(idx_eq) == l_undef)
|
||||
new_prop = true;
|
||||
if (!init_sel_eq())
|
||||
break;
|
||||
if (add_clause(idx_eq, sel_eq))
|
||||
new_prop = true;
|
||||
}
|
||||
|
|
|
@ -55,6 +55,7 @@ namespace bv {
|
|||
m_ackerman(*this),
|
||||
m_bb(m, get_config()),
|
||||
m_find(*this) {
|
||||
m_bb.set_flat(false);
|
||||
}
|
||||
|
||||
void solver::fixed_var_eh(theory_var v1) {
|
||||
|
|
|
@ -253,13 +253,14 @@ namespace euf {
|
|||
if (!is_relevant(n))
|
||||
continue;
|
||||
bool tt = l_true == s().value(n->bool_var());
|
||||
if (tt && mdl.is_false(e)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "Failed to validate " << bpp(n) << " " << mdl(e) << "\n");
|
||||
for (auto* arg : euf::enode_args(n))
|
||||
IF_VERBOSE(0, verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n");
|
||||
}
|
||||
if (!tt && mdl.is_true(e))
|
||||
IF_VERBOSE(0, verbose_stream() << "Failed to validate " << bpp(n) << " " << mdl(e) << "\n");
|
||||
if (tt && !mdl.is_false(e))
|
||||
continue;
|
||||
if (!tt && !mdl.is_true(e))
|
||||
continue;
|
||||
IF_VERBOSE(0,
|
||||
verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
|
||||
for (auto* arg : euf::enode_args(n))
|
||||
verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n";);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue