ersatz 0.4.5 → 0.4.6

raw patch · 9 files changed

+38/−8 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• .ghci +0/−1
• CHANGELOG.md +4/−0
• ersatz.cabal +1/−2
• examples/regexp-grid/Main.hs +1/−1
• examples/sudoku/Main.hs +1/−1
• src/Ersatz/Solver/Minisat.hs +28/−0
• tests/Moore.hs +1/−1
• tests/Speed.hs +1/−1
• tests/Z001.hs +1/−1

@@ -1,1 +0,0 @@-:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h -optP-Iincludes

@@ -1,3 +1,7 @@+0.4.6 [2019.05.20]+------------------+* Add support for `cryptominisat5`+ 0.4.5 [2019.05.02] ------------------ * Allow `ersatz-regexp-grid` to build with `base-4.13` (GHC 8.8).

@@ -1,5 +1,5 @@ name:           ersatz-version:        0.4.5+version:        0.4.6 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi@@ -82,7 +82,6 @@               , GHC == 8.6.5               , GHC == 8.8.1 extra-source-files:-  .ghci   .gitignore   .hlint.yaml   .travis.yml

@@ -11,7 +11,7 @@  main :: IO () main = do-  (res, msol) <- solveWith cryptominisat problem+  (res, msol) <- solveWith cryptominisat5 problem   when (res /= Satisfied) (fail (show res))   case msol of     Nothing  -> fail "Sol was Nothing"

@@ -21,7 +21,7 @@   putStr (render initValues)    putStrLn "Solution:"-  (res, msol) <- solveWith cryptominisat (problem initValues)+  (res, msol) <- solveWith cryptominisat5 (problem initValues)   when (res /= Satisfied) (fail (show res))   case msol of     Just sol -> putStr (render sol)

@@ -14,6 +14,8 @@   ( minisat   , cryptominisat   , minisatPath+  , cryptominisat5+  , cryptominisat5Path   ) where  import Data.ByteString.Builder@@ -68,3 +70,29 @@                             in  if 0 == v then m else IntMap.insert (abs v) (v>0) m                  ) IntMap.empty ys     _ -> IntMap.empty -- WRONG (should be Nothing)++-- | 'Solver' for 'SAT' problems that tries to invoke the @cryptominisat5@ executable from the @PATH@+cryptominisat5 :: MonadIO m => Solver SAT m+cryptominisat5 = cryptominisat5Path "cryptominisat5"++-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @cryptominisat5@ compatible arguments.+--+-- The 'FilePath' refers to the path to the executable.+cryptominisat5Path :: MonadIO m => FilePath -> Solver SAT m+cryptominisat5Path path problem = liftIO $+  withTempFiles ".cnf" "" $ \problemPath _ -> do+    withFile problemPath WriteMode $ \fh ->+      hPutBuilder fh (dimacs problem)++    (exit, out, _err) <-+      readProcessWithExitCode path [problemPath] []++    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)

@@ -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 minisat $ moore d k n s+  (s, mg) <- solveWith cryptominisat5 $ moore d k n s   case (s, mg) of      (Satisfied, Just g) -> do printA g ; return True      _ -> do return False

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

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