--------------------------------------------------------------------
-- |
-- 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 Control.Exception (IOException, handle)
import Control.Monad.IO.Class
import Data.IntMap (IntMap)
import Ersatz.Problem ( SAT, writeDimacs' )
import Ersatz.Solution
import Ersatz.Solver.Common
import qualified Data.IntMap.Strict as IntMap
import System.Process (readProcessWithExitCode)

import qualified Data.ByteString.Char8 as B
import qualified Data.List as 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 :: forall (m :: * -> *). MonadIO m => Solver SAT m
minisat = [Char] -> Solver SAT m
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 = [Char] -> Solver SAT m
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 = IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall a. IO a -> m a
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
$
  [Char]
-> [Char]
-> ([Char] -> [Char] -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall (m :: * -> *) a.
MonadIO m =>
[Char] -> [Char] -> ([Char] -> [Char] -> IO a) -> m a
withTempFiles [Char]
".cnf" [Char]
"" (([Char] -> [Char] -> IO (Result, IntMap Bool))
 -> IO (Result, IntMap Bool))
-> ([Char] -> [Char] -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$ \[Char]
problemPath [Char]
solutionPath -> do
    [Char] -> SAT -> IO ()
forall (m :: * -> *) t.
(MonadIO m, DIMACS t) =>
[Char] -> t -> m ()
writeDimacs' [Char]
problemPath 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

    (Result, IntMap Bool) -> IO (Result, IntMap Bool)
forall a. a -> IO a
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 = (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
<$> [Char] -> IO ByteString
B.readFile [Char]
path)
  where
    handler :: IOException -> IO (IntMap Bool)
    handler :: IOException -> IO (IntMap Bool)
handler IOException
_ = IntMap Bool -> IO (IntMap Bool)
forall a. a -> IO a
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 b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.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    -> [Char] -> IntMap Bool
forall a. HasCallStack => [Char] -> a
error ([Char] -> IntMap Bool) -> [Char] -> IntMap Bool
forall a b. (a -> b) -> a -> b
$ [Char]
"parseSolution: Expected an Int, received " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ByteString -> [Char]
forall a. Show a => a -> [Char]
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 :: forall (m :: * -> *). MonadIO m => Solver SAT m
cryptominisat5 = [Char] -> Solver SAT m
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 = IO (Result, IntMap Bool) -> m (Result, IntMap Bool)
forall a. IO a -> m a
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
$
  [Char]
-> [Char]
-> ([Char] -> [Char] -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall (m :: * -> *) a.
MonadIO m =>
[Char] -> [Char] -> ([Char] -> [Char] -> IO a) -> m a
withTempFiles [Char]
".cnf" [Char]
"" (([Char] -> [Char] -> IO (Result, IntMap Bool))
 -> IO (Result, IntMap Bool))
-> ([Char] -> [Char] -> IO (Result, IntMap Bool))
-> IO (Result, IntMap Bool)
forall a b. (a -> b) -> a -> b
$ \[Char]
problemPath [Char]
_ -> do
    [Char] -> SAT -> IO ()
forall (m :: * -> *) t.
(MonadIO m, DIMACS t) =>
[Char] -> t -> m ()
writeDimacs' [Char]
problemPath 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

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