Solving.hs

module Clingo.Solving
(
    ResultReady(..),
    MonadSolve(..),
    solverClose,
    allModels
)
where

import Control.Monad.IO.Class
import Control.Monad.Catch
import Clingo.Model (MonadModel)
import Clingo.Internal.Types
import Foreign.Ptr
import Foreign.Marshal.Utils
import Clingo.Internal.Utils
import qualified Clingo.Raw as Raw

data ResultReady = Ready | NotReady
    deriving (Eq, Show, Read, Ord)

toRR :: Bool -> ResultReady
toRR True  = Ready
toRR False = NotReady

class MonadModel m => MonadSolve m where
    -- | Get the next solve result.
    getResult    :: Solver s -> m s SolveResult

    -- | Get the next model if it exists.
    getModel     :: Solver s -> m s (Maybe (Model s))

    -- | Wait for the specified time to check if the result is ready.
    solverWait   :: Solver s -> Double -> m s ResultReady

    -- | Discard the last model and start search for the next.
    solverResume :: Solver s -> m s ()

    -- | Stop the running search and block until done.
    solverCancel :: Solver s -> m s ()

instance MonadSolve IOSym where
    getResult = getResult'
    getModel = getModel'
    solverWait = solverWait'
    solverResume = solverResume'
    solverCancel = solverCancel'

instance MonadSolve Clingo where
    getResult = getResult'
    getModel = getModel'
    solverWait = solverWait'
    solverResume = solverResume'
    solverCancel = solverCancel'

-- | Convenience method to get all models. Note that this is dependent on the
-- solver configuration!
allModels :: (Monad (m s), MonadSolve m) => Solver s -> m s [Model s]
allModels solver = do
    solverResume solver
    m <- getModel solver
    case m of
        Nothing -> pure []
        Just x  -> (x :) <$> allModels solver

getResult' :: (MonadThrow m, MonadIO m) => Solver s -> m SolveResult
getResult' (Solver s) = fromRawSolveResult <$> marshall1 (Raw.solveHandleGet s)

getModel' :: (MonadThrow m, MonadIO m) => Solver s -> m (Maybe (Model s))
getModel' (Solver s) = do
    m@(Raw.Model x) <- marshall1 $ Raw.solveHandleModel s
    pure $ if x == nullPtr then Nothing else Just (Model m)

solverWait' :: MonadIO m => Solver s -> Double -> m ResultReady
solverWait' (Solver s) timeout = do
    x <- marshall1V $ Raw.solveHandleWait s (realToFrac timeout)
    pure . toRR . toBool $ x

solverResume' :: (MonadThrow m, MonadIO m) => Solver s -> m ()
solverResume' (Solver s) = marshall0 $ Raw.solveHandleResume s

solverCancel' :: (MonadThrow m, MonadIO m) => Solver s -> m ()
solverCancel' (Solver s) = marshall0 $ Raw.solveHandleCancel s

-- | Stops the running search and releases the handle. Blocks until search is
-- stopped.
solverClose :: Solver s -> Clingo s ()
solverClose (Solver s) = marshall0 $ Raw.solveHandleClose s