toysolver-0.8.1: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Copyright(c) Masahiro Sakai 2012-2021
LicenseBSD-style
Maintainermasahiro.sakai@gmail.com
Stabilityprovisional
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010
Extensions
  • MonoLocalBinds
  • TypeFamilies
  • ViewPatterns
  • DeriveGeneric
  • TypeSynonymInstances
  • FlexibleInstances
  • ConstrainedClassMethods
  • MultiParamTypeClasses
  • KindSignatures
  • ExplicitNamespaces
  • PatternSynonyms

ToySolver.SAT.Formula

Description

 
Synopsis

Boolean formula type

data Formula where Source #

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

Instances details
Read Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

readsPrec :: Int -> ReadS Formula #

readList :: ReadS [Formula] #

readPrec :: ReadPrec Formula #

readListPrec :: ReadPrec [Formula] #

Show Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

showsPrec :: Int -> Formula -> ShowS #

show :: Formula -> String #

showList :: [Formula] -> ShowS #

Eq Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

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

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

Hashable Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

hashWithSalt :: Int -> Formula -> Int #

hash :: Formula -> Int #

Interned Formula Source # 
Instance details

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 Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

unintern :: Formula -> Uninterned Formula #

Boolean Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

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

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

Complement Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

notB :: Formula -> Formula Source #

MonotoneBoolean Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

true :: Formula Source #

false :: Formula Source #

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

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

andB :: [Formula] -> Formula Source #

orB :: [Formula] -> Formula Source #

IfThenElse Formula Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

ite :: Formula -> Formula -> Formula -> Formula Source #

Generic (Description Formula) Source # 
Instance details

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) Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

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

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

Hashable (Description Formula) Source # 
Instance details

Defined in ToySolver.SAT.Formula

Methods

hashWithSalt :: Int -> Description Formula -> Int #

hash :: Description Formula -> Int #

data Description Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

data Description Formula
type Uninterned Formula Source # 
Instance details

Defined in ToySolver.SAT.Formula

type Uninterned Formula
type Rep (Description Formula) Source # 
Instance details

Defined in ToySolver.SAT.Formula

type Rep (Description Formula) = D1 ('MetaData "Description" "ToySolver.SAT.Formula" "toysolver-0.8.1-8UpSeeDvJqYHlnd3w7teb3" '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 Source #

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

simplify :: Formula -> Formula Source #