diff --git a/Satchmo/Solver/Clasp.hs b/Satchmo/Solver/Clasp.hs new file mode 100644 --- /dev/null +++ b/Satchmo/Solver/Clasp.hs @@ -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 + diff --git a/Satchmo/Solver/Internal.hs b/Satchmo/Solver/Internal.hs new file mode 100644 --- /dev/null +++ b/Satchmo/Solver/Internal.hs @@ -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 diff --git a/Satchmo/Solver/Minisat.hs b/Satchmo/Solver/Minisat.hs --- a/Satchmo/Solver/Minisat.hs +++ b/Satchmo/Solver/Minisat.hs @@ -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 diff --git a/Satchmo/Solver/Pcosat.hs b/Satchmo/Solver/Pcosat.hs new file mode 100644 --- /dev/null +++ b/Satchmo/Solver/Pcosat.hs @@ -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 + diff --git a/Satchmo/Solver/Quantor.hs b/Satchmo/Solver/Quantor.hs --- a/Satchmo/Solver/Quantor.hs +++ b/Satchmo/Solver/Quantor.hs @@ -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 diff --git a/Satchmo/Solver/Qube.hs b/Satchmo/Solver/Qube.hs --- a/Satchmo/Solver/Qube.hs +++ b/Satchmo/Solver/Qube.hs @@ -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 diff --git a/Satchmo/Solver/Yices.hs b/Satchmo/Solver/Yices.hs new file mode 100644 --- /dev/null +++ b/Satchmo/Solver/Yices.hs @@ -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 diff --git a/satchmo-backends.cabal b/satchmo-backends.cabal --- a/satchmo-backends.cabal +++ b/satchmo-backends.cabal @@ -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