Ersatz.Internal.Literal

Documentation

newtype Literal

A naked possibly-negated Atom, present in the target Solver.

The literals -1 and 1 are dedicated for the constant False and the constant True respectively.

Constructors

Literal

Fields

• literalId :: Int

Instances

Eq Literal

Methods

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

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

Ord Literal

Methods

compare :: Literal -> Literal -> Ordering

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

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

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

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

max :: Literal -> Literal -> Literal

min :: Literal -> Literal -> Literal

Show Literal

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

Codec Literal

Associated Types

type Decoded Literal :: *

Methods

decode :: MonadPlus f => Solution -> Literal -> f (Decoded Literal)

encode :: Decoded Literal -> Literal

Variable Literal

Methods

literally :: (HasSAT s, MonadState s m) => m Literal -> m Literal

type Decoded Literal

type Decoded Literal = Bool

negateLiteral :: Literal -> Literal

literalFalse :: Literal

The False constant. The literal -1 is dedicated for it.

literalTrue :: Literal

The True constant. The literal 1 is dedicated for it.