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
getResult :: Solver s -> m s SolveResult
getModel :: Solver s -> m s (Maybe (Model s))
solverWait :: Solver s -> Double -> m s ResultReady
solverResume :: Solver s -> m s ()
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'
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
solverClose :: Solver s -> Clingo s ()
solverClose (Solver s) = marshall0 $ Raw.solveHandleClose s