mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 08:53:18 +00:00
Code Activity

#5518

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-31 16:38:27 -07:00
parent ab2baa764c
commit 1426390aec
3 changed files with 10 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -558,6 +558,7 @@ namespace array {
bool solver::add_interface_equalities() { bool solver::add_interface_equalities() {
sbuffer<theory_var> roots; sbuffer<theory_var> roots;
collect_defaults();
collect_shared_vars(roots); collect_shared_vars(roots);
bool prop = false; bool prop = false;
for (unsigned i = roots.size(); i-- > 0; ) { for (unsigned i = roots.size(); i-- > 0; ) {

36
src/sat/smt/array_model.cpp
View file

@ -72,20 +72,6 @@ namespace array {
if (!fi->get_else() && get_else(v)) if (!fi->get_else() && get_else(v))
fi->set_else(get_else(v)); fi->set_else(get_else(v));
#if 0
// this functionality is already taken care of by model_init.
if (!fi->get_else())
for (euf::enode* k : euf::enode_class(n))
if (a.is_const(k->get_expr()))
fi->set_else(values.get(k->get_arg(0)->get_root_id()));
if (!fi->get_else())
for (euf::enode* p : euf::enode_parents(n))
if (a.is_default(p->get_expr()))
fi->set_else(values.get(p->get_root_id()));
#endif
if (!fi->get_else()) { if (!fi->get_else()) {
expr* else_value = nullptr; expr* else_value = nullptr;
@ -135,24 +121,16 @@ namespace array {
euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2); euf::enode* n1 = var2enode(v1), *n2 = var2enode(v2);
euf::enode* r1 = n1->get_root(), * r2 = n2->get_root(); euf::enode* r1 = n1->get_root(), * r2 = n2->get_root();
expr* e1 = n1->get_expr(); expr* e1 = n1->get_expr();
expr* e;
if (!a.is_array(e1)) if (!a.is_array(e1))
return true; return true;
auto find_else = [&](theory_var v, euf::enode* r) {
var_data& d = get_var_data(find(v)); else1 = get_default(v1);
for (euf::enode* c : d.m_lambdas) else2 = get_default(v2);
if (a.is_const(c->get_expr(), e))
return expr2enode(e)->get_root();
for (euf::enode* p : euf::enode_parents(r))
for (euf::enode* pe : euf::enode_class(p))
if (a.is_default(pe->get_expr()))
return pe->get_root();
return (euf::enode*)nullptr;
};
else1 = find_else(v1, r1);
else2 = find_else(v2, r2);
if (else1 && else2 && else1->get_root() != else2->get_root() && has_large_domain(e1)) if (else1 && else2 && else1->get_root() != else2->get_root() && has_large_domain(e1))
return true; return true;
return false;
#if 0
struct eq { struct eq {
solver& s; solver& s;
eq(solver& s) :s(s) {} eq(solver& s) :s(s) {}
@ -196,6 +174,8 @@ namespace array {
}; };
return table_diff(r1, r2, else1) || table_diff(r2, r1, else2); return table_diff(r1, r2, else1) || table_diff(r2, r1, else2);
#endif
} }
void solver::collect_defaults() { void solver::collect_defaults() {

2
src/sat/smt/euf_solver.h
View file

@ -310,7 +310,7 @@ namespace euf {
std::ostream& display(std::ostream& out) const override; std::ostream& display(std::ostream& out) const override;
std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override; std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override; std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
euf::egraph::b_pp bpp(enode* n) { return m_egraph.bpp(n); } euf::egraph::b_pp bpp(enode* n) const { return m_egraph.bpp(n); }
clause_pp pp(literal_vector const& lits) { return clause_pp(*this, lits); } clause_pp pp(literal_vector const& lits) { return clause_pp(*this, lits); }
void collect_statistics(statistics& st) const override; void collect_statistics(statistics& st) const override;
extension* copy(sat::solver* s) override; extension* copy(sat::solver* s) override;