Clingo.Propagation

High level API for writing propagators.

Documentation

data Propagation phase s a

A concrete monad for propagators, which observes the invariants stipulated by clingo.

Instances

MonadSymbol (Propagation phase)

Methods

createSignature :: Text -> Natural -> Bool -> Propagation phase s (Signature s)

createNumber :: Integral a => a -> Propagation phase s (Symbol s)

createSupremum :: Propagation phase s (Symbol s)

createInfimum :: Propagation phase s (Symbol s)

createString :: Text -> Propagation phase s (Symbol s)

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

MonadReader (PropagateInit s) (Propagation Init s)

Methods

ask :: Propagation Init s (PropagateInit s)

local :: (PropagateInit s -> PropagateInit s) -> Propagation Init s a -> Propagation Init s a

reader :: (PropagateInit s -> a) -> Propagation Init s a

MonadReader (PropagateCtrl s) (Propagation Solving s)

Methods

ask :: Propagation Solving s (PropagateCtrl s)

local :: (PropagateCtrl s -> PropagateCtrl s) -> Propagation Solving s a -> Propagation Solving s a

reader :: (PropagateCtrl s -> a) -> Propagation Solving s a

Monad (Propagation phase s)

Methods

(>>=) :: Propagation phase s a -> (a -> Propagation phase s b) -> Propagation phase s b

(>>) :: Propagation phase s a -> Propagation phase s b -> Propagation phase s b

return :: a -> Propagation phase s a

fail :: String -> Propagation phase s a

Functor (Propagation phase s)

Methods

fmap :: (a -> b) -> Propagation phase s a -> Propagation phase s b

(<$) :: a -> Propagation phase s b -> Propagation phase s a

Applicative (Propagation phase s)

Methods

pure :: a -> Propagation phase s a

(<*>) :: Propagation phase s (a -> b) -> Propagation phase s a -> Propagation phase s b

(*>) :: Propagation phase s a -> Propagation phase s b -> Propagation phase s b

(<*) :: Propagation phase s a -> Propagation phase s b -> Propagation phase s a

MonadIO (Propagation phase s)

Methods

liftIO :: IO a -> Propagation phase s a

MonadThrow (Propagation phase s)

Methods

throwM :: Exception e => e -> Propagation phase s a

data PropagationPhase

Propagators can be in one of two phases, initialization and solving.

Constructors

Init

Solving

data Assignment s

data Literal s

Instances

Eq (Literal s)

Methods

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

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

Ord (Literal s)

Methods

compare :: Literal s -> Literal s -> Ordering

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

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

(>) :: Literal s -> Literal s -> Bool

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

max :: Literal s -> Literal s -> Literal s

min :: Literal s -> Literal s -> Literal s

Show (Literal s)

Methods

showsPrec :: Int -> Literal s -> ShowS

show :: Literal s -> String

showList :: [Literal s] -> ShowS

Generic (Literal s)

Associated Types

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

Methods

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

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

NFData (Literal s)

Methods

rnf :: Literal s -> ()

Hashable (Literal s)

Methods

hashWithSalt :: Int -> Literal s -> Int

hash :: Literal s -> Int

Signed (Literal s)

Methods

positive :: Literal s -> Bool

negative :: Literal s -> Bool

type Rep (Literal s)

type Rep (Literal s) = D1 (MetaData "Literal" "Clingo.Internal.Types" "clingo-0.2.0.0-DzJnCg9nABaE1yAGw8EIsO" True) (C1 (MetaCons "Literal" PrefixI True) (S1 (MetaSel (Just Symbol "rawLiteral") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Literal)))

class Signed a where

Methods

positive :: a -> Bool

negative :: a -> Bool

Instances

Signed Bool

Methods

positive :: Bool -> Bool

negative :: Bool -> Bool

Signed (AspifLiteral s)

Methods

positive :: AspifLiteral s -> Bool

negative :: AspifLiteral s -> Bool

Signed (Literal s)

Methods

positive :: Literal s -> Bool

negative :: Literal s -> Bool

Signed (Signature s)

Methods

positive :: Signature s -> Bool

negative :: Signature s -> Bool

Signed (SymbolicLiteral s)

Methods

positive :: SymbolicLiteral s -> Bool

negative :: SymbolicLiteral s -> Bool

Signed (FunctionSymbol s)

Methods

positive :: FunctionSymbol s -> Bool

negative :: FunctionSymbol s -> Bool

negateLiteral :: Literal s -> Literal s

