From e711808d3e76d88bd027de71423f3f70eee000f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Oct 2022 20:04:21 +0200 Subject: [PATCH] throttle on degree bounds Signed-off-by: Nikolaj Bjorner --- src/math/polysat/explain.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/math/polysat/explain.cpp b/src/math/polysat/explain.cpp index d68456b2b..44039e4c0 100644 --- a/src/math/polysat/explain.cpp +++ b/src/math/polysat/explain.cpp @@ -41,15 +41,22 @@ namespace polysat { LOG("c2: " << c2); pdd a = c1.eq(); pdd b = c2.eq(); + unsigned degree_a = a.degree(); + unsigned degree_b = b.degree(); pdd r = a; if (!a.resolve(v, b, r) && !b.resolve(v, a, r)) return {}; + unsigned degree_r = r.degree(); + if (degree_a < degree_r && degree_b < degree_r) + return {}; // Only keep result if the degree in c2 was reduced. // (this condition might be too strict, but we use it for now to prevent looping) // TODO: check total degree; only keep if total degree smaller or equal. // can always do this if c1 is linear. if (b.degree(v) <= r.degree(v)) return {}; + if (a.degree(v) <= r.degree(v)) + return {}; signed_constraint c = s.eq(r); LOG("resolved: " << c << " currently false? " << c.is_currently_false(s)); if (!c.is_currently_false(s))