mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

move callback into member function

Browse source
This commit is contained in:
Jakob Rath 2023-07-19 12:51:35 +02:00
parent b67caf5fc3
commit 114e7b73e5
3 changed files with 26 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/math/polysat/slicing.cpp
View file

@ -106,27 +106,7 @@ namespace polysat {
reg_decl_plugins(m_ast);
m_bv = alloc(bv_util, m_ast);
m_egraph.set_display_justification(display_dep);
std::function<void(enode* lit, enode* ante)> propagate_negation = [&](enode* lit, enode* ante) {
// LOG("lit: " << lit->get_id() << " value=" << lit->value());
// if (ante)
// LOG("ante: " << ante->get_id() << " value=" << ante->value());
// else
// LOG("ante: <null>");
// LOG(m_egraph);
// ante may be set when symmetric equality is added by congruence
if (ante)
return;
// on_propagate may be called before set_value
if (lit->value() == l_undef)
return;
SASSERT(lit->is_equality());
SASSERT_EQ(lit->value(), l_false);
SASSERT(lit->get_lit_justification().is_external());
// LOG("lit: id=" << lit->get_id() << " value=" << lit->value() << " dep=" << decode_dep(lit->get_lit_justification().ext<void>()));
m_disequality_conflict = lit;
};
m_egraph.set_on_propagate(propagate_negation);
m_egraph.set_on_propagate([&](enode* lit, enode* ante) { egraph_on_propagate(lit, ante); });
}
slicing::slice_info& slicing::info(euf::enode* n) {
@ -520,6 +500,19 @@ namespace polysat {
end_explain();
}
void slicing::egraph_on_propagate(enode* lit, enode* ante) {
// ante may be set when symmetric equality is added by congruence
if (ante)
return;
// on_propagate may be called before set_value
if (lit->value() == l_undef)
return;
SASSERT(lit->is_equality());
SASSERT_EQ(lit->value(), l_false);
SASSERT(lit->get_lit_justification().is_external());
m_disequality_conflict = lit;
}
bool slicing::can_propagate() const {
return !m_needs_congruence.empty() || m_egraph.can_propagate();
}

2
src/math/polysat/slicing.h
View file

@ -168,6 +168,8 @@ namespace polysat {
// (i.e., x and y have the same base, but are not necessarily in the same equivalence class)
void explain_equal(enode* x, enode* y, sat::literal_vector& out_lits, unsigned_vector& out_vars);
void egraph_on_propagate(enode* lit, enode* ante);
// Merge equivalence classes of two base slices.
// Returns true if merge succeeded without conflict.
[[nodiscard]] bool merge_base(enode* s1, enode* s2, dep_t dep);