From 561e8a14aa0ac007afbca1aa50d8a99ac3e27de7 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 4 Dec 2019 17:03:21 -0800 Subject: [PATCH] Make truncation-of-weighted-sum rewrite rule more conservative. Instead of modifying coefficients in a weighted sum, we now restrict ourselves to zeroing out coefficients that are equivalent to zero modulo 2^n. Fixes #362. --- what4/src/What4/Expr/Builder.hs | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 3baec2b51..775596e22 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -4734,8 +4734,8 @@ instance IsExprBuilder (ExprBuilder t st fs) where Just Refl <- return $ testEquality (addNat n1 n2) n bvConcat sb a' b' - -- Truncate a weighted sum: truncate all the integer coefficients - -- and remove terms with coefficients that become zero + -- Truncate a weighted sum: Remove terms with coefficients that + -- would become zero after truncation. -- -- Truncation of w-bit words down to n bits respects congruence -- modulo 2^n. Furthermore, w-bit addition and multiplication also @@ -4754,7 +4754,9 @@ instance IsExprBuilder (ExprBuilder t st fs) where , SR.SemiRingBVRepr SR.BVArithRepr _w <- WSum.sumRepr s , Just Refl <- testEquality idx (knownNat :: NatRepr 0) = do let mask = maxUnsigned n - let reduce i = let j = i Bits..&. mask in writer (j, Any (i /= j)) + let reduce i + | i Bits..&. mask == 0 = writer (0, Any True) + | otherwise = writer (i, Any False) let (s', Any changed) = runWriter $ WSum.traverseCoeffs reduce s x' <- if changed then sbMakeExpr sb (SemiRingSum s') else return x sbMakeExpr sb $ BVSelect idx n x'