Safe Haskell | None |
---|---|
Language | Haskell2010 |
High level API for writing propagators.
- data Propagation phase s a
- data PropagationPhase
- data Assignment s
- data Literal s
- class Signed a where
- negateLiteral :: Literal s -> Literal s
- data Propagator s = Propagator {
- 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
- propagatorToIO :: Propagator s -> IOPropagator s
- addWatch :: CanAddWatch phase => Literal s -> Propagation phase s ()
- countThreads :: Propagation Init s Integer
- solverLiteral :: AspifLiteral s -> Propagation Init s (Literal s)
- propSymbolicAtoms :: Propagation Init s (SymbolicAtoms s)
- propTheoryAtoms :: Propagation Init s (TheoryAtoms s)
- data Clause s = Clause [Literal s] ClauseType
- data ClauseType
- addClause :: Clause s -> Propagation Solving s ()
- propagate :: Propagation Solving s ()
- hasWatch :: Literal s -> Propagation Solving s Bool
- removeWatch :: Literal s -> Propagation Solving s ()
- getThreadId :: Propagation Solving s Integer
- newLiteral :: Propagation Solving s (Literal s)
- assignment :: Propagation Solving s (Assignment s)
- decisionLevel :: Assignment s -> Propagation Solving s Natural
- hasConflict :: Assignment s -> Propagation Solving s Bool
- hasLiteral :: Assignment s -> Literal s -> Propagation Solving s Bool
- levelOf :: Assignment s -> Literal s -> Propagation Solving s Natural
- decision :: Assignment s -> Natural -> Propagation Solving s (Literal s)
- isFixed :: Assignment s -> Literal s -> Propagation Solving s Bool
- truthValue :: Assignment s -> Literal s -> Propagation Solving s TruthValue
- data TruthValue
- pattern TruthFree :: TruthValue
- pattern TruthFalse :: TruthValue
- pattern TruthTrue :: TruthValue
- negateTruth :: TruthValue -> TruthValue
Documentation
data Propagation phase s a Source #
A concrete monad for propagators, which observes the invariants stipulated by clingo.
MonadSymbol (Propagation phase) Source # | |
MonadReader (PropagateInit s) (Propagation Init s) Source # | |
MonadReader (PropagateCtrl s) (Propagation Solving s) Source # | |
Monad (Propagation phase s) Source # | |
Functor (Propagation phase s) Source # | |
Applicative (Propagation phase s) Source # | |
MonadIO (Propagation phase s) Source # | |
MonadThrow (Propagation phase s) Source # | |
data PropagationPhase Source #
Propagators can be in one of two phases, initialization and solving.
data Assignment s Source #
negateLiteral :: Literal s -> Literal s Source #
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 Source #
A propagator is defined by four functions. No function is mandatory.
Propagator | |
|
emptyPropagator :: Propagator s Source #
The empty propagator for convenience.
propagatorToIO :: Propagator s -> IOPropagator s Source #
addWatch :: CanAddWatch phase => Literal s -> Propagation phase s () Source #
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 Source #
Obtain the number of solver threads.
solverLiteral :: AspifLiteral s -> Propagation Init s (Literal s) Source #
Convert an AspifLiteral
to a solver Literal
.
propSymbolicAtoms :: Propagation Init s (SymbolicAtoms s) Source #
Obtain a handle to the symbolic atoms, see Symbolic
propTheoryAtoms :: Propagation Init s (TheoryAtoms s) Source #
Obtain a handle to the theory atoms, see Theory
Actions During Solving
data ClauseType Source #
ClauseLearnt | |
ClauseVolatile Bool | Bool determines static |
ClauseStatic |
addClause :: Clause s -> Propagation Solving s () Source #
Add a clause. This call might result in termination of the propagation function, when backjumping is necessary.
propagate :: Propagation Solving s () Source #
Propagate implied literals from added clauses. Might result in backjumping and hence termination of the propagation.
removeWatch :: Literal s -> Propagation Solving s () Source #
Stop watching a literal.
getThreadId :: Propagation Solving s Integer Source #
Get the thread id of the calling solver thread.
newLiteral :: Propagation Solving s (Literal s) Source #
Introduce a new literal to the solver.
assignment :: Propagation Solving s (Assignment s) Source #
Obtain the current (partial) assignment.
Assignment
decisionLevel :: Assignment s -> Propagation Solving s Natural Source #
Get the current decision level.
hasConflict :: Assignment s -> Propagation Solving s Bool Source #
Determine whether assignment has a conflict.
hasLiteral :: Assignment s -> Literal s -> Propagation Solving s Bool Source #
Determine whether a literal is part of an assignment.
levelOf :: Assignment s -> Literal s -> Propagation Solving s Natural Source #
Find the decision level of a given literal in an assignment.
decision :: Assignment s -> Natural -> Propagation Solving s (Literal s) Source #
Determine the decision literal given a decision level.
isFixed :: Assignment s -> Literal s -> Propagation Solving s Bool Source #
Check if a literal has a fixed truth value.
truthValue :: Assignment s -> Literal s -> Propagation Solving s TruthValue Source #
Obtain the truth value of a literal
Truth Values
pattern TruthFree :: TruthValue Source #
pattern TruthFalse :: TruthValue Source #
pattern TruthTrue :: TruthValue Source #
negateTruth :: TruthValue -> TruthValue Source #