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

clarify

Browse source
This commit is contained in:
Jakob Rath 2023-06-28 10:26:39 +02:00
parent 92192144b1
commit b54beca037
2 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -198,7 +198,9 @@ namespace polysat {
} }
} }
void slicing::explain(slice x, slice y, dep_vector& out_deps) { void slicing::explain_base(slice x, slice y, dep_vector& out_deps) {
SASSERT(!has_sub(x));
SASSERT(!has_sub(y));
// /-> ... // /-> ...
// x -> x1 -> x2 -> lca <- y1 <- y // x -> x1 -> x2 -> lca <- y1 <- y
// r0 r1 r2 r4 r3 // r0 r1 r2 r4 r3

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

@ -133,7 +133,8 @@ namespace polysat {
// Returns true if merge succeeded without conflict. // Returns true if merge succeeded without conflict.
[[nodiscard]] bool merge_base(slice s1, slice s2, dep_t dep); [[nodiscard]] bool merge_base(slice s1, slice s2, dep_t dep);
void explain(slice x, slice y, dep_vector& out_deps); // Extract reason for equality of base slices
void explain_base(slice x, slice y, dep_vector& out_deps);
// Merge equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k // Merge equality x_1 ++ ... ++ x_n == y_1 ++ ... ++ y_k
// //