Merge pull request #94 from bruderj15/develop

Puiblish v2.6.1

CHANGELOG.md

@@ -6,6 +6,12 @@ file.
 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.1 _(2024-09-02)_
+
+### Added
+- Added module 'Language.Hasmtlib.Type.Relation' for encoding binary relations
+- Added rich documentation and usage examples for all public modules
+
 ## v2.6.0 _(2024-08-27)_
 
 ### Added

README.md

@@ -2,7 +2,7 @@
 
 # Hasmtlib - Haskell SMTLib MTL Library
 
-Hasmtlib is a library for generating SMTLib2-problems using a monad.
+Hasmtlib is a library with high-level-abstraction 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.
 It is highly inspired by [ekmett/ersatz](https://github.com/ekmett/ersatz) which does the same for QSAT. Communication with external solvers is handled by [tweag/smtlib-backends](https://github.com/tweag/smtlib-backends).
 
@@ -57,7 +57,7 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
 
 ## Features
 
-- [x] SMTLib2-Sorts in the Haskell-Type
+- [x] SMTLib2-Sorts in the Haskell-Type to guarantee well-typed expressions
   ```haskell
     data SMTSort =
         BoolSort
@@ -72,43 +72,10 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
   ```
 - [x] Full SMTLib 2.6 standard support for Sorts Bool, Int, Real, BitVec, Array & String
 - [x] Type-level length-indexed Bitvectors with type-level encoding (Signed/Unsigned) for BitVec
-  ```haskell
-  bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
-  bvLShR :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort enc n) -> Expr (BvSort Unsigned n)
-  bvAShR :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort enc n) -> Expr (BvSort Signed n)
-  ```
 - [x] Pure API with plenty common instances: `Num`, `Floating`, `Bounded`, `Bits`, `Ixed` and many more
-  ```haskell
-    solveWith @SMT (solver yices) $ do
-      setLogic "QF_BV"
-      x <- var @(BvSort Signed 16)
-      let f = x >? 42 && (x `div` 84 === maxBound - 100)
-      assert f
-      return x
-  ```
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)
-  ```haskell
-    -- | Function that turns a state (usually SMT or OMT) into a result and a solution
-    type Solver s m = s -> m (Result, Solution)
-  ```
 - [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla
-- [x] Incremental solving
-  ```haskell
-      cvc5Living <- interactiveSolver cvc5
-      interactiveWith @Pipe cvc5Living $ do
-        setLogic "QF_LIA"
-        setOption $ Incremental True
-        setOption $ ProduceModels True
-        x <- var @IntSort
-        assert $ x === 42
-        result <- checkSat
-        push
-        assert $ x <? 0
-        (result, solution) <- solve
-        case result of
-          Sat   -> return solution
-          Unsat -> pop >> ...
-  ```
+- [x] Support for incremental solving
 - [x] Pure quantifiers `for_all` and `exists`
   ```haskell
     solveWith @SMT (solver z3) $ do
@@ -134,6 +101,30 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
       return x
   ```
 
+## Related work
+- [ekmett/ersatz](https://hackage.haskell.org/package/ersatz):
+Huge inspiration for this library (some code stolen).
+We do for `SMT` what they do for `SAT`.
+- [hgoes/smtlib2](https://hackage.haskell.org/package/smtlib2):
+Their eDSL is highly expressive and focuses on well-typed SMT-expressions.
+But their approach is a little verbose and makes usage feel quite heavy.
+Their eDSL is also entirely monadic and therefore formula construction is painful.
+- [yav/simple-smt](https://hackage.haskell.org/package/simple-smt):
+They are lightweight but their types are weak and their API is barely embedded into Haskell.
+- [LevantErkok/sbv](https://hackage.haskell.org/package/sbv):
+While they "express properties about Haskell programs and automatically prove them using SMT",
+we instead use Haskell to simplify the encoding of SMT-Problems.
+They can do a whole lot (C-Code-Gen, Crypto-Stuff,...), which is cool, but adds weight.
+
+If you want highly specific implementations for different solvers, all their individual configurations and swallow the awkward typing,
+then use [hgoes/smtlib2](https://hackage.haskell.org/package/smtlib2).
+
+If you want to express properties about Haskell programs and automatically prove them using SMT,
+then use [LevantErkok/sbv](https://hackage.haskell.org/package/sbv).
+
+If you want to encode SMT-problems as lightweight and close to Haskell as possible, then use this library.
+I personally use it for scheduling/resource-allocation-problems.
+
 ## Examples
 There are some examples in [here](https://github.com/bruderj15/Hasmtlib/tree/master/src/Language/Hasmtlib/Example).
 

hasmtlib.cabal

@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.6.0
+version:               2.6.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.
@@ -56,8 +56,10 @@ library
                      , Language.Hasmtlib.Type.Option
                      , Language.Hasmtlib.Type.ArrayMap
                      , Language.Hasmtlib.Type.Bitvec
+                     , Language.Hasmtlib.Type.Relation
 
-  build-depends:       attoparsec                   >= 0.14.4 && < 1
+  build-depends:       array                        >= 0.5    && < 1
+                     , attoparsec                   >= 0.14.4 && < 1
                      , base                         >= 4.17.2 && < 5
                      , bytestring                   >= 0.11.5 && < 1
                      , containers                   >= 0.6.7  && < 1

src/Language/Hasmtlib.hs

@@ -1,28 +1,49 @@
 module Language.Hasmtlib
   (
-    module Language.Hasmtlib.Type.MonadSMT
+    -- * Type
+    -- ** Expr
+    module Language.Hasmtlib.Type.SMTSort
+  , module Language.Hasmtlib.Type.Value
+  , module Language.Hasmtlib.Type.Expr
+
+    -- ** Containers
+  , module Language.Hasmtlib.Type.Bitvec
+  , module Language.Hasmtlib.Type.ArrayMap
+  , module Language.Hasmtlib.Type.Relation
+
+    -- ** SMT
+  , module Language.Hasmtlib.Type.MonadSMT
   , module Language.Hasmtlib.Type.SMT
+  , module Language.Hasmtlib.Type.Option
+
+  -- ** OMT
   , module Language.Hasmtlib.Type.OMT
+
+  -- ** Pipe
   , module Language.Hasmtlib.Type.Pipe
-  , module Language.Hasmtlib.Type.Expr
-  , module Language.Hasmtlib.Type.Value
-  , module Language.Hasmtlib.Type.Solver
-  , module Language.Hasmtlib.Type.Option
-  , module Language.Hasmtlib.Type.SMTSort
-  , module Language.Hasmtlib.Type.Solution
-  , module Language.Hasmtlib.Type.ArrayMap
-  , module Language.Hasmtlib.Type.Bitvec
-  , module Language.Hasmtlib.Boolean
+
+  -- * Class
   , module Language.Hasmtlib.Codec
+  , module Language.Hasmtlib.Boolean
   , module Language.Hasmtlib.Counting
   , module Language.Hasmtlib.Variable
+
+  -- * Solver
+  -- ** Type
+  , module Language.Hasmtlib.Type.Solution
+  , module Language.Hasmtlib.Type.Solver
   , module Language.Hasmtlib.Solver.Common
-  , module Language.Hasmtlib.Solver.Bitwuzla
-  , module Language.Hasmtlib.Solver.CVC5
+
+  -- ** Concrete solvers
   , module Language.Hasmtlib.Solver.Z3
+  , module Language.Hasmtlib.Solver.CVC5
   , module Language.Hasmtlib.Solver.Yices
   , module Language.Hasmtlib.Solver.OpenSMT
   , module Language.Hasmtlib.Solver.MathSAT
+  , module Language.Hasmtlib.Solver.Bitwuzla
+
+  -- * Internal
+  -- ** Sharing
   , SharingMode(..), setSharingMode
   )
   where
@@ -39,6 +60,7 @@ import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.Bitvec
+import Language.Hasmtlib.Type.Relation
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Counting

src/Language/Hasmtlib/Boolean.hs

@@ -1,13 +1,45 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 
-module Language.Hasmtlib.Boolean where
+{- |
+This module provides a more generic version of bool-like algebras than what the Prelude does for 'Bool'.
+
+The class 'Boolean' therefore overloads most of the Preludes operators like '(&&)'.
+
+However, as 'Bool' also features an instance of 'Boolean', you can simply hide the Prelude ones - not having to import either qualified.
+
+==== __Example__
+
+@
+import Prelude hiding (not, any, all, (&&), (||), and, or)
+import Language.Hasmtlib
+
+problem :: MonadSMT s m => StateT s m (Expr BoolSort, Expr BoolSort)
+problem = do
+  x <- var \@BoolSort
+  y <- var
+  let b = False || True
+  assert $ x && y \<==\> and [x, y, true] && encode b ==> x && y
+  return (x,y)
+@
+-}
+module Language.Hasmtlib.Boolean
+(
+  -- * Class
+  Boolean(..)
+
+  -- * Operators
+, and, or
+, nand, nor
+, all, any
+)
+where
 
 import Prelude (Bool(..), (.), id, Eq(..))
 import qualified Prelude as P
 import Data.Bit
 import Data.Coerce
 import Data.Bits as Bits
-import Data.Foldable hiding (and, or)
+import Data.Foldable hiding (and, or, all, any)
 import qualified Data.Vector.Unboxed.Sized as V
 import GHC.TypeNats
 

src/Language/Hasmtlib/Codec.hs

@@ -3,7 +3,31 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
-module Language.Hasmtlib.Codec where
+{- |
+This module provides the class 'Codec' which takes care of marshalling data to and from external SMT-Solvers.
+
+A generic default implementation with 'GCodec' is possible.
+
+==== __Example__
+
+@
+data V3 a = V3 a a a deriving Generic
+instance Codec a => Codec (V3 a)
+
+constantV3 :: V3 (Expr RealSort)
+constantV3 = encode $ V3 7 69 42
+@
+-}
+module Language.Hasmtlib.Codec
+(
+  -- * Class
+  Codec(..)
+
+  -- * Generics
+, GCodec(..)
+, DefaultDecoded
+)
+where
 
 import Prelude hiding (not, (&&), (||), all, and)
 import Language.Hasmtlib.Type.Bitvec
@@ -23,6 +47,7 @@ import Data.Sequence (Seq)
 import Data.IntMap as IM hiding (foldl)
 import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
+import Data.Array (Array, Ix)
 import qualified Data.Text as Text
 import Data.Monoid (Sum, Product, First, Last, Dual)
 import qualified Data.Vector.Sized as V
@@ -31,7 +56,7 @@ import Control.Lens hiding (from, to)
 import GHC.Generics
 import GHC.TypeLits
 
--- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' to it's type arguments.
+-- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' over it's type arguments.
 type family DefaultDecoded a :: Type where
   DefaultDecoded (t a b c d e f g h) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g) (Decoded h)
   DefaultDecoded (t a b c d e f g) = t (Decoded a) (Decoded b) (Decoded c) (Decoded d) (Decoded e) (Decoded f) (Decoded g)
@@ -182,16 +207,21 @@ instance Codec a => Codec (Dual a)
 instance Codec a => Codec (Identity a)
 
 instance Codec a => Codec (IntMap a) where
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
   encode = fmap encode
 
 instance Codec a => Codec (Seq a) where
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
   encode = fmap encode
 
 instance Codec a => Codec (Map k a) where
   type Decoded (Map k a) = Map k (Decoded a)
-  decode sol = traverse (decode sol)
+  decode = traverse . decode
+  encode = fmap encode
+
+instance (Ix i, Codec e) => Codec (Array i e) where
+  type Decoded (Array i e) = Array i (Decoded e)
+  decode = traverse . decode
   encode = fmap encode
 
 class GCodec f where

src/Language/Hasmtlib/Counting.hs

@@ -1,4 +1,32 @@
-module Language.Hasmtlib.Counting where
+{- |
+This module provides functions for counting symbolic formulas and creating cardinality-constraints.
+
+Internally this converts each given 'Expr' 'BoolSort' into a numerical 'Expr' using 'ite', then sums them up:
+
+@
+  count :: forall t f. (Functor f, Foldable f, Num (Expr t)) => f (Expr BoolSort) -> Expr t
+  count = sum . fmap (\\b -> ite b 1 0)
+@
+
+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 $ ...@
+-}
+module Language.Hasmtlib.Counting
+(
+  -- * Count
+  count, count'
+
+  -- * At-Least
+, atLeast
+
+  -- * Exactly
+, exactly
+
+  -- * At-Most
+, atMost
+)
+where
 
 import Prelude hiding (not, (&&), (||), or)
 import Language.Hasmtlib.Type.SMTSort

src/Language/Hasmtlib/Example/Relation.hs

@@ -0,0 +1,24 @@
+module Language.Hasmtlib.Example.Relation where
+
+import Prelude hiding (not)
+import Language.Hasmtlib
+import Control.Lens
+import Control.Monad
+
+main :: IO ()
+main = do
+  (Sat, Just rel') <- solveWith @SMT (solver opensmt) $ do
+    setLogic "QF_LIA"
+
+    rel <- relation ((2,1), (6,5))
+
+    forM_ (image rel <$> domain rel) (assert . exactly @IntSort 1)
+    forM_ (preimage rel <$> codomain rel) (assert . exactly @IntSort 1)
+
+    assertMaybe $ do
+      item <- rel^?ix (3,3)
+      return $ item === true
+
+    return rel
+
+  putStrLn $ table rel'

src/Language/Hasmtlib/Internal/Parser.hs

@@ -7,6 +7,7 @@ import Prelude hiding (not, (&&), (||), and , or)
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
+import Language.Hasmtlib.Type.Value
 import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution

src/Language/Hasmtlib/Solver/Bitwuzla.hs

@@ -9,11 +9,3 @@ import SMTLIB.Backends.Process
 --   Make sure it's default SAT-Solver binary - probably @cadical@ - is in path too.
 bitwuzla :: Config
 bitwuzla = defaultConfig { exe = "bitwuzla", args = [] }
-
--- | A 'Config' for Bitwuzla which uses Kissat for SAT-Solving.
---   Requires binary @bitwuzla@ and @kissat@ to be in path.
---
--- Combination with Kissat currently behaves weirdly: https://github.com/bitwuzla/bitwuzla/issues/119
---
--- bitwuzlaWithKissat :: Config
--- bitwuzlaWithKissat = defaultConfig { exe = "bitwuzla", args = ["--sat-solver=kissat"] }