Clingo.Control

Documentation

data IOSym s a

A monad that serves as witness that data registered with a running solver still exists and can be used.

Instances

MonadSymbol IOSym

Methods

createSignature :: Text -> Natural -> Bool -> IOSym s (Signature s)

createNumber :: Integral a => a -> IOSym s (Symbol s)

createSupremum :: IOSym s (Symbol s)

createInfimum :: IOSym s (Symbol s)

createString :: Text -> IOSym s (Symbol s)

createFunction :: Text -> [Symbol s] -> Bool -> IOSym s (Symbol s)

MonadModel IOSym

Methods

modelType :: Model s -> IOSym s ModelType

modelNumber :: Model s -> IOSym s Natural

modelSymbols :: Model s -> SymbolSelection -> IOSym s [Symbol s]

contains :: Model s -> Symbol s -> IOSym s Bool

costVector :: Model s -> IOSym s [Integer]

optimalityProven :: Model s -> IOSym s Bool

context :: Model s -> IOSym s (SolveControl s)

modelAddClause :: Foldable t => SolveControl s -> t (SymbolicLiteral s) -> IOSym s ()

MonadSolve IOSym

Methods

getResult :: Solver s -> IOSym s SolveResult

getModel :: Solver s -> IOSym s (Maybe (Model s))

solverWait :: Solver s -> Double -> IOSym s ResultReady

solverResume :: Solver s -> IOSym s ()

solverCancel :: Solver s -> IOSym s ()

Monad (IOSym s)

Methods

(>>=) :: IOSym s a -> (a -> IOSym s b) -> IOSym s b

(>>) :: IOSym s a -> IOSym s b -> IOSym s b

return :: a -> IOSym s a

fail :: String -> IOSym s a

Functor (IOSym s)

Methods

fmap :: (a -> b) -> IOSym s a -> IOSym s b

(<$) :: a -> IOSym s b -> IOSym s a

MonadFix (IOSym s)

Methods

mfix :: (a -> IOSym s a) -> IOSym s a

Applicative (IOSym s)

Methods

pure :: a -> IOSym s a

(<*>) :: IOSym s (a -> b) -> IOSym s a -> IOSym s b

(*>) :: IOSym s a -> IOSym s b -> IOSym s b

(<*) :: IOSym s a -> IOSym s b -> IOSym s a

MonadIO (IOSym s)

Methods

liftIO :: IO a -> IOSym s a

Alternative (IOSym s)

Methods

empty :: IOSym s a

(<|>) :: IOSym s a -> IOSym s a -> IOSym s a

some :: IOSym s a -> IOSym s [a]

many :: IOSym s a -> IOSym s [a]

MonadPlus (IOSym s)

Methods

mzero :: IOSym s a

mplus :: IOSym s a -> IOSym s a -> IOSym s a

MonadThrow (IOSym s)

Methods

throwM :: Exception e => e -> IOSym s a

MonadCatch (IOSym s)

Methods

catch :: Exception e => IOSym s a -> (e -> IOSym s a) -> IOSym s a

MonadMask (IOSym s)

Methods

mask :: ((forall a. IOSym s a -> IOSym s a) -> IOSym s b) -> IOSym s b

uninterruptibleMask :: ((forall a. IOSym s a -> IOSym s a) -> IOSym s b) -> IOSym s b

data Clingo s a

The Clingo monad provides a base monad for computations utilizing the clingo answer set solver. It uses an additional type parameter to ensure that values that are managed by the solver can not leave scope.

Instances

MonadSymbol Clingo

Methods

createSignature :: Text -> Natural -> Bool -> Clingo s (Signature s)

createNumber :: Integral a => a -> Clingo s (Symbol s)

createSupremum :: Clingo s (Symbol s)

createInfimum :: Clingo s (Symbol s)

createString :: Text -> Clingo s (Symbol s)

createFunction :: Text -> [Symbol s] -> Bool -> Clingo s (Symbol s)

MonadModel Clingo

Methods

modelType :: Model s -> Clingo s ModelType

modelNumber :: Model s -> Clingo s Natural

modelSymbols :: Model s -> SymbolSelection -> Clingo s [Symbol s]

contains :: Model s -> Symbol s -> Clingo s Bool

costVector :: Model s -> Clingo s [Integer]

optimalityProven :: Model s -> Clingo s Bool

context :: Model s -> Clingo s (SolveControl s)

modelAddClause :: Foldable t => SolveControl s -> t (SymbolicLiteral s) -> Clingo s ()

MonadSolve Clingo

Methods

getResult :: Solver s -> Clingo s SolveResult

getModel :: Solver s -> Clingo s (Maybe (Model s))

solverWait :: Solver s -> Double -> Clingo s ResultReady

