hasmtlib 1.2.0 → 1.3.0

raw patch · 5 files changed

+37/−5 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• README.md +5/−4
• hasmtlib.cabal +2/−1
• src/Language/Hasmtlib.hs +2/−0
• src/Language/Hasmtlib/Counting.hs +23/−0

@@ -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.0 _(2024-07-12)_++### Added+- Added cardinality constraints with `Language.Hasmtlib.Counting`+ ## v1.2.0 _(2024-07-11)_  ### Added

@@ -62,7 +62,7 @@   ```haskell     data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort     data Expr (t :: SMTSort) where ...-  +     ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t   ``` - [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec & Array@@ -76,7 +76,7 @@       setLogic "QF_BV"       x <- var @(BvSort 16)       y <- var-      assert $ x - (maxBound `mod` 8) === y * y +      assert $ x - (maxBound `mod` 8) === y * y       return (x,y)   ``` - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)@@ -87,14 +87,15 @@ - [x] Solvers via external processes: CVC5, Z3, Yices2-SMT & MathSAT   ```haskell     (result, solution) <- solveWith (solver mathsat) $ do-      setLogic "QF_LIA" +      setLogic "QF_LIA"       assert $ ...   ``` - [x] Incremental solving   ```haskell       cvc5Living <- interactiveSolver cvc5       interactiveWith cvc5Living $ do-        setLogic "QF_LIA"    +        setLogic "QF_LIA"+        setOption $ Incremental True         setOption $ ProduceModels True         x <- var @IntSort         assert $ x === 42

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               1.2.0+version:               1.3.0 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.@@ -30,6 +30,7 @@                      , Language.Hasmtlib.Iteable                      , Language.Hasmtlib.Boolean                      , Language.Hasmtlib.Variable+                     , Language.Hasmtlib.Counting                      , Language.Hasmtlib.Equatable                      , Language.Hasmtlib.Orderable                      , Language.Hasmtlib.Integraled

@@ -14,6 +14,7 @@   , module Language.Hasmtlib.Equatable   , module Language.Hasmtlib.Orderable   , module Language.Hasmtlib.Codec+  , module Language.Hasmtlib.Counting   , module Language.Hasmtlib.Variable   , module Language.Hasmtlib.Solver.Common   , module Language.Hasmtlib.Solver.CVC5@@ -37,6 +38,7 @@ import Language.Hasmtlib.Equatable import Language.Hasmtlib.Orderable import Language.Hasmtlib.Codec+import Language.Hasmtlib.Counting import Language.Hasmtlib.Variable import Language.Hasmtlib.Solver.Common import Language.Hasmtlib.Solver.CVC5

@@ -0,0 +1,23 @@+module Language.Hasmtlib.Counting where++import Prelude hiding (not, (&&), (||), or)+import Language.Hasmtlib.Internal.Expr.Num ()+import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Equatable+import Language.Hasmtlib.Orderable+import Language.Hasmtlib.Iteable++-- | 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)+{-# 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)+{-# 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)+{-# INLINEABLE exactly #-}