{-# LANGUAGE OverloadedStrings #-}

module Ersatz.Solver.Lingeling
  ( lingeling
  , plingeling
  , treengeling
  , lingelingPath
  , plingelingPath
  , treengelingPath
  ) where

import Control.Monad.IO.Class
  ( MonadIO ( liftIO
            )
  )
import Ersatz.Problem
  ( SAT
  , writeDimacs'
  )
import Ersatz.Solution
  ( Solver
  )
import Ersatz.Solver.Common
  ( resultOf
  , withTempFiles
  , parseSolution5
  )
import System.Process
  ( readProcessWithExitCode
  )

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

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

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

-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes
-- @lingeling@ compatible arguments.
--
-- The 'FilePath' refers to the path to the executable.
lingelingPath :: MonadIO m => FilePath -> Solver SAT m
lingelingPath :: forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
lingelingPath = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
ngelingPath

-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes
-- @plingeling@ compatible arguments.
--
-- The 'FilePath' refers to the path to the executable.
plingelingPath :: MonadIO m => FilePath -> Solver SAT m
plingelingPath :: forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
plingelingPath = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
ngelingPath

-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes
-- @treengeling@ compatible arguments.
--
-- The 'FilePath' refers to the path to the executable.
treengelingPath :: MonadIO m => FilePath -> Solver SAT m
treengelingPath :: forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
treengelingPath = FilePath -> Solver SAT m
forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
ngelingPath

-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes
-- @*ngeling@ compatible arguments.
--
-- The 'FilePath' refers to the path to the executable.
ngelingPath :: MonadIO m => FilePath -> Solver SAT m
ngelingPath :: forall (m :: * -> *). MonadIO m => FilePath -> Solver SAT m
ngelingPath FilePath
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
$
  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 -> SAT -> IO ()
forall (m :: * -> *) t.
(MonadIO m, DIMACS t) =>
FilePath -> t -> m ()
writeDimacs' FilePath
problemPath 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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExitCode -> Result
resultOf ExitCode
exit, IntMap Bool
sol)