solverResume :: Solver s -> Clingo s ()

solverCancel :: Solver s -> Clingo s ()

Monad (Clingo s)

Methods

(>>=) :: Clingo s a -> (a -> Clingo s b) -> Clingo s b

(>>) :: Clingo s a -> Clingo s b -> Clingo s b

return :: a -> Clingo s a

fail :: String -> Clingo s a

Functor (Clingo s)

Methods

fmap :: (a -> b) -> Clingo s a -> Clingo s b

(<$) :: a -> Clingo s b -> Clingo s a

MonadFix (Clingo s)

Methods

mfix :: (a -> Clingo s a) -> Clingo s a

Applicative (Clingo s)

Methods

pure :: a -> Clingo s a

(<*>) :: Clingo s (a -> b) -> Clingo s a -> Clingo s b

(*>) :: Clingo s a -> Clingo s b -> Clingo s b

(<*) :: Clingo s a -> Clingo s b -> Clingo s a

MonadIO (Clingo s)

Methods

liftIO :: IO a -> Clingo s a

Alternative (Clingo s)

Methods

empty :: Clingo s a

(<|>) :: Clingo s a -> Clingo s a -> Clingo s a

some :: Clingo s a -> Clingo s [a]

many :: Clingo s a -> Clingo s [a]

MonadPlus (Clingo s)

Methods

mzero :: Clingo s a

mplus :: Clingo s a -> Clingo s a -> Clingo s a

MonadThrow (Clingo s)

Methods

throwM :: Exception e => e -> Clingo s a

MonadCatch (Clingo s)

Methods

catch :: Exception e => Clingo s a -> (e -> Clingo s a) -> Clingo s a

MonadMask (Clingo s)

Methods

mask :: ((forall a. Clingo s a -> Clingo s a) -> Clingo s b) -> Clingo s b

uninterruptibleMask :: ((forall a. Clingo s a -> Clingo s a) -> Clingo s b) -> Clingo s b

data ClingoWarning

Instances

Show ClingoWarning

Methods

showsPrec :: Int -> ClingoWarning -> ShowS

show :: ClingoWarning -> String

showList :: [ClingoWarning] -> ShowS

Exception ClingoWarning

Methods

toException :: ClingoWarning -> SomeException

fromException :: SomeException -> Maybe ClingoWarning

displayException :: ClingoWarning -> String

warningString :: MonadIO m => ClingoWarning -> m Text

data ClingoSetting

Data type to encapsulate the settings for clingo.

Constructors

ClingoSetting

Fields

• clingoArgs :: [String]
• clingoLogger :: Maybe (ClingoWarning -> Text -> IO ())
• msgLimit :: Natural

defaultClingo :: ClingoSetting

Default settings for clingo. This is like calling clingo with no arguments, and no logger.

withDefaultClingo :: (forall s. Clingo s r) -> IO r

Equal to withClingo defaultClingo

withClingo :: ClingoSetting -> (forall s. Clingo s r) -> IO r

The entry point into a computation utilizing clingo. Inside, a handle to the clingo solver is available, which can not leave scope. By the same mechanism, derived handles cannot be passed out either.

data Part s

A Part is one building block of a logic program in clingo. Parts can be grounded separately and can have arguments, which need to be initialized with the solver.

Constructors

Part

Fields

• partName :: Text
• partParams :: [Symbol s]

loadProgram :: FilePath -> Clingo s ()

Load a logic program from a file.

addProgram

Arguments

:: Foldable t

=> Text

Part Name

-> t Text

Part Arguments

-> Text

Program Code

-> Clingo s ()

Add an ungrounded logic program to the solver as a Text. This function can be used in order to utilize clingo's parser. See parseProgram for when you want to modify the AST before adding it.

ground

Arguments

:: [Part s]

Parts to be grounded

-> Maybe (Location -> Text -> [Symbol s] -> ([Symbol s] -> IO ()) -> IO ())

Callback for injecting symbols

-> Clingo s ()

Ground logic program parts. A callback can be provided to inject symbols when needed.

interrupt :: Clingo s ()

Interrupt the current solve call.

cleanup :: Clingo s ()

Clean up the domains of clingo's grounding component using the solving component's top level assignment.

This function removes atoms from domains that are false and marks atoms as facts that are true. With multi-shot solving, this can result in smaller groundings because less rules have to be instantiated and more simplifications can be applied.

registerPropagator :: Bool -> Propagator s -> Clingo s ()

Register a custom propagator with the solver.

If the sequential flag is set to true, the propagator is called sequentially when solving with multiple threads.

See the Propagation module for more information.

registerUnsafePropagator :: Bool -> IOPropagator s -> Clingo s ()

