hasmtlib 1.3.0 → 1.3.1

raw patch · 3 files changed

+18/−4 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

+ Language.Hasmtlib.Counting: count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t

+ Language.Hasmtlib.Counting: count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t

- Language.Hasmtlib.Type.Solution: solVal :: forall t_aHq7. Lens' (SMTVarSol t_aHq7) (Value t_aHq7)

+ Language.Hasmtlib.Type.Solution: solVal :: forall t_aHrb. Lens' (SMTVarSol t_aHrb) (Value t_aHrb)

- Language.Hasmtlib.Type.Solution: solVar :: forall t_aHq7. Lens' (SMTVarSol t_aHq7) (SMTVar t_aHq7)

+ Language.Hasmtlib.Type.Solution: solVar :: forall t_aHrb. Lens' (SMTVarSol t_aHrb) (SMTVar t_aHrb)

Files

CHANGELOG.md +5/−0
hasmtlib.cabal +1/−1
src/Language/Hasmtlib/Counting.hs +12/−3

CHANGELOG.md view

@@ -6,6 +6,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [PVP versioning](https://pvp.haskell.org/). +## v1.3.1 _(2024-07-12)_++### Added+- Added `count` in `Language.Hasmtlib.Counting`+ ## v1.3.0 _(2024-07-12)_  ### Added

hasmtlib.cabal view

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               1.3.0+version:               1.3.1 synopsis:              A monad for interfacing with external SMT solvers description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.

src/Language/Hasmtlib/Counting.hs view

@@ -6,18 +6,27 @@ import Language.Hasmtlib.Equatable import Language.Hasmtlib.Orderable import Language.Hasmtlib.Iteable+import Data.Proxy +count' :: forall t f. (Functor f, Foldable f, Num (Expr t)) => Proxy t -> f (Expr BoolSort) -> Expr t+count' _ = sum . fmap (\b -> ite b 1 0)+{-# INLINEABLE count' #-}++count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t+count = count' (Proxy @t)+{-# INLINE count #-}+ -- | Out of many bool-expressions build a formula which encodes that __at most__ 'k' of them are 'true' atMost  :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort-atMost  k = (<=? k) . sum . fmap (\b -> ite b 1 0)+atMost  k = (<=? k) . count {-# INLINEABLE atMost #-}  -- | Out of many bool-expressions build a formula which encodes that __at least__ 'k' of them are 'true' atLeast :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort-atLeast k = (>=? k) . sum . fmap (\b -> ite b 1 0)+atLeast k = (>=? k) . count {-# INLINEABLE atLeast #-}  -- | Out of many bool-expressions build a formula which encodes that __exactly__ 'k' of them are 'true' exactly :: forall t f. (Functor f, Foldable f, Num (Expr t), Orderable (Expr t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort-exactly k = (=== k) . sum . fmap (\b -> ite b 1 0)+exactly k = (=== k) . count {-# INLINEABLE exactly #-}