From 0888f92efd4bfb8aae3a1b60285fd7cd245e397b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Sep 2022 08:53:00 -0700 Subject: [PATCH] remove 'change' just return Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict.cpp | 2 ++ src/math/polysat/simplify_clause.cpp | 8 ++++---- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp index ec72b5bfd..bf358df01 100644 --- a/src/math/polysat/conflict.cpp +++ b/src/math/polysat/conflict.cpp @@ -157,6 +157,8 @@ namespace polysat { UNREACHABLE(); // we don't follow the regular loop when backjumping return false; } + UNREACHABLE(); + return false; } bool conflict::is_relevant(sat::literal lit) const { diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp index dbdaf6833..41bbeeb3e 100644 --- a/src/math/polysat/simplify_clause.cpp +++ b/src/math/polysat/simplify_clause.cpp @@ -22,10 +22,9 @@ namespace polysat { {} bool simplify_clause::apply(clause& cl) { - bool changed = false; - if (try_unilinear_subsumption(cl)) - changed = true; - return changed; + if (try_constant_subsumptions(cl)) + return true; + return false; } pdd simplify_clause::abstract(pdd const& p, pdd& v) { @@ -80,6 +79,7 @@ namespace polysat { entry.valid = true; } + /** * Test simple subsumption between univariate and linear literals, i.e., * the case where both literals can be represented by a single contiguous forbidden interval.