mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fx

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-12 12:19:55 -07:00
parent 766b9df4e2
commit 1765141261
2 changed files with 19 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/euf/euf_egraph.cpp
View file

@ -205,6 +205,7 @@ namespace euf {
} }
void egraph::new_diseq(enode* n, void* reason) { void egraph::new_diseq(enode* n, void* reason) {
force_push();
SASSERT(m.is_eq(n->get_expr())); SASSERT(m.is_eq(n->get_expr()));
auto j = justification::external(reason); auto j = justification::external(reason);
auto a = n->get_arg(0), b = n->get_arg(1); auto a = n->get_arg(0), b = n->get_arg(1);

26
src/ast/sls/sls_euf_plugin.cpp
View file

@ -45,6 +45,10 @@ namespace sls {
void euf_plugin::start_propagation() { void euf_plugin::start_propagation() {
m_g = alloc(euf::egraph, m); m_g = alloc(euf::egraph, m);
std::function<void(std::ostream&, void*)> dj = [&](std::ostream& out, void* j) {
out << "lit " << to_literal(reinterpret_cast<size_t*>(j));
};
m_g->set_display_justification(dj);
init_egraph(*m_g, !m_incremental); init_egraph(*m_g, !m_incremental);
} }
@ -87,22 +91,30 @@ namespace sls {
return; return;
++m_stats.m_num_conflicts; ++m_stats.m_num_conflicts;
unsigned n = 1; unsigned n = 0;
sat::literal_vector lits; sat::literal_vector lits;
sat::literal flit = sat::null_literal, slit; sat::literal flit = sat::null_literal, slit;
ptr_vector<size_t> explain; ptr_vector<size_t> explain;
g.begin_explain(); g.begin_explain();
g.explain<size_t>(explain, nullptr); g.explain<size_t>(explain, nullptr);
g.end_explain(); g.end_explain();
TRACE("enf",
for (auto p : explain) {
sat::literal l = to_literal(p);
tout << l << " " << mk_pp(ctx.atom(l.var()), m) << " " << ctx.is_unit(l) << "\n";
});
for (auto p : explain) { for (auto p : explain) {
sat::literal l = to_literal(p); sat::literal l = to_literal(p);
CTRACE("euf", !ctx.is_true(l), tout << "not true " << l << "\n"; ctx.display(tout););
SASSERT(ctx.is_true(l)); SASSERT(ctx.is_true(l));
lits.push_back(~l);
if (ctx.is_unit(l)) if (ctx.is_unit(l))
continue; continue;
lits.push_back(~l);
if (ctx.rand(++n) == 0) if (ctx.rand(++n) == 0)
flit = l; flit = l;
} }
//verbose_stream() << "conflict: " << lits << " flip " << flit << "\n";
ctx.add_clause(lits); ctx.add_clause(lits);
if (flit == sat::null_literal) if (flit == sat::null_literal)
return; return;
@ -139,16 +151,14 @@ namespace sls {
if (!e) if (!e)
return; return;
TRACE("euf", tout << "propagate " << lit << "\n");
m_stack.push_back(lit); m_stack.push_back(lit);
g.push(); g.push();
if (m.is_eq(e, x, y)) { if (m.is_eq(e, x, y)) {
if (lit.sign()) if (lit.sign())
g.new_diseq(g.find(e), to_ptr(lit)); g.new_diseq(g.find(e), to_ptr(lit));
else { else
auto a = g.find(x); g.merge(g.find(x), g.find(y), to_ptr(lit));
auto b = g.find(y);
g.merge(a, b, to_ptr(lit));
}
// g.merge(g.find(e), g.find(!lit.sign()), to_ptr(lit)); // g.merge(g.find(e), g.find(!lit.sign()), to_ptr(lit));
} }
@ -160,7 +170,7 @@ namespace sls {
auto b = to_app(e)->get_arg(j); auto b = to_app(e)->get_arg(j);
expr_ref eq(m.mk_eq(a, b), m); expr_ref eq(m.mk_eq(a, b), m);
auto c = g.find(eq); auto c = g.find(eq);
if (!g.find(eq)) { if (!c) {
euf::enode* args[2] = { g.find(a), g.find(b) }; euf::enode* args[2] = { g.find(a), g.find(b) };
c = g.mk(eq, 0, 2, args); c = g.mk(eq, 0, 2, args);
} }