ersatz 0.4.11 → 0.4.12

raw patch · 9 files changed

+195/−13 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• AUTHORS.md +1/−1
• CHANGELOG.md +5/−0
• ersatz.cabal +2/−1
• src/Ersatz/Equatable.hs +40/−0
• src/Ersatz/Orderable.hs +88/−0
• src/Ersatz/Solver.hs +2/−0
• src/Ersatz/Solver/Common.hs +13/−5
• src/Ersatz/Solver/Minisat.hs +0/−6
• src/Ersatz/Solver/Z3.hs +44/−0

@@ -6,7 +6,7 @@  It was revived by [Johan Kiviniemi](mailto:ersatz@johan.kiviniemi.name) [@ion1](https://github.com/ion1) who got it into a working condition by implementing some missing parts, which inspired the original author into polishing it up and releasing it. -Eric Mertens (@glguy](https://github.com/glguy) has been pouring code into it ever since then.+Eric Mertens [@glguy](https://github.com/glguy) has been pouring code into it ever since then.  Omission from this page is by no means an attempt to discount your contributions! Thank you for all of your help! 

@@ -1,3 +1,8 @@+0.4.12 [2022.08.11]+-------------------+* Add `Equatable` and `Orderable` instances for more base and containers types+* Add solver support for `z3`+ 0.4.11 [2022.05.18] ------------------- * Allow building with `mtl-2.3.*` and `transformers-0.6.*`.

@@ -1,5 +1,5 @@ name:           ersatz-version:        0.4.11+version:        0.4.12 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi@@ -196,6 +196,7 @@     Ersatz.Solver     Ersatz.Solver.DepQBF     Ersatz.Solver.Minisat+    Ersatz.Solver.Z3     Ersatz.Variable     Ersatz.Counting     Ersatz.Relation

@@ -24,10 +24,18 @@  import Ersatz.Bit import GHC.Generics+import Numeric.Natural import Data.IntMap (IntMap)+import Data.Foldable (toList) import Data.Map (Map)+import Data.Int+import Data.Word+import Data.Void+import Data.List.NonEmpty (NonEmpty) import qualified Data.Map as Map import qualified Data.IntMap as IntMap+import qualified Data.Sequence as Seq+import qualified Data.Tree as Tree  infix  4 ===, /== @@ -57,6 +65,15 @@     | IntMap.keys x == IntMap.keys y = IntMap.elems x === IntMap.elems y     | otherwise                      = false +instance Equatable v => Equatable (Seq.Seq v) where+  x === y+    | Seq.length x == Seq.length y = toList x === toList y+    | otherwise                    = false++-- manually written because ancient GHC didn't have the generics instance+instance Equatable a => Equatable (Tree.Tree a) where+  Tree.Node x xs === Tree.Node y ys = x === y && xs === ys+ instance (Equatable a, Equatable b) => Equatable (a,b) instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c) instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)@@ -65,6 +82,7 @@ instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g) instance Equatable a => Equatable (Maybe a) instance Equatable a => Equatable [a]+instance Equatable a => Equatable (NonEmpty a) instance (Equatable a, Equatable b) => Equatable (Either a b)  class GEquatable f where@@ -89,3 +107,25 @@  instance Equatable a => GEquatable (K1 i a) where   K1 a ===# K1 b = a === b++-- Boring instances that end up being useful when deriving Equatable with Generics++instance Equatable ()       where _ === _ = true+instance Equatable Void     where x === y = x `seq` y `seq` error "Equatable[Void].==="+instance Equatable Int      where x === y = bool (x == y)+instance Equatable Integer  where x === y = bool (x == y)+instance Equatable Natural  where x === y = bool (x == y)+instance Equatable Word     where x === y = bool (x == y)+instance Equatable Word8    where x === y = bool (x == y)+instance Equatable Word16   where x === y = bool (x == y)+instance Equatable Word32   where x === y = bool (x == y)+instance Equatable Word64   where x === y = bool (x == y)+instance Equatable Int8     where x === y = bool (x == y)+instance Equatable Int16    where x === y = bool (x == y)+instance Equatable Int32    where x === y = bool (x == y)+instance Equatable Int64    where x === y = bool (x == y)+instance Equatable Char     where x === y = bool (x == y)+instance Equatable Float    where x === y = bool (x == y)+instance Equatable Double   where x === y = bool (x == y)+instance Equatable Ordering where x === y = bool (x == y)+instance Equatable Bool     where x === y = bool (x == y)

@@ -25,9 +25,18 @@  import Prelude hiding ((&&),(||),not,and,or,all,any) +import Data.Foldable (toList)+import Data.Int+import Data.Void+import Data.Word import Ersatz.Bit import Ersatz.Equatable import GHC.Generics+import Numeric.Natural+import qualified Data.IntMap as IntMap+import qualified Data.Map as Map+import qualified Data.Sequence as Seq+import qualified Data.Tree as Tree  infix  4 <?, <=?, >=?, >? @@ -57,6 +66,44 @@   a <?  b = not a && b   a <=? b = not a || b +-- | Compare by lexicographic order on sorted key-value pairs+instance (Ord k, Orderable v) => Orderable (Map.Map k v) where+  x <?  y = assocsLt (Map.assocs x) (Map.assocs y)+  x <=? y = assocsLe (Map.assocs x) (Map.assocs y)++-- | Compare by lexicographic order on sorted key-value pairs+instance Orderable v => Orderable (IntMap.IntMap v) where+  x <?  y = assocsLt (IntMap.assocs x) (IntMap.assocs y)+  x <=? y = assocsLe (IntMap.assocs x) (IntMap.assocs y)++assocsLt :: (Ord k, Orderable v) => [(k,v)] -> [(k,v)] -> Bit+assocsLt _ [] = false+assocsLt [] _ = true+assocsLt ((k1,v1):xs) ((k2,v2):ys) =+  case compare k1 k2 of+    LT -> true+    GT -> false+    EQ -> v1 <? v2 || v1 === v2 && assocsLt xs ys++assocsLe :: (Ord k, Orderable v) => [(k,v)] -> [(k,v)] -> Bit+assocsLe [] _ = true+assocsLe _ [] = false+assocsLe ((k1,v1):xs) ((k2,v2):ys) =+  case compare k1 k2 of+    LT -> true+    GT -> false+    EQ -> v1 <? v2 || v1 === v2 && assocsLe xs ys++-- | Compare by lexicographic order on elements+instance Orderable v => Orderable (Seq.Seq v) where+  x <?  y = toList x <?  toList y+  x <=? y = toList x <=? toList y++-- | Compare by lexicographic order on: root node, list of children+instance Orderable a => Orderable (Tree.Tree a) where+  Tree.Node x xs <?  Tree.Node y ys = (x,xs) <?  (y,ys)+  Tree.Node x xs <=? Tree.Node y ys = (x,xs) <=? (y,ys)+ instance (Orderable a, Orderable b) => Orderable (a,b) instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c) instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d)@@ -115,3 +162,44 @@ instance Orderable a => GOrderable (K1 i a) where   K1 a <?#  K1 b = a <?  b   K1 a <=?# K1 b = a <=? b++-- Boring instances that end up being useful when deriving Orderable with Generics++instance Orderable ()       where _ <?  _ = false+                                  _ <=? _ = true+instance Orderable Void     where x <?  y = x `seq` y `seq` error "Orderable[Void].<?"+                                  x <=? y = x `seq` y `seq` error "Orderable[Void].<=?"+instance Orderable Int      where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Integer  where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Natural  where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word8    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word16   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word32   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word64   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int8     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int16    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int32    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int64    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Char     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Float    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Double   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Ordering where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Bool     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)

