Satyros.CNF.Clause

Documentation

newtype ClauseLike a

Constructors

ClauseLike [a]

Bundled Patterns

pattern Clause :: [Literal] -> Clause

Instances

Show a => Show (ClauseLike a)

Defined in Satyros.CNF.Clause

Methods

showsPrec :: Int -> ClauseLike a -> ShowS

show :: ClauseLike a -> String

showList :: [ClauseLike a] -> ShowS

Semigroup (ClauseLike a)

Defined in Satyros.CNF.Clause

Methods

(<>) :: ClauseLike a -> ClauseLike a -> ClauseLike a

sconcat :: NonEmpty (ClauseLike a) -> ClauseLike a

stimes :: Integral b => b -> ClauseLike a -> ClauseLike a

Monoid (ClauseLike a)

Defined in Satyros.CNF.Clause

Methods

mempty :: ClauseLike a

mappend :: ClauseLike a -> ClauseLike a -> ClauseLike a

mconcat :: [ClauseLike a] -> ClauseLike a

Wrapped (ClauseLike a)

Defined in Satyros.CNF.Clause

Associated Types

type Unwrapped (ClauseLike a)

Methods

_Wrapped' :: Iso' (ClauseLike a) (Unwrapped (ClauseLike a))

ClauseLike a1 ~ t => Rewrapped (ClauseLike a2) t

Defined in Satyros.CNF.Clause

HasClauses (Storage s) (Vector Clause)

Defined in Satyros.DPLL.Storage

Methods

clauses :: Lens' (Storage s) (Vector Clause)

type Unwrapped (ClauseLike a)

Defined in Satyros.CNF.Clause

type Unwrapped (ClauseLike a) = [a]

type Clause = ClauseLike Literal

entriesOfClauseLike :: Iso' (ClauseLike a) [a]

literalsOfClause :: Iso' Clause [Literal]

emptyClause :: Clause -> Bool

unitClause :: Clause -> Bool

maxVariableInClause :: Clause -> Variable