Like registerPropagator but allows using IOPropagators from Propagation. This function is unsafe!

data Continue

A datatype that can be used to indicate whether solving shall continue or not.

Constructors

Continue

Stop

Instances

Bounded Continue

Methods

minBound :: Continue

maxBound :: Continue

Enum Continue

Methods

succ :: Continue -> Continue

pred :: Continue -> Continue

toEnum :: Int -> Continue

fromEnum :: Continue -> Int

enumFrom :: Continue -> [Continue]

enumFromThen :: Continue -> Continue -> [Continue]

enumFromTo :: Continue -> Continue -> [Continue]

enumFromThenTo :: Continue -> Continue -> Continue -> [Continue]

Eq Continue

Methods

(==) :: Continue -> Continue -> Bool

(/=) :: Continue -> Continue -> Bool

Ord Continue

Methods

compare :: Continue -> Continue -> Ordering

(<) :: Continue -> Continue -> Bool

(<=) :: Continue -> Continue -> Bool

(>) :: Continue -> Continue -> Bool

(>=) :: Continue -> Continue -> Bool

max :: Continue -> Continue -> Continue

min :: Continue -> Continue -> Continue

Read Continue

Methods

readsPrec :: Int -> ReadS Continue

readList :: ReadS [Continue]

readPrec :: ReadPrec Continue

readListPrec :: ReadPrec [Continue]

Show Continue

Methods

showsPrec :: Int -> Continue -> ShowS

show :: Continue -> String

showList :: [Continue] -> ShowS

data SymbolicLiteral s

Constructors

SLPositive (Symbol s)

SLNegative (Symbol s)

Instances

Eq (SymbolicLiteral s)

Methods

(==) :: SymbolicLiteral s -> SymbolicLiteral s -> Bool

(/=) :: SymbolicLiteral s -> SymbolicLiteral s -> Bool

Ord (SymbolicLiteral s)

Methods

compare :: SymbolicLiteral s -> SymbolicLiteral s -> Ordering

(<) :: SymbolicLiteral s -> SymbolicLiteral s -> Bool

(<=) :: SymbolicLiteral s -> SymbolicLiteral s -> Bool

(>) :: SymbolicLiteral s -> SymbolicLiteral s -> Bool

(>=) :: SymbolicLiteral s -> SymbolicLiteral s -> Bool

max :: SymbolicLiteral s -> SymbolicLiteral s -> SymbolicLiteral s

min :: SymbolicLiteral s -> SymbolicLiteral s -> SymbolicLiteral s

Generic (SymbolicLiteral s)

Associated Types

type Rep (SymbolicLiteral s) :: * -> *

Methods

from :: SymbolicLiteral s -> Rep (SymbolicLiteral s) x

to :: Rep (SymbolicLiteral s) x -> SymbolicLiteral s

Hashable (SymbolicLiteral s)

Methods

hashWithSalt :: Int -> SymbolicLiteral s -> Int

hash :: SymbolicLiteral s -> Int

Signed (SymbolicLiteral s)

Methods

positive :: SymbolicLiteral s -> Bool

negative :: SymbolicLiteral s -> Bool

type Rep (SymbolicLiteral s)

type Rep (SymbolicLiteral s) = D1 (MetaData "SymbolicLiteral" "Clingo.Internal.Types" "clingo-0.2.0.0-DzJnCg9nABaE1yAGw8EIsO" False) ((:+:) (C1 (MetaCons "SLPositive" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Symbol s)))) (C1 (MetaCons "SLNegative" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Symbol s)))))

data SolveResult

Constructors

Satisfiable Bool

Unsatisfiable Bool

Interrupted

Instances

Eq SolveResult

Methods

(==) :: SolveResult -> SolveResult -> Bool

(/=) :: SolveResult -> SolveResult -> Bool

Read SolveResult

Methods

readsPrec :: Int -> ReadS SolveResult

readList :: ReadS [SolveResult]

readPrec :: ReadPrec SolveResult

readListPrec :: ReadPrec [SolveResult]

Show SolveResult

Methods

showsPrec :: Int -> SolveResult -> ShowS

show :: SolveResult -> String

showList :: [SolveResult] -> ShowS

Generic SolveResult

Associated Types

type Rep SolveResult :: * -> *

Methods

from :: SolveResult -> Rep SolveResult x

to :: Rep SolveResult x -> SolveResult

NFData SolveResult

Methods

rnf :: SolveResult -> ()

Hashable SolveResult

Methods

hashWithSalt :: Int -> SolveResult -> Int

hash :: SolveResult -> Int

type Rep SolveResult

