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

-- | 'Solver' for 'SAT' problems that tries to invoke the @cryptominisat@ executable from the @PATH@
cryptominisat :: MonadIO m => Solver SAT m
cryptominisat :: forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat = forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
minisatPath [Char]
"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 :: forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
minisatPath [Char]
path SAT
problem = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a.
MonadIO m =>
[Char] -> [Char] -> ([Char] -> [Char] -> IO a) -> m a
withTempFiles [Char]
".cnf" [Char]
"" forall a b. (a -> b) -> a -> b
$ \[Char]
problemPath [Char]
solutionPath -> do
    forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
problemPath IOMode
WriteMode forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
      Handle -> Builder -> IO ()
hPutBuilder Handle
fh (forall t. DIMACS t => t -> Builder
dimacs SAT
problem)

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

    IntMap Bool
sol <- [Char] -> IO (IntMap Bool)
parseSolutionFile [Char]
solutionPath

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

parseSolutionFile :: FilePath -> IO (IntMap Bool)
parseSolutionFile :: [Char] -> IO (IntMap Bool)
parseSolutionFile [Char]
path = forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle IOException -> IO (IntMap Bool)
handler (ByteString -> IntMap Bool
parseSolution forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO ByteString
B.readFile [Char]
path)
  where
    handler :: IOException -> IO (IntMap Bool)
    handler :: IOException -> IO (IntMap Bool)
handler IOException
_ = forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Eq a => a -> a -> Bool
== ByteString
"SAT" ->
          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 forall a. Eq a => a -> a -> Bool
== Int
v then IntMap Bool
m else forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (forall a. Num a => a -> a
abs Int
v) (Int
vforall a. Ord a => a -> a -> Bool
>Int
0) IntMap Bool
m
                              Maybe (Int, ByteString)
Nothing    -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"parseSolution: Expected an Int, received " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show ByteString
y
                 ) forall a. IntMap a
IntMap.empty [ByteString]
ys
    [ByteString]
_ -> 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 :: forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat5 = forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
cryptominisat5Path [Char]
"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 :: forall (m :: * -> *). MonadIO m => [Char] -> Solver SAT m
cryptominisat5Path [Char]
path SAT
problem = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a.
MonadIO m =>
[Char] -> [Char] -> ([Char] -> [Char] -> IO a) -> m a
withTempFiles [Char]
".cnf" [Char]
"" forall a b. (a -> b) -> a -> b
$ \[Char]
problemPath [Char]
_ -> do
    forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
problemPath IOMode
WriteMode forall a b. (a -> b) -> a -> b
$ \Handle
fh ->
      Handle -> Builder -> IO ()
hPutBuilder Handle
fh (forall t. DIMACS t => t -> Builder
dimacs SAT
problem)

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

    let sol :: IntMap Bool
sol = [Char] -> IntMap Bool
parseSolution5 [Char]
out

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