From 3796770e4693ed0c691a390be51c9fcd27367c48 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 23 Mar 2023 14:36:38 +0100 Subject: [PATCH] Fix subsumption (need to check whether entry is valid) --- src/math/polysat/simplify_clause.cpp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp index e061dc398..d8a86cae7 100644 --- a/src/math/polysat/simplify_clause.cpp +++ b/src/math/polysat/simplify_clause.cpp @@ -342,19 +342,17 @@ namespace polysat { return false; unsigned j = 0; for (unsigned i = 0; i < cl.size(); ++i) - if (!m_entries[i].subsuming) + if (!m_entries[i].valid || !m_entries[i].subsuming) cl[j++] = cl[i]; cl.m_literals.shrink(j); return true; } - // decomposes into a plain constant and a part containing variables. e.g., 2*x*y + 3*z - 2 gets { 2*x*y + 3*z, -2 } - static std::pair decouple_constant(const pdd& p) { - for (const auto& m : p) { - if (m.vars.empty()) - return { p - m.coeff, p.manager().mk_val(m.coeff) }; - } - return { p, p.manager().mk_val(0) }; + // decomposes into a plain constant and a part containing variables. e.g., 2*x*y + 3*z - 2 becomes { 2*x*y + 3*z, -2 } + static std::pair decouple_constant(pdd const& p) { + auto& m = p.manager(); + rational offset = p.offset(); + return { p - offset, m.mk_val(offset) }; } // 2^(k - d) * x = m * 2^(k - d) @@ -549,6 +547,7 @@ namespace polysat { * More generally: parity can be replaced by lsb in case we check for subsumption between the bit-masks rather than comparing the parities (special case) */ bool simplify_clause::try_bit_subsumptions(clause& cl) { + LOG_H2("Try bit subsumptions: " << cl); struct pdd_info { unsigned sz;