{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternSynonyms #-}
module Clingo.Control
(
IOSym,
Clingo,
ClingoWarning,
warningString,
ClingoSetting (..),
defaultClingo,
withDefaultClingo,
withClingo,
Part (..),
loadProgram,
addProgram,
ground,
interrupt,
cleanup,
registerPropagator,
registerUnsafePropagator,
Continue (..),
SymbolicLiteral (..),
SolveResult (..),
exhausted,
Solver,
solve,
withSolver,
SolveMode,
pattern SolveModeAsync,
pattern SolveModeYield,
statistics,
programBuilder,
configuration,
backend,
symbolicAtoms,
theoryAtoms,
TruthValue,
pattern TruthTrue,
pattern TruthFalse,
pattern TruthFree,
negateTruth,
assignExternal,
releaseExternal,
getConst,
hasConst,
useEnumAssumption,
version
)
where
import Control.Monad.IO.Class
import Control.Monad.Trans
import Control.Monad.Catch
import Data.Text (Text, pack, unpack)
import Data.Foldable
import Foreign
import Foreign.C
import Numeric.Natural
import qualified Clingo.Raw as Raw
import Clingo.Internal.Utils
import Clingo.Internal.Symbol
import Clingo.Internal.Types
import Clingo.Solving (solverClose)
import Clingo.Propagation (Propagator, propagatorToIO)
data ClingoSetting = ClingoSetting
{ clingoArgs :: [String]
, clingoLogger :: Maybe (ClingoWarning -> Text -> IO ())
, msgLimit :: Natural }
defaultClingo :: ClingoSetting
defaultClingo = ClingoSetting [] Nothing 0
withClingo :: ClingoSetting -> (forall s. Clingo s r) -> IO r
withClingo settings action = do
let argc = length (clingoArgs settings)
argv <- liftIO $ mapM newCString (clingoArgs settings)
ctrl <- marshall1 $ \x ->
withArray argv $ \argvArr -> do
logCB <- maybe (pure nullFunPtr) wrapCBLogger
(clingoLogger settings)
let argv' = case clingoArgs settings of
[] -> nullPtr
_ -> argvArr
Raw.controlNew argv' (fromIntegral argc)
logCB nullPtr (fromIntegral . msgLimit $ settings) x
finally (runClingo ctrl action) $ do
Raw.controlFree ctrl
liftIO $ mapM_ free argv
withDefaultClingo :: (forall s. Clingo s r) -> IO r
withDefaultClingo = withClingo defaultClingo
loadProgram :: FilePath -> Clingo s ()
loadProgram path = askC >>= \ctrl ->
marshall0 (withCString path (Raw.controlLoad ctrl))
addProgram :: Foldable t
=> Text
-> t Text
-> Text
-> Clingo s ()
addProgram name params code = askC >>= \ctrl -> marshall0 $
withCString (unpack name) $ \n ->
withCString (unpack code) $ \c -> do
ptrs <- mapM (newCString . unpack) (toList params)
withArrayLen ptrs $ \s ps ->
Raw.controlAdd ctrl n ps (fromIntegral s) c
data Part s = Part
{ partName :: Text
, partParams :: [Symbol s] }
rawPart :: Part s -> IO Raw.Part
rawPart p = Raw.Part <$> newCString (unpack (partName p))
<*> newArray (map rawSymbol . partParams $ p)
<*> pure (fromIntegral (length . partParams $ p))
freeRawPart :: Raw.Part -> IO ()
freeRawPart p = do
free (Raw.partName p)
free (Raw.partParams p)
ground :: [Part s]
-> Maybe
(Location -> Text -> [Symbol s] -> ([Symbol s] -> IO ()) -> IO ())
-> Clingo s ()
ground parts extFun = askC >>= \ctrl -> marshall0 $ do
rparts <- mapM rawPart parts
res <- withArrayLen rparts $ \len arr -> do
groundCB <- maybe (pure nullFunPtr) wrapCBGround extFun
Raw.controlGround ctrl arr (fromIntegral len) groundCB nullPtr
mapM_ freeRawPart rparts
return res
wrapCBGround :: MonadIO m
=> (Location -> Text -> [Symbol s]
-> ([Symbol s] -> IO ()) -> IO ())
-> m (FunPtr (Raw.CallbackGround ()))
wrapCBGround f = liftIO $ Raw.mkCallbackGround go
where go :: Raw.CallbackGround ()
go loc name arg args _ cbSym _ = reraiseIO $ do
loc' <- fromRawLocation =<< peek loc
name' <- pack <$> peekCString name
syms <- mapM pureSymbol =<< peekArray (fromIntegral args) arg
f loc' name' syms (unwrapCBSymbol $ Raw.getCallbackSymbol cbSym)
unwrapCBSymbol :: Raw.CallbackSymbol () -> ([Symbol s] -> IO ())
unwrapCBSymbol f syms =
withArrayLen (map rawSymbol syms) $ \len arr ->
marshall0 (f arr (fromIntegral len) nullPtr)
interrupt :: Clingo s ()
interrupt = Raw.controlInterrupt =<< askC
cleanup :: Clingo s ()
cleanup = marshall0 . Raw.controlCleanup =<< askC
data Continue = Continue | Stop
deriving (Eq, Show, Ord, Read, Enum, Bounded)
continueBool :: Continue -> Bool
continueBool Continue = True
continueBool Stop = False
solve :: SolveMode -> [SymbolicLiteral s]
-> Maybe (Maybe (Model s) -> IOSym s Continue)
-> Clingo s (Solver s)
solve mode assumptions onEvent = do
ctrl <- askC
Solver <$> marshall1 (go ctrl)
where go ctrl x =
withArrayLen (map rawSymLit assumptions) $ \len arr -> do
eventCB <- maybe (pure nullFunPtr) wrapCBEvent onEvent
Raw.controlSolve
ctrl (rawSolveMode mode)
arr (fromIntegral len) eventCB nullPtr
x
withSolver :: [SymbolicLiteral s]
-> (forall s1. Solver s1 -> IOSym s1 r)
-> Clingo s r
withSolver assumptions f = do
x <- solve SolveModeYield assumptions Nothing
Clingo (lift (f x))
`finally` solverClose x
wrapCBEvent :: MonadIO m
=> (Maybe (Model s) -> IOSym s Continue)
-> m (FunPtr (Raw.CallbackEvent ()))
wrapCBEvent f = liftIO $ Raw.mkCallbackEvent go
where go :: Raw.SolveEvent
-> Ptr Raw.Model
-> Ptr a
-> Ptr Raw.CBool
-> IO Raw.CBool
go ev m _ r = reraiseIO $ do
m' <- case ev of
Raw.SolveEventModel -> Just . Model <$> peek m
Raw.SolveEventFinish -> pure Nothing
_ -> error "wrapCBEvent: Invalid solve event"
poke r . fromBool. continueBool =<< iosym (f m')
statistics :: Clingo s (Statistics s)
statistics = fmap Statistics . marshall1 . Raw.controlStatistics =<< askC
programBuilder :: Clingo s (ProgramBuilder s)
programBuilder = fmap ProgramBuilder . marshall1
. Raw.controlProgramBuilder =<< askC
backend :: Clingo s (Backend s)
backend = fmap Backend . marshall1 . Raw.controlBackend =<< askC
configuration :: Clingo s (Configuration s)
configuration = fmap Configuration . marshall1
. Raw.controlConfiguration =<< askC
symbolicAtoms :: Clingo s (SymbolicAtoms s)
symbolicAtoms = fmap SymbolicAtoms . marshall1
. Raw.controlSymbolicAtoms =<< askC
theoryAtoms :: Clingo s (TheoryAtoms s)
theoryAtoms = fmap TheoryAtoms . marshall1 . Raw.controlTheoryAtoms =<< askC
useEnumAssumption :: Bool -> Clingo s ()
useEnumAssumption b = askC >>= \ctrl ->
marshall0 $ Raw.controlUseEnumAssumption ctrl (fromBool b)
assignExternal :: Symbol s -> TruthValue -> Clingo s ()
assignExternal s t = askC >>= \ctrl ->
marshall0 $ Raw.controlAssignExternal ctrl (rawSymbol s) (rawTruthValue t)
releaseExternal :: Symbol s -> Clingo s ()
releaseExternal s = askC >>= \ctrl ->
marshall0 $ Raw.controlReleaseExternal ctrl (rawSymbol s)
getConst :: Text -> Clingo s (Symbol s)
getConst name = askC >>= \ctrl -> pureSymbol =<< marshall1 (go ctrl)
where go ctrl x = withCString (unpack name) $ \cstr ->
Raw.controlGetConst ctrl cstr x
hasConst :: Text -> Clingo s Bool
hasConst name = askC >>= \ctrl -> toBool <$> marshall1 (go ctrl)
where go ctrl x = withCString (unpack name) $ \cstr ->
Raw.controlHasConst ctrl cstr x
registerPropagator :: Bool -> Propagator s -> Clingo s ()
registerPropagator sequ prop = do
ctrl <- askC
prop' <- rawPropagator . propagatorToIO $ prop
res <- liftIO $ with prop' $ \ptr ->
Raw.controlRegisterPropagator ctrl ptr nullPtr (fromBool sequ)
checkAndThrow res
registerUnsafePropagator :: Bool -> IOPropagator s -> Clingo s ()
registerUnsafePropagator sequ prop = do
ctrl <- askC
prop' <- rawPropagator prop
res <- liftIO $ with prop' $ \ptr ->
Raw.controlRegisterPropagator ctrl ptr nullPtr (fromBool sequ)
checkAndThrow res
version :: MonadIO m => m (Int, Int, Int)
version = do
(a,b,c) <- marshall3V Raw.version
return (fromIntegral a, fromIntegral b, fromIntegral c)