mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

delay distinct axiom

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-18 15:41:42 -07:00
parent 6c3fe3cf46
commit 3f33e2c098
2 changed files with 72 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

62
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -86,7 +86,8 @@ namespace sls {
g(c.egraph()),
dt(m),
m_axioms(m),
m_values(m) {
m_values(m),
m_eval(m) {
m_fid = dt.get_family_id();
}
@ -227,6 +228,9 @@ namespace sls {
ors.push_back(m.mk_app(r, t));
}
m_axioms.push_back(m.mk_or(ors));
#if 0
// expanded lazily
// EUF already handles enumeration datatype case.
for (unsigned i = 0; i < cns.size(); ++i) {
auto r1 = dt.get_constructor_is(cns[i]);
for (unsigned j = i + 1; j < cns.size(); ++j) {
@ -234,6 +238,7 @@ namespace sls {
m_axioms.push_back(m.mk_or(m.mk_not(m.mk_app(r1, t)), m.mk_not(m.mk_app(r2, t))));
}
}
#endif
for (auto c : cns) {
auto r = dt.get_constructor_is(c);
auto& acc = *dt.get_constructor_accessors(c);
@ -244,7 +249,7 @@ namespace sls {
}
}
}
collect_path_axioms();
//collect_path_axioms();
TRACE("dt", for (auto a : m_axioms) tout << mk_pp(a, m) << "\n";);
@ -451,6 +456,22 @@ namespace sls {
++m_stats.m_num_occurs;
};
for (auto n : g->nodes()) {
if (!n->is_root())
continue;
euf::enode* con = nullptr;
for (auto sib : euf::enode_class(n)) {
if (dt.is_constructor(sib->get_expr())) {
if (!con)
con = sib;
if (con && con->get_decl() != sib->get_decl()) {
ctx.add_constraint(m.mk_not(m.mk_eq(con->get_expr(), sib->get_expr())));
++m_stats.m_num_occurs;
}
}
}
}
for (auto n : g->nodes()) {
if (!n->is_root())
continue;
@ -548,6 +569,43 @@ namespace sls {
bool datatype_plugin::is_sat() { return true; }
void datatype_plugin::register_term(expr* e) {}
bool datatype_plugin::repair_down(app* e) {
verbose_stream() << "repair-down " << mk_bounded_pp(e, m) << "\n";
return false;
}
void datatype_plugin::repair_up(app* e) {
verbose_stream() << "repair-up " << mk_bounded_pp(e, m) << "\n";
}
expr_ref datatype_plugin::eval1(expr* e) {
auto n = g->find(e)->get_root();
e = n->get_expr();
if (!dt.is_datatype(e))
return ctx.get_value(e);
auto con = get_constructor(n);
if (con) {
expr_ref_vector args(m);
for (auto arg : euf::enode_args(con))
args.push_back(eval0(arg));
return expr_ref(m.mk_app(con->get_decl(), args), m);
}
return eval0(n);
}
expr_ref datatype_plugin::eval0(expr* n) {
if (!dt.is_datatype(n->get_sort()))
return ctx.get_value(n);
if (!m_eval.get(n->get_id(), nullptr))
m_eval[n->get_id()] = m_model->get_some_value(n->get_sort());
return expr_ref(m_eval.get(n->get_id()), m);
}
expr_ref datatype_plugin::eval0(euf::enode* n) {
return eval0(n->get_root()->get_expr());
}
void datatype_plugin::collect_statistics(statistics& st) const {
st.update("sls-dt-axioms", m_axioms.size());

19
src/ast/sls/sls_datatype_plugin.h
View file

@ -39,7 +39,7 @@ namespace sls {
obj_map<expr, vector<parent_t>> m_parents;
mutable datatype_util dt;
expr_ref_vector m_axioms, m_values;
expr_ref_vector m_axioms, m_values, m_eval;
model_ref m_model;
stats m_stats;
@ -54,6 +54,11 @@ namespace sls {
euf::enode* get_constructor(euf::enode* n) const;
expr_ref eval1(expr* e);
expr_ref eval0(euf::enode* n);
expr_ref eval0(expr* n);
public:
datatype_plugin(context& c);
~datatype_plugin() override;
@ -65,17 +70,17 @@ namespace sls {
bool propagate() override;
bool is_sat() override;
void register_term(expr* e) override;
std::ostream& display(std::ostream& out) const override;
bool set_value(expr* e, expr* v) override { return false; }
void repair_up(app* e) override {}
bool repair_down(app* e) override { return false; }
void repair_literal(sat::literal lit) override {}
bool include_func_interp(func_decl* f) const override;
bool repair_down(app* e) override;
void repair_up(app* e) override;
std::ostream& display(std::ostream& out) const override;
void collect_statistics(statistics& st) const override;
void reset_statistics() override;
bool include_func_interp(func_decl* f) const override;
};