what4 1.6.1 → 1.6.2

raw patch · 9 files changed

+19/−16 lines, 9 files

Files

CHANGES.md +4/−0
src/What4/Expr/BoolMap.hs +2/−2
src/What4/Expr/WeightedSum.hs +2/−2
src/What4/Solver/CVC5.hs +0/−1
src/What4/Utils/AnnotatedMap.hs +3/−4
src/What4/Utils/Environment.hs +2/−2
src/What4/Utils/Word16String.hs +4/−2
test/InvariantSynthesis.hs +0/−1
what4.cabal +2/−2

CHANGES.md view

@@ -1,3 +1,7 @@+# 1.6.2 (Sep 2024)++* Allow building with GHC 9.10.+ # 1.6.1 (Sep 2024)  * Fix a bug in which `what4`'s CVC5 adapter would fail to parse models

src/What4/Expr/BoolMap.hs view

@@ -34,7 +34,7 @@  import           Control.Lens (_1, over) import           Data.Hashable-import           Data.List (foldl')+import qualified Data.List as List (foldl') import           Data.List.NonEmpty (NonEmpty(..)) import           Data.Kind (Type) import           Data.Parameterized.Classes@@ -150,7 +150,7 @@ -- | Generate a bool map from a list of terms and polarities by repeatedly --   calling @addVar@. fromVars :: (HashableF f, OrdF f) => [(f BaseBoolType, Polarity)] -> BoolMap f-fromVars = foldl' (\m (x,p) -> addVar x p m) (BoolMap AM.empty)+fromVars = List.foldl' (\m (x,p) -> addVar x p m) (BoolMap AM.empty)  -- | Merge two bool maps, performing resolution as necessary. combine :: OrdF f => BoolMap f -> BoolMap f -> BoolMap f

src/What4/Expr/WeightedSum.hs view

@@ -74,7 +74,7 @@ import qualified Data.BitVector.Sized as BV import           Data.Hashable import           Data.Kind-import           Data.List (foldl')+import qualified Data.List as List (foldl') import           Data.Maybe import           Data.Parameterized.Classes @@ -432,7 +432,7 @@     traverse (_1 (traverseWrap f)) (AM.toList (_prodMap pd))  where   sr = prodRepr pd-  rebuild = foldl' (\m (WrapF t, occ) -> AM.insert (WrapF t) (mkProdNote sr occ t) occ m) AM.empty+  rebuild = List.foldl' (\m (WrapF t, occ) -> AM.insert (WrapF t) (mkProdNote sr occ t) occ m) AM.empty   -- | This returns a variable times a constant.

src/What4/Solver/CVC5.hs view

@@ -35,7 +35,6 @@  import           Control.Monad (forM_, when) import           Data.Bits-import           Data.String import           System.IO import qualified System.IO.Streams as Streams

src/What4/Utils/AnnotatedMap.hs view

@@ -44,7 +44,6 @@  import           Data.Functor.Identity import qualified Data.Foldable as Foldable-import           Data.Foldable (foldl') import           Prelude hiding (null, filter, lookup)  import qualified Data.FingerTree as FT@@ -57,19 +56,19 @@   FT.Measured v a =>   (a -> Bool) -> FT.FingerTree v a -> FT.FingerTree v a filterFingerTree p =-  foldl' (\xs x -> if p x then xs FT.|> x else xs) FT.empty+  Foldable.foldl' (\xs x -> if p x then xs FT.|> x else xs) FT.empty  mapMaybeFingerTree ::   (FT.Measured v2 a2) =>   (a1 -> Maybe a2) -> FT.FingerTree v1 a1 -> FT.FingerTree v2 a2 mapMaybeFingerTree f =-  foldl' (\xs x -> maybe xs (xs FT.|>) (f x)) FT.empty+  Foldable.foldl' (\xs x -> maybe xs (xs FT.|>) (f x)) FT.empty  traverseMaybeFingerTree ::   (Applicative f, FT.Measured v2 a2) =>   (a1 -> f (Maybe a2)) -> FT.FingerTree v1 a1 -> f (FT.FingerTree v2 a2) traverseMaybeFingerTree f =-   foldl' (\m x -> rebuild <$> m <*> f x) (pure FT.empty)+   Foldable.foldl' (\m x -> rebuild <$> m <*> f x) (pure FT.empty)  where  rebuild ys Nothing  = ys  rebuild ys (Just y) = ys FT.|> y

src/What4/Utils/Environment.hs view

@@ -24,7 +24,7 @@  import Control.Monad.IO.Class import Data.Char-import Data.List (foldl')+import qualified Data.List as List (foldl') import Data.Map (Map) import qualified Data.Map as Map import qualified System.Directory as Sys@@ -81,7 +81,7 @@   let init_map = Map.fromList [ ("MSS_BINPATH", prog_path) ]   -- Extend init_map with environment variables.   env <- getEnvironment-  let expanded_map = foldl' (\m (k,v) -> Map.insert k v m) init_map env+  let expanded_map = List.foldl' (\m (k,v) -> Map.insert k v m) init_map env   -- Return expanded path.   expandVars (Map.union base_map expanded_map) path

src/What4/Utils/Word16String.hs view

@@ -20,7 +20,9 @@ , take , append , length-, foldl'+-- Qualify this name to disambiguate it from the Prelude version of foldl'+-- (defined in base-4.20 or later).+, What4.Utils.Word16String.foldl' , findSubstring , isInfixOf , isPrefixOf@@ -91,7 +93,7 @@ --   where the 16bit words are encoded as two bytes --   in little-endian order. -----   PRECONDITION: the input bytestring must +--   PRECONDITION: the input bytestring must --   have a length which is a multiple of 2. fromLEByteString :: ByteString -> Word16String fromLEByteString xs

test/InvariantSynthesis.hs view

@@ -13,7 +13,6 @@ import           Data.Maybe import           System.Environment -import qualified Data.BitVector.Sized as BV import           Data.Parameterized.Context import           Data.Parameterized.Map (MapF) import           Data.Parameterized.Nonce

what4.cabal view

@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name:          what4-Version:       1.6.1+Version:       1.6.2 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com Copyright:     (c) Galois, Inc 2014-2023@@ -9,7 +9,7 @@ Build-type:    Simple Homepage:      https://github.com/GaloisInc/what4 Bug-reports:   https://github.com/GaloisInc/what4/issues-Tested-with:   GHC==8.6.5, GHC==8.8.4, GHC==8.10.7, GHC==9.0.2+Tested-with:   GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.4, GHC==9.6.2, GHC==9.8.1, GHC==9.10.1 Category:      Formal Methods, Theorem Provers, Symbolic Computation, SMT Synopsis:      Solver-agnostic symbolic values support for issuing queries Description: