From b54beca037d652a366bec09676c6159ebff048ef Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 28 Jun 2023 10:26:39 +0200 Subject: [PATCH] clarify --- src/math/polysat/slicing.cpp | 4 +++- src/math/polysat/slicing.h | 3 ++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/math/polysat/slicing.cpp b/src/math/polysat/slicing.cpp index a76d4cb80..b462e2ac1 100644 --- a/src/math/polysat/slicing.cpp +++ b/src/math/polysat/slicing.cpp @@ -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 // r0 r1 r2 r4 r3 diff --git a/src/math/polysat/slicing.h b/src/math/polysat/slicing.h index 5aa074a8c..3c426d998 100644 --- a/src/math/polysat/slicing.h +++ b/src/math/polysat/slicing.h @@ -133,7 +133,8 @@ namespace polysat { // Returns true if merge succeeded without conflict. [[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 //