ersatz 0.4.6 → 0.4.7

raw patch · 10 files changed

+52/−14 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

+ Ersatz.Solver.Minisat: anyminisat :: Solver SAT IO

Files

.hlint.yaml +2/−0
.travis.yml +3/−8
CHANGELOG.md +4/−0
ersatz.cabal +1/−1
src/Ersatz/Solver.hs +6/−2
src/Ersatz/Solver/Common.hs +28/−0
src/Ersatz/Solver/Minisat.hs +5/−0
tests/Moore.hs +1/−1
tests/Speed.hs +1/−1
tests/Z001.hs +1/−1

.hlint.yaml view

@@ -1,3 +1,5 @@+- arguments: [--cpp-define=HLINT, --cpp-ansi]+ - ignore:     name: Use camelCase

.travis.yml view

@@ -4,7 +4,7 @@ # # For more information, see https://github.com/haskell-CI/haskell-ci #-# version: 0.3.20190425+# version: 0.3.20190521 # language: c dist: xenial@@ -119,7 +119,6 @@   - cat $CABALHOME/config   - rm -fv cabal.project cabal.project.local cabal.project.freeze   - travis_retry ${CABAL} v2-update -v-  - if [ $HCNUMVER -eq 80801 ] ; then ${CABAL} v2-install -w ${HC} -j2 hlint --constraint='hlint ==2.1.*' | color_cabal_output ; fi   # Generate cabal.project   - rm -rf cabal.project cabal.project.local cabal.project.freeze   - touch cabal.project@@ -130,7 +129,7 @@     echo "  flags: +examples"                  >> cabal.project     echo ""                                    >> cabal.project     echo "write-ghc-environment-files: always" >> cabal.project-  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | grep -vE -- '^(ersatz)$' | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(ersatz)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"   - cat cabal.project || true   - cat cabal.project.local || true   - if [ -f "./configure.ac" ]; then (cd "." && autoreconf -i); fi@@ -156,7 +155,7 @@     echo "  flags: +examples"                  >> cabal.project     echo ""                                    >> cabal.project     echo "write-ghc-environment-files: always" >> cabal.project-  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | grep -vE -- '^(ersatz)$' | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(ersatz)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"   - cat cabal.project || true   - cat cabal.project.local || true   # Building with tests and benchmarks...@@ -164,10 +163,6 @@   - ${CABAL} v2-build -w ${HC} ${TEST} ${BENCH} all | color_cabal_output   # Testing...   - ${CABAL} v2-test -w ${HC} ${TEST} ${BENCH} all | color_cabal_output-  # HLint..-  - if [ $HCNUMVER -eq 80801 ] ; then (cd ersatz-* && hlint --cpp-ansi --cpp-define=HLINT src) ; fi-  - if [ $HCNUMVER -eq 80801 ] ; then (cd ersatz-* && hlint --cpp-ansi --cpp-define=HLINT examples/sudoku) ; fi-  - if [ $HCNUMVER -eq 80801 ] ; then (cd ersatz-* && hlint --cpp-ansi --cpp-define=HLINT examples/regexp-grid) ; fi   # cabal check...   - (cd ersatz-* && ${CABAL} -vnormal check)   # haddock...

CHANGELOG.md view

@@ -1,3 +1,7 @@+0.4.7 [2019.06.01]+------------------+* Add `anyminisat` and `trySolvers`+ 0.4.6 [2019.05.20] ------------------ * Add support for `cryptominisat5`

ersatz.cabal view

@@ -1,5 +1,5 @@ name:           ersatz-version:        0.4.6+version:        0.4.7 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi

src/Ersatz/Solver.hs view

@@ -24,9 +24,13 @@ import Ersatz.Solver.Minisat  #if __GLASGOW_HASKELL__ < 710-solveWith :: (Monad m, Alternative n, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a))+solveWith ::+  (Monad m, Alternative n, MonadPlus n, HasSAT s, Default s, Codec a) =>+  Solver s m -> StateT s m a -> m (Result, n (Decoded a)) #else-solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a))+solveWith ::+  (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) =>+  Solver s m -> StateT s m a -> m (Result, n (Decoded a)) #endif solveWith solver m = do   (a, problem) <- runStateT m def

src/Ersatz/Solver/Common.hs view

@@ -10,11 +10,17 @@ module Ersatz.Solver.Common   ( withTempFiles   , resultOf++  -- * Support for trying many solvers+  , trySolvers+  , NoSolvers(..)   ) 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.Temp (withSystemTempDirectory)  withTempFiles :: MonadIO m@@ -32,3 +38,25 @@ resultOf (ExitFailure 10) = Satisfied resultOf (ExitFailure 20) = Unsatisfied resultOf _                = Unsolved++-- | This error is thrown by 'trySolvers' when no solvers are found.+newtype NoSolvers = NoSolvers [IOError] deriving Show++instance Exception NoSolvers where+  displayException _ = "no ersatz solvers were found"++-- | Try a list of solvers in order. When a solver fails due to+-- a missing executable the next solver will be tried. Throws+-- 'NoSolvers' exception if none of the given solvers were installed.+trySolvers :: [Solver s IO] -> Solver s IO+trySolvers solvers problem = foldr runSolver noSolvers solvers []+  where+    noSolvers = throwIO . NoSolvers . reverse++    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

src/Ersatz/Solver/Minisat.hs view

@@ -16,6 +16,7 @@   , minisatPath   , cryptominisat5   , cryptominisat5Path+  , anyminisat   ) where  import Data.ByteString.Builder@@ -31,6 +32,10 @@  import qualified Data.ByteString.Char8 as B import Data.List ( foldl' )++-- | Hybrid 'Solver' that tries to use: 'cryptominisat5', 'cryptominisat', and 'minisat'+anyminisat :: Solver SAT IO+anyminisat = trySolvers [cryptominisat5, cryptominisat, minisat]  -- | 'Solver' for 'SAT' problems that tries to invoke the @minisat@ executable from the @PATH@ minisat :: MonadIO m => Solver SAT m

tests/Moore.hs view

@@ -38,7 +38,7 @@  mainf d k n s = do   putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "symmetry ==", show s ]-  (s, mg) <- solveWith cryptominisat5 $ moore d k n s+  (s, mg) <- solveWith anyminisat $ moore d k n s   case (s, mg) of      (Satisfied, Just g) -> do printA g ; return True      _ -> do return False

tests/Speed.hs view

@@ -14,7 +14,7 @@  mainf n = do   putStrLn $ unwords [ "n",  show n ]-  (s, mgs) <- solveWith cryptominisat5 $ do+  (s, mgs) <- solveWith anyminisat $ do       gs <- replicateM n exists       forM_ (zip gs $ tail gs) $ \ (x,y) -> assert ( x /== y )       return (gs :: [Bit])

tests/Z001.hs view

@@ -15,7 +15,7 @@ import Control.Monad.State  main = do-  (Satisfied, Just ms) <- solveWith cryptominisat5 $ do+  (Satisfied, Just ms) <- solveWith anyminisat $ do     [ Restricted a, Restricted b ]         :: [ Restricted 5 (NBV 3) ] <- replicateM 2 unknown     -- assert $ gt (a^2 * b^2) (b^3 * a^3)