From 2da3261d8a28ce3d3016812419f70831f50a60a4 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 29 Jan 2024 17:07:17 +0100 Subject: [PATCH] make lemma sound --- src/sat/smt/polysat/monomials.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/polysat/monomials.cpp b/src/sat/smt/polysat/monomials.cpp index e292eb3fa..2d0f040f1 100644 --- a/src/sat/smt/polysat/monomials.cpp +++ b/src/sat/smt/polysat/monomials.cpp @@ -172,6 +172,9 @@ namespace polysat { } // p * q = p => q = 1 or p = 0 + // + // In general not true, because there exist a, b >= 2 with a * b = 0; then (a+1) * b = b. + // For now, add no-overflow condition on p*q. bool monomials::mul1_inverse(monomial const& mon) { for (unsigned j = mon.size(); j-- > 0; ) { auto const& arg_val = mon.arg_vals[j]; @@ -181,7 +184,7 @@ namespace polysat { for (unsigned k = mon.size(); k-- > 0; ) if (k != j) qs *= mon.args[k]; - c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), C.eq(qs, 1), C.eq(p) }, true); + c.add_axiom("p * q = p => q = 1 or p = 0", { ~C.eq(mon.var, p), ~C.umul_ovfl(p, qs), C.eq(qs, 1), C.eq(p) }, true); return true; } }