ToySolver.SAT.Formula

Boolean formula type

data Formula where

Arbitrary formula not restricted to CNF

Bundled Patterns

pattern Atom :: Lit -> Formula

pattern And :: [Formula] -> Formula

pattern Or :: [Formula] -> Formula

pattern Not :: Formula -> Formula

pattern Equiv :: Formula -> Formula -> Formula

pattern Imply :: Formula -> Formula -> Formula

pattern ITE :: Formula -> Formula -> Formula -> Formula

Instances

FromJSON Formula

Defined in ToySolver.SAT.Formula

Methods

parseJSON :: Value -> Parser Formula

parseJSONList :: Value -> Parser [Formula]

omittedField :: Maybe Formula

ToJSON Formula

Defined in ToySolver.SAT.Formula

Methods

toJSON :: Formula -> Value

toEncoding :: Formula -> Encoding

toJSONList :: [Formula] -> Value

toEncodingList :: [Formula] -> Encoding

omitField :: Formula -> Bool

Read Formula

Defined in ToySolver.SAT.Formula

Methods

readsPrec :: Int -> ReadS Formula

readList :: ReadS [Formula]

readPrec :: ReadPrec Formula

readListPrec :: ReadPrec [Formula]

Show Formula

Defined in ToySolver.SAT.Formula

Methods

showsPrec :: Int -> Formula -> ShowS

show :: Formula -> String

showList :: [Formula] -> ShowS

Eq Formula

Defined in ToySolver.SAT.Formula

Methods

(==) :: Formula -> Formula -> Bool

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

Hashable Formula

Defined in ToySolver.SAT.Formula

Methods

hashWithSalt :: Int -> Formula -> Int

hash :: Formula -> Int

Interned Formula

Defined in ToySolver.SAT.Formula

Associated Types

data Description Formula

type Uninterned Formula

Methods

describe :: Uninterned Formula -> Description Formula

identify :: Id -> Uninterned Formula -> Formula

seedIdentity :: p Formula -> Id

cacheWidth :: p Formula -> Int

modifyAdvice :: IO Formula -> IO Formula

cache :: Cache Formula

Uninternable Formula

Defined in ToySolver.SAT.Formula

Methods

unintern :: Formula -> Uninterned Formula

Boolean Formula

Defined in ToySolver.SAT.Formula

Methods

(.=>.) :: Formula -> Formula -> Formula

(.<=>.) :: Formula -> Formula -> Formula

Complement Formula

Defined in ToySolver.SAT.Formula

Methods

notB :: Formula -> Formula

MonotoneBoolean Formula

Defined in ToySolver.SAT.Formula

Methods

true :: Formula

false :: Formula

(.&&.) :: Formula -> Formula -> Formula

(.||.) :: Formula -> Formula -> Formula

andB :: [Formula] -> Formula

orB :: [Formula] -> Formula

IfThenElse Formula Formula

Defined in ToySolver.SAT.Formula

Methods

ite :: Formula -> Formula -> Formula -> Formula

Generic (Description Formula)

Defined in ToySolver.SAT.Formula

Associated Types

type Rep (Description Formula) :: Type -> Type

Methods

from :: Description Formula -> Rep (Description Formula) x

to :: Rep (Description Formula) x -> Description Formula

Eq (Description Formula)

Defined in ToySolver.SAT.Formula

Methods

(==) :: Description Formula -> Description Formula -> Bool

(/=) :: Description Formula -> Description Formula -> Bool

Hashable (Description Formula)

Defined in ToySolver.SAT.Formula

Methods

hashWithSalt :: Int -> Description Formula -> Int

hash :: Description Formula -> Int

data Description Formula

Defined in ToySolver.SAT.Formula

data Description Formula

• = DAtom Lit
• | DAnd [Id]
• | DOr [Id]
• | DNot Id
• | DImply Id Id
• | DEquiv Id Id
• | DITE Id Id Id

type Uninterned Formula

Defined in ToySolver.SAT.Formula

type Uninterned Formula

type Rep (Description Formula)

Defined in ToySolver.SAT.Formula

type Rep (Description Formula) = D1 ('MetaData "Description" "ToySolver.SAT.Formula" "toysolver-0.9.0-87cq5PU0Vno4kXxl9oPWHg" 'False) ((C1 ('MetaCons "DAtom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lit)) :+: (C1 ('MetaCons "DAnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Id])) :+: C1 ('MetaCons "DOr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Id])))) :+: ((C1 ('MetaCons "DNot" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id)) :+: C1 ('MetaCons "DImply" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id))) :+: (C1 ('MetaCons "DEquiv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id)) :+: C1 ('MetaCons "DITE" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Id))))))

fold :: Boolean b => (Lit -> b) -> Formula -> b

evalFormula :: IModel m => m -> Formula -> Bool

simplify :: Formula -> Formula