type Rep SolveResult = D1 (MetaData "SolveResult" "Clingo.Internal.Types" "clingo-0.2.0.0-DzJnCg9nABaE1yAGw8EIsO" False) ((:+:) (C1 (MetaCons "Satisfiable" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) ((:+:) (C1 (MetaCons "Unsatisfiable" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool))) (C1 (MetaCons "Interrupted" PrefixI False) U1)))

exhausted :: SolveResult -> Bool

data Solver s

solve :: SolveMode -> [SymbolicLiteral s] -> Maybe (Maybe (Model s) -> IOSym s Continue) -> Clingo s (Solver s)

Solve the currently grounded logic program enumerating its models. Takes an optional event callback. Since Clingo 5.2, the callback is no longer the only way to interact with models. The callback can still be used to obtain the same functionality as before. It will be called with Nothing when there is no more model.

Furthermore, asynchronous solving and iterative solving is also controlled from this function. See Clingo.Solving for more details.

The Solver must be closed explicitly after use. See withSolver for a bracketed version.

withSolver :: [SymbolicLiteral s] -> (forall s1. Solver s1 -> IOSym s1 r) -> Clingo s r

data SolveMode

Instances

Eq SolveMode

Methods

(==) :: SolveMode -> SolveMode -> Bool

(/=) :: SolveMode -> SolveMode -> Bool

Ord SolveMode

Methods

compare :: SolveMode -> SolveMode -> Ordering

(<) :: SolveMode -> SolveMode -> Bool

(<=) :: SolveMode -> SolveMode -> Bool

(>) :: SolveMode -> SolveMode -> Bool

(>=) :: SolveMode -> SolveMode -> Bool

max :: SolveMode -> SolveMode -> SolveMode

min :: SolveMode -> SolveMode -> SolveMode

Read SolveMode

Methods

readsPrec :: Int -> ReadS SolveMode

readList :: ReadS [SolveMode]

readPrec :: ReadPrec SolveMode

readListPrec :: ReadPrec [SolveMode]

Show SolveMode

Methods

showsPrec :: Int -> SolveMode -> ShowS

show :: SolveMode -> String

showList :: [SolveMode] -> ShowS

pattern SolveModeAsync :: SolveMode

pattern SolveModeYield :: SolveMode

statistics :: Clingo s (Statistics s)

Obtain statistics handle. See Statistics.

programBuilder :: Clingo s (ProgramBuilder s)

Obtain program builder handle. See ProgramBuilding.

configuration :: Clingo s (Configuration s)

Obtain configuration handle. See Configuration.

backend :: Clingo s (Backend s)

Obtain backend handle. See ProgramBuilding.

symbolicAtoms :: Clingo s (SymbolicAtoms s)

Obtain symbolic atoms handle. See SymbolicAtoms.

theoryAtoms :: Clingo s (TheoryAtoms s)

Obtain theory atoms handle. See TheoryAtoms.

data TruthValue

Instances

Eq TruthValue

Methods

(==) :: TruthValue -> TruthValue -> Bool

(/=) :: TruthValue -> TruthValue -> Bool

Ord TruthValue

Methods

compare :: TruthValue -> TruthValue -> Ordering

(<) :: TruthValue -> TruthValue -> Bool

(<=) :: TruthValue -> TruthValue -> Bool

(>) :: TruthValue -> TruthValue -> Bool

(>=) :: TruthValue -> TruthValue -> Bool

max :: TruthValue -> TruthValue -> TruthValue

min :: TruthValue -> TruthValue -> TruthValue

Show TruthValue

Methods

showsPrec :: Int -> TruthValue -> ShowS

show :: TruthValue -> String

showList :: [TruthValue] -> ShowS

pattern TruthTrue :: TruthValue

pattern TruthFalse :: TruthValue

pattern TruthFree :: TruthValue

negateTruth :: TruthValue -> TruthValue

assignExternal :: Symbol s -> TruthValue -> Clingo s ()

Assign a truth value to an external atom.

If the atom does not exist or is not external, this is a noop.

releaseExternal :: Symbol s -> Clingo s ()

Release an external atom.

After this call, an external atom is no longer external and subject to program simplifications. If the atom does not exist or is not external, this is a noop.

getConst :: Text -> Clingo s (Symbol s)

Get the symbol for a constant definition #const name = symbol.

hasConst :: Text -> Clingo s Bool

Check if there is a constant definition for the given constant.

useEnumAssumption :: Bool -> Clingo s ()

Configure how learnt constraints are handled during enumeration.

If the enumeration assumption is enabled, then all information learnt from the solver's various enumeration modes is removed after a solve call. This includes enumeration of cautious or brave consequences, enumeration of answer sets with or without projection, or finding optimal models, as well as clauses added with clingo_solve_control_add_clause().

version :: MonadIO m => m (Int, Int, Int)

Get clingo version.