satchmo-backends 1.8.2 → 1.9.1

raw patch · 8 files changed

+83/−233 lines, 8 filesdep +arraydep +timeitPVP ok

version bump matches the API change (PVP)

Dependencies added: array, timeit

API changes (from Hackage documentation)

Files

• Satchmo/Solver/Clasp.hs +0/−78
• Satchmo/Solver/Internal.hs +10/−1
• Satchmo/Solver/Minisat.hs +44/−49
• Satchmo/Solver/Pcosat.hs +15/−5
• Satchmo/Solver/Quantor.hs +0/−43
• Satchmo/Solver/Qube.hs +0/−43
• Satchmo/Solver/Yices.hs +9/−8
• satchmo-backends.cabal +5/−6

@@ -1,78 +0,0 @@-{-# language PatternSignatures #-}---- | http://www.cs.uni-potsdam.de/clasp/--module Satchmo.Solver.Clasp--( solve-, using-)--where--import Satchmo.Data-import Satchmo.SAT-import qualified Satchmo.Solve-import Satchmo.Solver.Internal--import Data.Monoid-import System.Process-import System.Exit-import System.IO-import Control.Monad ( when )-import Control.Concurrent-import Control.Exception--import qualified Data.ByteString.Char8 as S-import qualified Data.ByteString.Lazy.Char8 as BS--- import qualified Data.ByteString.Lazy as BS--import qualified Data.Map as M--solve = using "clasp"--using fp = Satchmo.Solve.solve $ clasp fp--clasp :: FilePath -> Satchmo.Solve.Implementation-clasp fp cs Header{numVars=numVars, numClauses=numClauses}   = do-    let header = mkDimacsHeader numVars numClauses-        cs'    = BS.pack ( header ++ "\n" ) `mappend` cs-    let debug = False-    if debug -       then BS.hPut stderr cs'-       else hPutStrLn stderr header --    ( hin, hout, herr, proc ) <- -        System.Process.runInteractiveCommand-            $ unwords [ fp, "--dimacs",  "--number=1",  "--sat-p=20,25,150"-                      , "--hParam=0,512"  ] --    container <- newEmptyMVar-    forkIO $ do -        -- hPutStrLn stderr "before hPut"-        BS.hPut hin cs'-        -- waitForProcess proc-        -- hPutStrLn stderr "before hGetContents"-        ds <- hGetContents hout-        hPutStrLn stderr $ unwords [ "output", "length", show ( length ds ) ]-        putMVar container ds--    out <- takeMVar container -        `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do -            -- hPutStrLn stderr "caught exception"-            terminateProcess proc-            return ""--    when debug $ hPutStrLn stdout out-    let -        assign = M.fromList $ do-                'v' : xs <- lines out-                l <- map read $ takeWhile ( /= "0" ) $ words xs-                return ( variable l, positive l )-        status = filter ( \ cs -> take 1 cs == "s" ) $ lines out-    case status of-        "s SATISFIABLE" : post  -> do-            return $ Just assign-        _ -> do-            return $ Nothing-

@@ -10,10 +10,19 @@         (hIn, hOut, hErr, hProc) <-              runInteractiveProcess exec args Nothing Nothing         try (BS.hPut hIn input) :: IO (Either AsyncException ())+        stdout <- BS.hGetContents hOut+        stderr <- hGetContents hErr+        code   <- waitForProcess hProc+        return (code, BS.unpack stdout, stderr)++readProcessWithExitCodeS exec args input = do+        (hIn, hOut, hErr, hProc) <- +            runInteractiveProcess exec args Nothing Nothing+        try (S.hPut hIn input) :: IO (Either AsyncException ())         stdout <- S.hGetContents hOut         stderr <- hGetContents hErr         code   <- waitForProcess hProc         return (code, S.unpack stdout, stderr)  mkDimacsHeader numVars numClauses = -    "p cnf " ++ show numVars ++ " " ++ show numClauses +    "p cnf " ++ show numVars ++ " " ++ show numClauses ++ "\n"

@@ -11,75 +11,70 @@ import Satchmo.Data import qualified Satchmo.Solve import Satchmo.Solver.Internal-import Satchmo.SAT+import Satchmo.SAT.Seq -import qualified Data.ByteString.Char8 as S-import qualified Data.ByteString.Lazy.Char8 as BS--- import qualified Data.ByteString.Lazy as BS+import qualified Data.ByteString.Char8 as BS+-- import qualified Data.ByteString.Lazy.Char8 as BS  import Data.Monoid-import System.IO (stderr, hFlush, hClose, hPutStrLn, hGetContents-       , hSetBuffering, BufferMode (..) )+import System.IO  import System.Process import Control.Monad ( when ) import Control.Concurrent import Control.Exception-import qualified Control.Exception as C -import qualified Data.Map as M+import System.TimeIt+import Text.Printf -solve = using "/usr/bin/minisat2"+-- import qualified Data.Map as M+import qualified Data.Array as A +solve = using "minisat2"+ using fp = Satchmo.Solve.solve $ minisat fp  minisat :: FilePath -> Satchmo.Solve.Implementation minisat fp cs Header{numVars=numVars, numClauses=numClauses} = do-    let header = mkDimacsHeader numVars numClauses-        cs'    = BS.pack header `mappend` cs+    let header = BS.pack $ mkDimacsHeader numVars numClauses+         let debug = False-    if debug-       then BS.hPut stderr cs'-       else hPutStrLn stderr header >> hFlush stderr---- copied from--- http://hackage.haskell.org/packages/archive/process/1.0.1.5/doc/html/src/System-Process.html#readProcessWithExitCode--    ( Just inh, Just outh, Just errh, pid ) <- -       createProcess ( proc fp  [ "/dev/stdin", "/dev/stdout" ] )-           { std_in  = CreatePipe, std_out = CreatePipe, std_err = CreatePipe }--    outMVar <- newEmptyMVar--    -- fork off a thread to start consuming stdout-    out  <- hGetContents outh-    _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()--    -- fork off a thread to start consuming stderr-    err  <- hGetContents errh-    _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()--    -- now write and flush any input-    do BS.hPut  inh cs'; hFlush inh ; hClose inh -- done with stdin+    when debug $ do+        BS.hPutStrLn stderr header+        BS.hPutStrLn stderr cs -    -- wait on the output-    takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do -        terminateProcess pid-    takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do -        terminateProcess pid-    hClose outh ; hClose errh+    ( hin, hout, herr, proc ) <- runInteractiveCommand+           ( unwords [ fp, "/dev/stdin", "/dev/stdout" ] )+    +    container <- newEmptyMVar -    -- wait on the process-    ex <- waitForProcess pid+    streamer <- forkIO $ do+        BS.hPutStr hin ( mappend header cs )+        -- waitForProcess proc+        ds <- hGetContents hout+        hPutStrLn stderr $ unwords [ "output", "length", show (length ds) ]+        hPutStrLn stderr $ take 80 ds+        putMVar container ds -    hPutStrLn stderr $ unwords [ "output", "length", show ( length out ) ]-    -- hPutStrLn stderr out+    out <- takeMVar container `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do +        -- hPutStrLn stderr "got exception in waitForProcess"+        killThread streamer+        terminateProcess proc+        -- hPutStrLn stderr "terminateProcess done"+        return ""+    -- hPutStrLn stderr "end waitForProcess"      case lines out of         "SAT" : xs : _ -> do-           let dict = Just $ M.fromList $ do-                            l <- map read $ takeWhile ( /= "0" ) $ words xs-                            return ( variable l, positive l )-           when debug $ print dict-           return dict+           let dict = Just $ A.listArray (1,numVars) $ do+                            (v,l) <- zip [1..] $ map read $ takeWhile ( /= "0" ) $ words xs+                            return $ if variable l == v then  positive l else error "huh"+           seq (length out) $ return dict         _ -> return $ Nothing ++timeItMsg msg action = do +    (time, res) <- timeItT action+    hPrintf stderr "CPU time: %6.2fs for %s\n" time msg    +    hFlush stderr +    return res+    

@@ -24,11 +24,11 @@ import Control.Concurrent import Control.Exception -import qualified Data.ByteString.Char8 as S-import qualified Data.ByteString.Lazy.Char8 as BS--- import qualified Data.ByteString.Lazy as BS+-- import qualified Data.ByteString.Lazy.Char8 as BS+import qualified Data.ByteString.Char8 as BS -import qualified Data.Map as M+-- import qualified Data.Map as M+import qualified Data.Array as A  solve = using "precosat" @@ -40,7 +40,7 @@ pcosat :: FilePath -> Satchmo.Solve.Implementation pcosat fp cs Header{numVars=numVars, numClauses=numClauses}   = do     let header = mkDimacsHeader numVars numClauses-        cs'    = BS.pack ( header ++ "\n" ) `mappend` cs+        cs'    = BS.pack header `mappend` cs     if debug         then BS.hPut stderr cs'        else hPutStrLn stderr header @@ -67,10 +67,20 @@      when debug $ hPutStrLn stdout out     let core = filter ( \ cs -> take 1 cs /= "c" ) $ lines out++{-         assign = M.fromList $ do                 'v' : xs <- core                 l <- map read $ takeWhile ( /= "0" ) $ words xs                 return ( variable l, positive l )+-}++        assign = A.array (1, numVars) $ do+                'v' : xs <- core+                l <- map read $ takeWhile ( /= "0" ) $ words xs+                return ( variable l, positive l )+            +         status = filter ( \ cs -> take 1 cs == "s" ) $ lines out     case status of         "s SATISFIABLE" : post  -> do

@@ -1,43 +0,0 @@-module Satchmo.Solver.Quantor--( solve-)--where--import Satchmo.Data-import qualified Satchmo.Solve-import Satchmo.Solver.Internal-import Satchmo.SAT--import Data.Monoid-import qualified Data.ByteString.Char8 as S-import qualified Data.ByteString.Lazy.Char8 as BS-import System.IO  (stderr, hFlush, hPutStrLn)-import System.Process-import Control.Monad ( when )--import qualified Data.Map as M--solve = Satchmo.Solve.solve quantor--quantor :: Satchmo.Solve.Implementation-quantor cs Header{numVars=numVars, numClauses=numClauses} = do-    let header = mkDimacsHeader numVars numClauses-        cs'    = BS.pack header `mappend` cs-    let debug = True-    if debug -       then BS.hPut stderr cs'-       else hPutStrLn stderr header >> hFlush stderr-    ( code, stdout, stderr ) <- -        readProcessWithExitCodeBS "quantor" [ "-v", "--resolve-exported=0" ] cs'-    when debug $ hPutStrLn System.IO.stderr stdout-    let -    case filter ( \ ws -> take 1 ws /= [ "c" ] ) $ map words $ lines stdout of-        [ "s", ok ] : rest | ok `elem` [ "TRUE", "SATISFIABLE" ] -> -            return $ Just $ M.fromList $ do-                "v" : vars <- rest-                l <- map read $ takeWhile ( /= "0" ) vars-                return ( variable l, positive l  )-        _ -> return $ Nothing-

@@ -1,43 +0,0 @@-module Satchmo.Solver.Qube--( solve-)--where--import Satchmo.Data-import qualified Satchmo.Solve-import Satchmo.Solver.Internal-import Satchmo.SAT--import qualified Data.ByteString.Char8 as S-import qualified Data.ByteString.Lazy.Char8 as BS--import Data.Monoid-import System.IO (stderr, hPutStrLn)-import System.Process-import Control.Monad ( when )--import qualified Data.Map as M--solve = Satchmo.Solve.solve qube--qube :: Satchmo.Solve.Implementation-qube cs Header{numVars=numVars, numClauses=numClauses} = do-    let header = mkDimacsHeader numVars numClauses-    let debug = True-    if debug -       then BS.hPut stderr cs-       else hPutStrLn stderr header-    ( code, stdout, stderr ) <- -        readProcessWithExitCodeBS "QuBE6.5" [ "/dev/stdin" ] (BS.pack header `mappend` cs)-    when debug $ hPutStrLn System.IO.stderr stdout-    let -    case filter ( \ ws -> take 1 ws /= [ "c" ] ) $ map words $ lines stdout of-        [ "s", "cnf", "1" ] : rest -> -            return $ Just $ M.fromList $ do-                "v" : vars <- rest-                l <- map read $ takeWhile ( /= "0" ) vars-                return ( variable l, positive l )-        _ -> return $ Nothing-

@@ -7,8 +7,7 @@  where -import qualified Data.ByteString.Char8 as S-import qualified Data.ByteString.Lazy.Char8 as BS+import qualified Data.ByteString.Char8 as BS import Data.Monoid import Satchmo.Data import qualified Satchmo.Solve@@ -21,7 +20,8 @@ import System.Process import Control.Monad ( when ) -import qualified Data.Map as M+-- import qualified Data.Map as M+import qualified Data.Array as A  type Seconds = Int @@ -31,18 +31,19 @@ yices :: Maybe Seconds -> Satchmo.Solve.Implementation yices timeout cs Header{numVars=numVars, numClauses=numClauses} = do     let header = mkDimacsHeader numVars numClauses-    let debug = False+    let debug = True     if debug        then BS.hPut stderr cs        else hPutStrLn stderr header >> hFlush stderr      let opts = ["-e","-d"] ++ maybe [] (\t -> ["-tm", show t]) timeout -    ( code, stdout, stderr ) <- readProcessWithExitCodeBS "yices" opts (BS.pack header `mappend` cs)+    ( code, stdout, stderr ) <- +        readProcessWithExitCodeS "yices" opts (BS.pack header `mappend` cs)     when debug $ hPutStrLn System.IO.stderr stdout     when (not $ null stderr) $ putStrLn stderr     case lines stdout of-        "sat" : xs : _ -> return $ Just $ M.fromList $ do+        "sat" : xs : _ -> return $ Just $ A.array (1, numVars) $ do             l :: Literal <- map read $ words xs             return ( variable l, positive l )         _ -> return $ Nothing@@ -57,11 +58,11 @@      let opts =  ["-e","-d","-ms", "-mw", show maxWeight] ++ maybe [] (\t -> ["-tm", show t]) timeout -    ( code, stdout, stderr ) <- readProcessWithExitCodeBS "yices" opts (BS.pack header `mappend` cs)+    ( code, stdout, stderr ) <- readProcessWithExitCodeS "yices" opts (BS.pack header `mappend` cs)     when debug $ hPutStrLn System.IO.stderr stdout     when (not $ null stderr) $ putStrLn stderr     case lines stdout of-        "sat" : xs : _ -> return $ Just $ M.fromList $ do+        "sat" : xs : _ -> return $ Just $ A.array (1, Weighted.numVars h) $ do             l <- map read $ words xs             return ( variable l, positive l )         _ -> return $ Nothing

@@ -1,5 +1,5 @@ Name:           satchmo-backends-Version:        1.8.2+Version:        1.9.1  License:        GPL License-file:	gpl-2.0.txt@@ -19,15 +19,14 @@ build-type: Simple  library-    Build-depends: satchmo >= 1.8, process, base == 4.* , containers, bytestring+    Build-depends: satchmo >= 1.8, process, base == 4.* , containers, array, bytestring, timeit     Exposed-modules:         Satchmo.Solver.Minisat         Satchmo.Solver.Pcosat-        Satchmo.Solver.Clasp-        Satchmo.Solver.Quantor-        Satchmo.Solver.Qube+        -- Satchmo.Solver.Clasp+        -- Satchmo.Solver.Quantor+        -- Satchmo.Solver.Qube         Satchmo.Solver.Yices     Other-modules:         Satchmo.Solver.Internal     hs-source-dirs:	.-