Clingo.Internal.Propagation

Documentation

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)))

Propagation Handles and Types

data PropagateInit s

Instances

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

data PropagateCtrl s

Instances

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

data IOPropagator s

Constructors

IOPropagator

Fields

• propagatorInit :: Maybe (PropagateInit s -> IO ())
• propagatorPropagate :: Maybe (PropagateCtrl s -> [Literal s] -> IO ())
• propagatorUndo :: Maybe (PropagateCtrl s -> [Literal s] -> IO ())
• propagatorCheck :: Maybe (PropagateCtrl s -> IO ())

data PropagationStop

Constructors

Continue

Stop

Instances

Bounded PropagationStop

Methods

minBound :: PropagationStop

maxBound :: PropagationStop

Enum PropagationStop

Methods

succ :: PropagationStop -> PropagationStop

pred :: PropagationStop -> PropagationStop

toEnum :: Int -> PropagationStop

fromEnum :: PropagationStop -> Int

enumFrom :: PropagationStop -> [PropagationStop]

enumFromThen :: PropagationStop -> PropagationStop -> [PropagationStop]

enumFromTo :: PropagationStop -> PropagationStop -> [PropagationStop]

enumFromThenTo :: PropagationStop -> PropagationStop -> PropagationStop -> [PropagationStop]

Eq PropagationStop

Methods

(==) :: PropagationStop -> PropagationStop -> Bool

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

Ord PropagationStop

Methods

compare :: PropagationStop -> PropagationStop -> Ordering

(<) :: PropagationStop -> PropagationStop -> Bool

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

(>) :: PropagationStop -> PropagationStop -> Bool

(>=) :: PropagationStop -> PropagationStop -> Bool

max :: PropagationStop -> PropagationStop -> PropagationStop

min :: PropagationStop -> PropagationStop -> PropagationStop

Read PropagationStop

Methods

readsPrec :: Int -> ReadS PropagationStop

readList :: ReadS [PropagationStop]

readPrec :: ReadPrec PropagationStop

readListPrec :: ReadPrec [PropagationStop]

Show PropagationStop

Methods

showsPrec :: Int -> PropagationStop -> ShowS

show :: PropagationStop -> String

showList :: [PropagationStop] -> ShowS

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

Assignment

decisionLevel :: MonadIO m => Assignment s -> m Natural

Get the current decision level.

hasConflict :: MonadIO m => Assignment s -> m Bool

Determine whether assignment has a conflict.

hasLiteral :: MonadIO m => Assignment s -> Literal s -> m Bool

Determine whether a literal is part of an assignment.

levelOf :: (MonadIO m, MonadThrow m) => Assignment s -> Literal s -> m Natural

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

decision :: (MonadIO m, MonadThrow m) => Assignment s -> Natural -> m (Literal s)

Determine the decision literal given a decision level.

isFixed :: (MonadIO m, MonadThrow m) => Assignment s -> Literal s -> m Bool

Check if a literal has a fixed truth value.

truthValue :: (MonadIO m, MonadThrow m) => Assignment s -> Literal s -> m TruthValue

Obtain the truth value of a literal

Clauses

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

Propagation

assignment :: MonadIO m => PropagateCtrl s -> m (Assignment s)

addClause :: (MonadIO m, MonadThrow m) => PropagateCtrl s -> Clause s -> m PropagationStop

addLiteral :: (MonadIO m, MonadThrow m) => PropagateCtrl s -> m (Literal s)

addWatch :: (MonadIO m, MonadThrow m) => PropagateCtrl s -> Literal s -> m ()

hasWatch :: MonadIO m => PropagateCtrl s -> Literal s -> m Bool

removeWatch :: MonadIO m => PropagateCtrl s -> Literal s -> m ()

propagate :: (MonadIO m, MonadThrow m) => PropagateCtrl s -> m PropagationStop

getThreadId :: MonadIO m => PropagateCtrl s -> m Integer

Initialization

initAddWatch :: (MonadIO m, MonadThrow m) => PropagateInit s -> Literal s -> m ()

countThreads :: MonadIO m => PropagateInit s -> m Integer

solverLiteral :: (MonadIO m, MonadThrow m) => PropagateInit s -> AspifLiteral s -> m (Literal s)

symbolicAtoms :: (MonadIO m, MonadThrow m) => PropagateInit s -> m (SymbolicAtoms s)

theoryAtoms :: (MonadIO m, MonadThrow m) => PropagateInit s -> m (TheoryAtoms s)