--------------------------------------------------------------------
-- |
-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------

{-# language OverloadedStrings #-}

module Ersatz.Solver.Minisat
  ( minisat
  , cryptominisat
  , minisatPath
  , cryptominisat5
  , cryptominisat5Path
  , anyminisat
  ) where

import Data.ByteString.Builder
import Control.Exception (IOException, handle)
import Control.Monad.IO.Class
import Data.IntMap (IntMap)
import Ersatz.Problem
import Ersatz.Solution
import Ersatz.Solver.Common
import qualified Data.IntMap.Strict as IntMap
import System.IO
import System.Process (readProcessWithExitCode)

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 :: Solver SAT IO
anyminisat = [Solver SAT IO] -> Solver SAT IO
forall s. [Solver s IO] -> Solver s IO
trySolvers [Solver SAT IO
forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat5, Solver SAT IO
forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat, Solver SAT IO
forall (m :: * -> *). MonadIO m => Solver SAT m
minisat]

-- | 'Solver' for 'SAT' problems that tries to invoke the @minisat@ executable from the @PATH@
minisat :: MonadIO m => Solver SAT m
minisat :: Solver SAT m
minisat = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
minisatPath FilePath
"minisat"

-- | 'Solver' for 'SAT' problems that tries to invoke the @cryptominisat@ executable from the @PATH@
cryptominisat :: MonadIO m => Solver SAT m
cryptominisat :: Solver SAT m
cryptominisat = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
minisatPath FilePath
"cryptominisat"

-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @minisat@ compatible arguments.
--
-- The 'FilePath' refers to the path to the executable.
minisatPath :: MonadIO m => FilePath -> Solver SAT m
minisatPath :: FilePath -> Solver SAT m
minisatPath FilePath
path SAT
problem = IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Result, IntMap Bool) -> m (Result, IntMap Bool))
-> IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$
  FilePath
-> FilePath
-> (FilePath -> FilePath -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall (m :: * -> *) a.
MonadIO m =>
FilePath -> FilePath -> (FilePath -> FilePath -> IO a) -> m a
withTempFiles FilePath
".cnf" FilePath
"" ((FilePath -> FilePath -> IO (Result, IntMap Bool))
 -> IO (Result, IntMap Bool))
-> (FilePath -> FilePath -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$ \FilePath
problemPath FilePath
solutionPath -> do
    FilePath -> IOMode -> (Handle -> IO ()) -> IO ()
forall r. FilePath -> IOMode -> (Handle -> IO r) -> IO r
withFile FilePath
problemPath IOMode
WriteMode ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
      Handle -> Builder -> IO ()
hPutBuilder Handle
fh (SAT -> Builder
forall t. DIMACS t => t -> Builder
dimacs SAT
problem)

    (ExitCode
exit, FilePath
_out, FilePath
_err) <-
      FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode FilePath
path [FilePath
problemPath, FilePath
solutionPath] []

    IntMap Bool
sol <- FilePath -> IO (IntMap Bool)
parseSolutionFile FilePath
solutionPath

    (Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> Result
resultOf ExitCode
exit, IntMap Bool
sol)

parseSolutionFile :: FilePath -> IO (IntMap Bool)
parseSolutionFile :: FilePath -> IO (IntMap Bool)
parseSolutionFile FilePath
path = (IOException -> IO (IntMap Bool))
-> IO (IntMap Bool) -> IO (IntMap Bool)
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle IOException -> IO (IntMap Bool)
handler (ByteString -> IntMap Bool
parseSolution (ByteString -> IntMap Bool) -> IO ByteString -> IO (IntMap Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO ByteString
B.readFile FilePath
path)
  where
    handler :: IOException -> IO (IntMap Bool)
    handler :: IOException -> IO (IntMap Bool)
handler IOException
_ = IntMap Bool -> IO (IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return IntMap Bool
forall a. IntMap a
IntMap.empty

parseSolution :: B.ByteString -> IntMap Bool
parseSolution :: ByteString -> IntMap Bool
parseSolution ByteString
s =
  case ByteString -> [ByteString]
B.words ByteString
s of
    ByteString
x : [ByteString]
ys | ByteString
x ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
"SAT" ->
          (IntMap Bool -> ByteString -> IntMap Bool)
-> IntMap Bool -> [ByteString] -> IntMap Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ( \ IntMap Bool
m ByteString
y -> case ByteString -> Maybe (Int, ByteString)
B.readInt ByteString
y of
                              Just (Int
v,ByteString
_) -> if Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v then IntMap Bool
m else Int -> Bool -> IntMap Bool -> IntMap Bool
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Int -> Int
forall a. Num a => a -> a
abs Int
v) (Int
vInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
0) IntMap Bool
m
                              Maybe (Int, ByteString)
Nothing    -> FilePath -> IntMap Bool
forall a. HasCallStack => FilePath -> a
error (FilePath -> IntMap Bool) -> FilePath -> IntMap Bool
forall a b. (a -> b) -> a -> b
$ FilePath
"parseSolution: Expected an Int, received " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ByteString -> FilePath
forall a. Show a => a -> FilePath
show ByteString
y
                 ) IntMap Bool
forall a. IntMap a
IntMap.empty [ByteString]
ys
    [ByteString]
_ -> IntMap Bool
forall a. IntMap a
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 :: Solver SAT m
cryptominisat5 = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
cryptominisat5Path FilePath
"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 :: FilePath -> Solver SAT m
cryptominisat5Path FilePath
path SAT
problem = IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Result, IntMap Bool) -> m (Result, IntMap Bool))
-> IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$
  FilePath
-> FilePath
-> (FilePath -> FilePath -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall (m :: * -> *) a.
MonadIO m =>
FilePath -> FilePath -> (FilePath -> FilePath -> IO a) -> m a
withTempFiles FilePath
".cnf" FilePath
"" ((FilePath -> FilePath -> IO (Result, IntMap Bool))
 -> IO (Result, IntMap Bool))
-> (FilePath -> FilePath -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$ \FilePath
problemPath FilePath
_ -> do
    FilePath -> IOMode -> (Handle -> IO ()) -> IO ()
forall r. FilePath -> IOMode -> (Handle -> IO r) -> IO r
withFile FilePath
problemPath IOMode
WriteMode ((Handle -> IO ()) -> IO ()) -> (Handle -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
      Handle -> Builder -> IO ()
hPutBuilder Handle
fh (SAT -> Builder
forall t. DIMACS t => t -> Builder
dimacs SAT
problem)

    (ExitCode
exit, FilePath
out, FilePath
_err) <-
      FilePath
-> [FilePath] -> FilePath -> IO (ExitCode, FilePath, FilePath)
readProcessWithExitCode FilePath
path [FilePath
problemPath] []

    let sol :: IntMap Bool
sol = FilePath -> IntMap Bool
parseSolution5 FilePath
out

    (Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> Result
resultOf ExitCode
exit, IntMap Bool
sol)