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

explain_fixed is currently just explain_value for a slice

Browse source
This commit is contained in:
Jakob Rath 2023-08-08 17:26:52 +02:00
parent 6eb81fbb9d
commit f9cbee3b3d
2 changed files with 12 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -781,17 +781,15 @@ namespace polysat {
return cb.build(); return cb.build();
} }
void slicing::explain_value(pvar v, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) { void slicing::explain_value(enode* s, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
SASSERT(m_solver.m_justification[v].is_propagation_by_slicing());
SASSERT(invariant()); SASSERT(invariant());
SASSERT(m_marked_lits.empty()); SASSERT(m_marked_lits.empty());
enode* sv = var2slice(v); enode* r = s->get_root();
enode* rv = sv->get_root(); SASSERT(is_value(r)); // by convention, value slices are always the root; and this method may only be called if s is equivalent to a value node.
SASSERT(is_value(rv)); // by convention, value slices are always the root; and this method may only be called if v is equivalent to a value in the egraph.
SASSERT(m_tmp_deps.empty()); SASSERT(m_tmp_deps.empty());
explain_equal(sv, rv, m_tmp_deps); explain_equal(s, r, m_tmp_deps);
for (void* dp : m_tmp_deps) { for (void* dp : m_tmp_deps) {
dep_t const d = dep_t::decode(dp); dep_t const d = dep_t::decode(dp);
@ -810,6 +808,10 @@ namespace polysat {
m_tmp_deps.reset(); m_tmp_deps.reset();
} }
void slicing::explain_value(pvar v, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
explain_value(var2slice(v), on_lit, on_var);
}
bool slicing::find_range_in_ancestor(enode* s, enode* a, unsigned& out_hi, unsigned& out_lo) { bool slicing::find_range_in_ancestor(enode* s, enode* a, unsigned& out_hi, unsigned& out_lo) {
out_hi = width(s) - 1; out_hi = width(s) - 1;
out_lo = 0; out_lo = 0;
@ -1380,9 +1382,7 @@ namespace polysat {
} }
void slicing::explain_fixed(euf::enode* const n, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) { void slicing::explain_fixed(euf::enode* const n, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var) {
enode* const r = n->get_root(); explain_value(n, on_lit, on_var);
SASSERT(is_value(r));
NOT_IMPLEMENTED_YET(); // TODO: like explain_value
} }
std::ostream& slicing::display(std::ostream& out) const { std::ostream& slicing::display(std::ostream& out) const {

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

@ -184,6 +184,9 @@ namespace polysat {
// (i.e., x and y have the same base, but are not necessarily in the same equivalence class) // (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, ptr_vector<void>& out_deps); void explain_equal(enode* x, enode* y, ptr_vector<void>& out_deps);
/** Explain why slice is equivalent to a value */
void explain_value(enode* s, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
/** Extract reason for conflict */ /** Extract reason for conflict */
void explain(ptr_vector<void>& out_deps); void explain(ptr_vector<void>& out_deps);