satchmo-backends 1.4 → 1.8.0

raw patch · 8 files changed

+337/−32 lines, 8 filesdep +bytestringdep ~basedep ~satchmoPVP ok

version bump matches the API change (PVP)

Dependencies added: bytestring

Dependency ranges changed: base, satchmo

API changes (from Hackage documentation)

Files

• Satchmo/Solver/Clasp.hs +78/−0
• Satchmo/Solver/Internal.hs +19/−0
• Satchmo/Solver/Minisat.hs +51/−14
• Satchmo/Solver/Pcosat.hs +81/−0
• Satchmo/Solver/Quantor.hs +15/−8
• Satchmo/Solver/Qube.hs +15/−8
• Satchmo/Solver/Yices.hs +70/−0
• satchmo-backends.cabal +8/−2

@@ -0,0 +1,78 @@+{-# 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+

@@ -0,0 +1,19 @@+module Satchmo.Solver.Internal where++import Control.Exception+import qualified Data.ByteString.Char8 as S+import qualified Data.ByteString.Lazy.Char8 as BS+import System.IO+import System.Process++readProcessWithExitCodeBS exec args input = do+        (hIn, hOut, hErr, hProc) <- +            runInteractiveProcess exec args Nothing Nothing+        try (BS.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 

@@ -1,33 +1,70 @@+{-# language PatternSignatures #-}+ module Satchmo.Solver.Minisat   ( solve+, using )  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 qualified Data.ByteString.Lazy as BS++import Data.Monoid+import System.IO (stderr, hFlush, hPutStrLn, hGetContents) import System.Process import Control.Monad ( when )+import Control.Concurrent+import Control.Exception  import qualified Data.Map as M -solve = Satchmo.Solve.solve minisat+solve = using "minisat" -minisat :: Satchmo.Solve.Implementation-minisat cs = do+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 debug = False-    if debug -       then putStrLn cs-       else putStrLn $ head $ lines cs-    ( code, stdout, stderr ) <- -        readProcessWithExitCode "minisat" [ "/dev/stdin", "/dev/stdout" ] cs-    when debug $ putStrLn stdout-    case lines stdout of-        "SAT" : xs : _ -> return $ Just $ M.fromList $ do-            x <- takeWhile ( /= 0 ) $ map read $ words xs-            let l = literal $ abs x-            return ( l, x > 0 )+    if False +       then BS.hPut stderr cs'+       else hPutStrLn stderr header >> hFlush stderr+++    ( hin, hout, herr, proc ) <- +        System.Process.runInteractiveCommand+            $ unwords [ fp, "/dev/stdin", "/dev/stdout" ] ++    container <- newEmptyMVar+    forkIO $ do +        BS.hPut hin cs+        -- waitForProcess proc+        ds <- hGetContents hout+        hPutStrLn stderr $ unwords [ "output", "length", show ( length ds ) ]+        putMVar container ds++    out <- takeMVar container `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do +        -- hPutStrLn stderr "got exception in waitForProcess"+        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         _ -> return $ Nothing 

@@ -0,0 +1,81 @@+{-# language PatternSignatures #-}++-- | textual interface to Precosat/Picosat solver,+-- cf. http://fmv.jku.at/precosat/++module Satchmo.Solver.Pcosat++( 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 "precosat"++using fp = Satchmo.Solve.solve $ pcosat fp++debug :: Bool+debug = False++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+    if debug +       then BS.hPut stderr cs'+       else hPutStrLn stderr header ++    ( hin, hout, herr, proc ) <- +        System.Process.runInteractiveCommand+            $ unwords [ fp ] ++    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 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 )+        status = filter ( \ cs -> take 1 cs == "s" ) $ lines out+    case status of+        "s SATISFIABLE" : post  -> do+            when debug $ hPutStrLn stderr $ show assign+            return $ Just assign+        _ -> do+            return $ Nothing+

@@ -7,7 +7,13 @@  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 ) @@ -16,21 +22,22 @@ solve = Satchmo.Solve.solve quantor  quantor :: Satchmo.Solve.Implementation-quantor cs = do+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 putStrLn cs-       else putStrLn $ head $ lines cs+       then BS.hPut stderr cs'+       else hPutStrLn stderr header >> hFlush stderr     ( code, stdout, stderr ) <- -        readProcessWithExitCode "quantor" [ "-v", "--resolve-exported=0" ] cs-    when debug $ putStrLn stdout+        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-                x <- takeWhile ( /= 0 ) $ map read vars-                let l = literal $ abs x-                return ( l, x > 0 )+                l <- map read $ takeWhile ( /= "0" ) vars+                return ( variable l, positive l  )         _ -> return $ Nothing 

@@ -7,7 +7,14 @@  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 ) @@ -16,21 +23,21 @@ solve = Satchmo.Solve.solve qube  qube :: Satchmo.Solve.Implementation-qube cs = do+qube cs Header{numVars=numVars, numClauses=numClauses} = do+    let header = mkDimacsHeader numVars numClauses     let debug = True     if debug -       then putStrLn cs-       else putStrLn $ head $ lines cs+       then BS.hPut stderr cs+       else hPutStrLn stderr header     ( code, stdout, stderr ) <- -        readProcessWithExitCode "QuBE6.5" [ "/dev/stdin" ] cs-    when debug $ putStrLn stdout+        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-                x <- takeWhile ( /= 0 ) $ map read vars-                let l = literal $ abs x-                return ( l, x > 0 )+                l <- map read $ takeWhile ( /= "0" ) vars+                return ( variable l, positive l )         _ -> return $ Nothing 

@@ -0,0 +1,70 @@+{-# LANGUAGE RecordWildCards, NamedFieldPuns, PatternSignatures #-}++module Satchmo.Solver.Yices++( solve, solveW+)++where++import qualified Data.ByteString.Char8 as S+import qualified Data.ByteString.Lazy.Char8 as BS+import Data.Monoid+import Satchmo.Data+import qualified Satchmo.Solve+import Satchmo.Solver.Internal+import Satchmo.SAT+import qualified Satchmo.SAT.Weighted as Weighted++import Control.Exception+import System.IO+import System.Process+import Control.Monad ( when )++import qualified Data.Map as M++type Seconds = Int++solve  timeout = Satchmo.Solve.solve (yices timeout)+solveW timeout maxW = Satchmo.Solve.solveW maxW (yicesW timeout)++yices :: Maybe Seconds -> Satchmo.Solve.Implementation+yices timeout cs Header{numVars=numVars, numClauses=numClauses} = do+    let header = mkDimacsHeader numVars numClauses+    let debug = False+    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)+    when debug $ hPutStrLn System.IO.stderr stdout+    when (not $ null stderr) $ putStrLn stderr+    case lines stdout of+        "sat" : xs : _ -> return $ Just $ M.fromList $ do+            l :: Literal <- map read $ words xs+            return ( variable l, positive l )+        _ -> return $ Nothing++yicesW :: Maybe Seconds -> Satchmo.Solve.WeightedImplementation+yicesW timeout cs h@Weighted.Header{Weighted.maxWeight=maxWeight} = do+    let header = mkMaxWalkSatDimacsHeader h+    let debug = False+    if debug+       then BS.hPut stderr cs+       else hPutStrLn stderr header >> hFlush stdout++    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)+    when debug $ hPutStrLn System.IO.stderr stdout+    when (not $ null stderr) $ putStrLn stderr+    case lines stdout of+        "sat" : xs : _ -> return $ Just $ M.fromList $ do+            l <- map read $ words xs+            return ( variable l, positive l )+        _ -> return $ Nothing++mkMaxWalkSatDimacsHeader Weighted.Header{..}+  = "p wcnf " ++ show numVars ++ " " ++ show numClauses ++ " " ++ show maxWeight

@@ -1,5 +1,5 @@ Name:           satchmo-backends-Version:        1.4+Version:        1.8.0  License:        GPL License-file:	gpl-2.0.txt@@ -14,11 +14,17 @@                 minisat (download from http://minisat.se/ ) 		quantor (download from http://fmv.jku.at/quantor/ ) 		qube    (download from http://www.star.dist.unige.it/~qube/ )-Build-depends: satchmo, process, base, containers+cabal-version: >= 1.6+Build-depends: satchmo == 1.8.*, process, base == 4.* , containers, bytestring Exposed-modules:         Satchmo.Solver.Minisat+        Satchmo.Solver.Pcosat+        Satchmo.Solver.Clasp         Satchmo.Solver.Quantor         Satchmo.Solver.Qube+        Satchmo.Solver.Yices+Other-modules:+        Satchmo.Solver.Internal hs-source-dirs:	. extensions:  build-type: Simple