A propagator is defined by four functions. The first is executed during the initialization phase. The remaining three are called during solving, depending on how the propagator is initialized.

Initialization: This function is called once before each solving step. It is used to map relevant program literals to solver literals, add watches for solver literals, and initialize the data structures used during propagation. This is the last point to access symbolic and theory atoms. Once the search has started, they are no longer accessible.

Propagation: Can be used to add conflicts in order to propagate solver literals.

Undo: Is called on backjumping and can be used to synchronize internal data structures of the propagator.

Check: Can be used to check whether an assignment is valid.

data Propagator s

A propagator is defined by four functions. No function is mandatory.

Constructors

Propagator

Fields

• propInit :: Maybe (Propagation Init s ())
• propPropagate :: Maybe ([Literal s] -> Propagation Solving s ())
• propUndo :: Maybe ([Literal s] -> Propagation Solving s ())
• propCheck :: Maybe (Propagation Solving s ())

emptyPropagator :: Propagator s

The empty propagator for convenience.

propagatorToIO :: Propagator s -> IOPropagator s

addWatch :: CanAddWatch phase => Literal s -> Propagation phase s ()

Watches can be added in any phase of the propagation. The propagate and undo functions will only be called on changes to watched literals!

Initialization

countThreads :: Propagation Init s Integer

Obtain the number of solver threads.

solverLiteral :: AspifLiteral s -> Propagation Init s (Literal s)

Convert an AspifLiteral to a solver Literal.

propSymbolicAtoms :: Propagation Init s (SymbolicAtoms s)

Obtain a handle to the symbolic atoms, see Symbolic

propTheoryAtoms :: Propagation Init s (TheoryAtoms s)

Obtain a handle to the theory atoms, see Theory

Actions During Solving

data Clause s

Constructors

Clause [Literal s] ClauseType

Instances

Show (Clause s)

Methods

showsPrec :: Int -> Clause s -> ShowS

show :: Clause s -> String

showList :: [Clause s] -> ShowS

data ClauseType

Constructors

ClauseLearnt

ClauseVolatile Bool

Bool determines static

ClauseStatic

Instances

Eq ClauseType

Methods

(==) :: ClauseType -> ClauseType -> Bool

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

Ord ClauseType

Methods

compare :: ClauseType -> ClauseType -> Ordering

(<) :: ClauseType -> ClauseType -> Bool

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

(>) :: ClauseType -> ClauseType -> Bool

(>=) :: ClauseType -> ClauseType -> Bool

max :: ClauseType -> ClauseType -> ClauseType

min :: ClauseType -> ClauseType -> ClauseType

Show ClauseType

Methods

showsPrec :: Int -> ClauseType -> ShowS

show :: ClauseType -> String

showList :: [ClauseType] -> ShowS

addClause :: Clause s -> Propagation Solving s ()

Add a clause. This call might result in termination of the propagation function, when backjumping is necessary.

propagate :: Propagation Solving s ()

Propagate implied literals from added clauses. Might result in backjumping and hence termination of the propagation.

hasWatch :: Literal s -> Propagation Solving s Bool

Check whether a Literal is watched.

removeWatch :: Literal s -> Propagation Solving s ()

Stop watching a literal.

getThreadId :: Propagation Solving s Integer

Get the thread id of the calling solver thread.

newLiteral :: Propagation Solving s (Literal s)

Introduce a new literal to the solver.

assignment :: Propagation Solving s (Assignment s)

Obtain the current (partial) assignment.

Assignment

decisionLevel :: Assignment s -> Propagation Solving s Natural

Get the current decision level.

hasConflict :: Assignment s -> Propagation Solving s Bool

Determine whether assignment has a conflict.

hasLiteral :: Assignment s -> Literal s -> Propagation Solving s Bool

Determine whether a literal is part of an assignment.

levelOf :: Assignment s -> Literal s -> Propagation Solving s Natural

Find the decision level of a given literal in an assignment.

decision :: Assignment s -> Natural -> Propagation Solving s (Literal s)

Determine the decision literal given a decision level.

isFixed :: Assignment s -> Literal s -> Propagation Solving s Bool

Check if a literal has a fixed truth value.

truthValue :: Assignment s -> Literal s -> Propagation Solving s TruthValue

Obtain the truth value of a literal

Truth Values

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 TruthFree :: TruthValue

pattern TruthFalse :: TruthValue

pattern TruthTrue :: TruthValue

negateTruth :: TruthValue -> TruthValue