From 2beb63554c66f48859b44923783594ed2a80cf19 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 12 Nov 2019 21:55:30 -0800 Subject: [PATCH] Add special case to `bvSelect` for truncating a WeightedSum of bitvectors. Truncating a WeightedSum of bitvectors now truncates all the integer coefficients in the weighted sum, removing those that reduce to 0. This is useful for simplifying e.g. alignment constraints. Fixes GaloisInc/saw-script#586. --- what4/src/What4/Expr/Builder.hs | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs index 742f0bb7..5e26b0ff 100644 --- a/what4/src/What4/Expr/Builder.hs +++ b/what4/src/What4/Expr/Builder.hs @@ -162,6 +162,7 @@ import Control.Lens hiding (asIndex, (:>), Empty) import Control.Monad import Control.Monad.IO.Class import Control.Monad.ST +import Control.Monad.Trans.Writer.CPS (writer, runWriter) import Data.Bimap (Bimap) import qualified Data.Bimap as Bimap import qualified Data.Binary.IEEE754 as IEEE754 @@ -176,6 +177,7 @@ import Data.List.NonEmpty (NonEmpty(..)) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe +import Data.Monoid (Any(..)) import Data.Parameterized.Classes import Data.Parameterized.Context as Ctx import qualified Data.Parameterized.HashTable as PH @@ -4639,6 +4641,16 @@ instance IsExprBuilder (ExprBuilder t st fs) where Just Refl <- return $ testEquality (addNat n1 n2) n bvConcat sb a' b' + -- Truncate a weighted sum: remove terms with coefficients that become zero + | Just (SemiRingSum s) <- asApp x + , SR.SemiRingBVRepr SR.BVArithRepr _w <- WSum.sumRepr s + , Just Refl <- testEquality idx (knownNat :: NatRepr 0) = + do let mask = maxUnsigned n + let reduce i = writer (i Bits..&. mask, Any (i > mask)) + 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' + {- Avoid doing work that may lose sharing... -- Select from a weighted XOR: push down through the sum