hasmtlib 2.6.1 → 2.6.2

raw patch · 5 files changed

+37/−14 lines, 5 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Counting.hs +26/−11
• src/Language/Hasmtlib/Type/Expr.hs +3/−0
• src/Language/Hasmtlib/Type/Relation.hs +2/−2

@@ -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/). +## v2.6.2 _(2024-09-04)_++### Changed+- Functions for enconding cardinality-constraints in `Language.Hasmtlib.Counting` now use specialized encodings for some cardinalities - improving solvers efficiency.+ ## v2.6.1 _(2024-09-02)_  ### Added

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.6.1+version:               2.6.2 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.

@@ -10,7 +10,9 @@  Therefore additional information for the temporal summation may need to be provided. -E.g. if your logic is \"QF_LIA\" you would want @count \@IntSort $ ...@+E.g. if your logic is \"QF_LIA\" you would want @'count'' \@'IntSort' $ ...@++It is worth noting that some cardinality constraints use optimized encodings, such as @'atLeast' 1 ≡ 'or'@. -} module Language.Hasmtlib.Counting (@@ -31,6 +33,7 @@ import Prelude hiding (not, (&&), (||), or) import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Expr+import Language.Hasmtlib.Boolean import Data.Proxy  -- | Wrapper for 'count' which takes a 'Proxy'.@@ -43,17 +46,29 @@ 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) . count-{-# INLINEABLE atMost #-}+-- | 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, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort+atMost (Constant 0) = nand+atMost (Constant 1) = atMostOneLinear+atMost k = (<=? k) . count+{-# INLINE 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+atMostOneLinear :: (Foldable f, Boolean b) => f b -> b+atMostOneLinear xs =+  let (_, sz) = foldr (plus . (, false)) (false, false) xs+   in not sz+  where+    plus (xe, xz) (ye, yz) = (xe || ye, xz || yz || (xe && ye))++-- | 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, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort+atLeast (Constant 0) = const true+atLeast (Constant 1) = or atLeast k = (>=? k) . count-{-# INLINEABLE atLeast #-}+{-# INLINE 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+-- | 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, KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Expr t -> f (Expr BoolSort) -> Expr BoolSort+exactly (Constant 0) = nand exactly k = (=== k) . count-{-# INLINEABLE exactly #-}+{-# INLINE exactly #-}

@@ -737,6 +737,9 @@   xor x (Constant (BoolValue y)) = if y then not x else x   xor x y = Xor x y   {-# INLINE xor #-}+  (Constant (BoolValue False)) ==> _ = true+  x ==> y  = Impl x y+  {-# INLINE (==>) #-}   (<==>) = (===)   {-# INLINE (<==>) #-} 

@@ -203,7 +203,7 @@ -- | Returns a list of 'Expr' 'BoolSort' indicating whether the projection on -- given element \( x \in A \) holds for every element in the codomain: ----- \( \{ (x,y) \in R \mid y \in codomain(B) \} \)+-- \( \{ (x,y) \in R \mid y \in codomain(R) \} \) image :: (Ix a, Ix b) => Relation a b -> a -> [Expr BoolSort] image r x = mapMaybe ((r !?) . (x,)) (codomain r) {-# INLINE image #-}@@ -211,7 +211,7 @@ -- | Returns a list of 'Expr' 'BoolSort' indicating whether the projection on -- given element \( y \in B \) holds for every element in the domain: ----- \( \{ (x,y) \in R \mid x \in domain(A) \} \)+-- \( \{ (x,y) \in R \mid x \in domain(R) \} \) preimage :: (Ix a, Ix b) => Relation a b -> b -> [Expr BoolSort] preimage r y = mapMaybe ((r !?) . (,y)) (domain r) {-# INLINE preimage #-}