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

slicing: explain

Browse source
This commit is contained in:
Jakob Rath 2023-06-28 10:23:55 +02:00
parent 3a7cdc36d6
commit 9e7a392e21
1 changed files with 26 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -199,8 +199,33 @@ namespace polysat {
}
void slicing::explain(slice x, slice y, dep_vector& out_deps) {
// /-> ...
// x -> x1 -> x2 -> lca <- y1 <- y
// r0 r1 r2 r4 r3
SASSERT_EQ(find(x), find(y));
NOT_IMPLEMENTED_YET();
begin_mark();
// mark ancestors of x in the proof forest
slice s = x;
while (s != null_slice) {
mark(s);
s = m_proof_parent[s];
}
// find lowest common ancestor of x and y
// and collect deps from y to lca
slice lca = y;
while (!is_marked(lca)) {
out_deps.push_back(m_proof_reason[lca]);
lca = m_proof_parent[lca];
SASSERT(lca != null_slice);
}
// collect deps from x to lca
s = x;
while (s != lca) {
out_deps.push_back(m_proof_reason[s]);
s = m_proof_parent[s];
SASSERT(s != null_slice);
}
end_mark();
}
bool slicing::merge(slice_vector& xs, slice_vector& ys, dep_t dep) {