content: --------------------------------------------------------------------
  -- |
  -- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
  -- License   :  BSD3
  -- Maintainer:  Edward Kmett <ekmett@gmail.com>
  -- Stability :  experimental
  -- Portability: non-portable
  --
  --------------------------------------------------------------------
  module Ersatz.Solver.Common
    ( withTempFiles
    , resultOf
  
    -- * Support for trying many solvers
    , trySolvers
    , NoSolvers(..)
  
    , parseSolution5
    ) where
  
  import Control.Exception (Exception(..), throwIO)
  import Control.Monad.IO.Class
  import Ersatz.Solution
  import System.Exit (ExitCode(..))
  import System.IO.Error (tryIOError)
  import System.IO.Temp (withSystemTempDirectory)
  import Data.IntMap (IntMap)
  import qualified Data.IntMap.Strict as IntMap
  
  withTempFiles :: MonadIO m
                => FilePath  -- ^ Problem file extension including the dot, if any
                -> FilePath  -- ^ Solution file extension including the dot, if any
                -> (FilePath -> FilePath -> IO a) -> m a
  withTempFiles problemExt solutionExt f = liftIO $
    withSystemTempDirectory "ersatz" $ \dir -> do
      let problemPath  = dir ++ "/problem"  ++ problemExt
          solutionPath = dir ++ "/solution" ++ solutionExt
  
      f problemPath solutionPath
  
  resultOf :: ExitCode -> Result
  resultOf (ExitFailure 10) = Satisfied
  resultOf (ExitFailure 20) = Unsatisfied
  resultOf _                = Unsolved
  
  -- | This error is thrown by 'trySolvers' when no solvers are found.
  newtype NoSolvers = NoSolvers [IOError] deriving Show
  
  instance Exception NoSolvers where
    displayException _ = "no ersatz solvers were found"
  
  -- | Try a list of solvers in order. When a solver fails due to
  -- a missing executable the next solver will be tried. Throws
  -- 'NoSolvers' exception if none of the given solvers were installed.
  trySolvers :: [Solver s IO] -> Solver s IO
  trySolvers solvers problem = foldr runSolver noSolvers solvers []
    where
      noSolvers = throwIO . NoSolvers . reverse
  
      runSolver solver next es =
        do res <- tryIOError (solver problem)
           case res of
             Left  e -> next (e:es)
             Right x -> return x
  
  parseSolution5 :: String -> IntMap Bool
  parseSolution5 txt = IntMap.fromList [(abs v, v > 0) | v <- vars, v /= 0]
    where
      vlines = [l | ('v':l) <- lines txt]
      vars = map read (foldMap words vlines)
  