@@ -10,6 +10,7 @@ module Ersatz.Solver   ( module Ersatz.Solver.DepQBF   , module Ersatz.Solver.Minisat+  , module Ersatz.Solver.Z3   , solveWith   ) where @@ -21,6 +22,7 @@ import Ersatz.Solution import Ersatz.Solver.DepQBF import Ersatz.Solver.Minisat+import Ersatz.Solver.Z3  solveWith ::   (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) =>

@@ -14,14 +14,18 @@   -- * Support for trying many solvers   , trySolvers   , NoSolvers(..)++  , parseSolution5   ) where  import Control.Exception (Exception(..), throwIO) import Control.Monad.IO.Class import Ersatz.Solution import System.Exit (ExitCode(..))-import System.IO.Error (isDoesNotExistError, tryIOError)+import System.IO.Error (tryIOError) import System.IO.Temp (withSystemTempDirectory)+import Data.IntMap (IntMap)+import qualified Data.IntMap.Strict as IntMap  withTempFiles :: MonadIO m               => FilePath  -- ^ Problem file extension including the dot, if any@@ -56,7 +60,11 @@     runSolver solver next es =       do res <- tryIOError (solver problem)          case res of-           Left e-             | isDoesNotExistError e -> next (e:es)-             | otherwise             -> ioError e-           Right x                   -> return x+           Left  e -> next (e:es)+           Right x -> return x++parseSolution5 :: String -> IntMap Bool+parseSolution5 txt = IntMap.fromList [(abs v, v > 0) | v <- vars, v /= 0]+  where+    vlines = [l | ('v':l) <- lines txt]+    vars = map read (foldMap words vlines)

@@ -96,9 +96,3 @@     let sol = parseSolution5 out      return (resultOf exit, sol)--parseSolution5 :: String -> IntMap Bool-parseSolution5 txt = IntMap.fromList [(abs v, v > 0) | v <- vars, v /= 0]-  where-    vlines = [l | ('v':l) <- lines txt]-    vars = map read (foldMap words vlines)

@@ -0,0 +1,44 @@+--------------------------------------------------------------------+-- |+-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Solver.Z3+  ( z3+  , z3Path+  ) where++import Data.ByteString.Builder+import Control.Monad.IO.Class+import Ersatz.Problem+import Ersatz.Solution+import Ersatz.Solver.Common+import System.IO+import System.Process (readProcessWithExitCode)++-- | 'Solver' for 'SAT' problems that tries to invoke the @z3@ executable from the @PATH@+z3 :: MonadIO m => Solver SAT m+z3 = z3Path "z3"++-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @z3@ compatible arguments.+--+-- The 'FilePath' refers to the path to the executable.+z3Path :: MonadIO m => FilePath -> Solver SAT m+z3Path path problem = liftIO $+  withTempFiles ".cnf" "" $ \problemPath _ -> do+    withFile problemPath WriteMode $ \fh ->+      hPutBuilder fh (dimacs problem)++    (_exit, out, _err) <-+      readProcessWithExitCode path ["-dimacs", problemPath] []++    let result = case lines out of+                    "s SATISFIABLE":_   -> Satisfied+                    "s UNSATISFIABLE":_ -> Unsatisfied+                    _                   -> Unsolved++    return (result, parseSolution5 out)