Satyros.DPLL.Effect

Documentation

newtype DPLL s f a

Constructors

DPLL

Fields

• runDPLL :: FreeT (DPLLF f) (State (Storage s)) a

Instances

Generic1 (DPLL s f :: Type -> Type)

Defined in Satyros.DPLL.Effect

Associated Types

type Rep1 (DPLL s f) :: k -> Type

Methods

from1 :: forall (a :: k). DPLL s f a -> Rep1 (DPLL s f) a

to1 :: forall (a :: k). Rep1 (DPLL s f) a -> DPLL s f a

Functor f => MonadState (Storage s) (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

get :: DPLL s f (Storage s)

put :: Storage s -> DPLL s f ()

state :: (Storage s -> (a, Storage s)) -> DPLL s f a

Functor f => MonadFree (DPLLF f) (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

wrap :: DPLLF f (DPLL s f a) -> DPLL s f a

Functor f => Monad (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

(>>=) :: DPLL s f a -> (a -> DPLL s f b) -> DPLL s f b

(>>) :: DPLL s f a -> DPLL s f b -> DPLL s f b

return :: a -> DPLL s f a

Functor f => Functor (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

fmap :: (a -> b) -> DPLL s f a -> DPLL s f b

(<$) :: a -> DPLL s f b -> DPLL s f a

Functor f => Applicative (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

pure :: a -> DPLL s f a

(<*>) :: DPLL s f (a -> b) -> DPLL s f a -> DPLL s f b

liftA2 :: (a -> b -> c) -> DPLL s f a -> DPLL s f b -> DPLL s f c

(*>) :: DPLL s f a -> DPLL s f b -> DPLL s f b

(<*) :: DPLL s f a -> DPLL s f b -> DPLL s f a

(Show1 f, Functor f) => Show1 (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> DPLL s f a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [DPLL s f a] -> ShowS

(Show1 f, Functor f, Show a) => Show (DPLL s f a)

Defined in Satyros.DPLL.Effect

Methods

showsPrec :: Int -> DPLL s f a -> ShowS

show :: DPLL s f a -> String

showList :: [DPLL s f a] -> ShowS

Generic (DPLL s f a)

Defined in Satyros.DPLL.Effect

Associated Types

type Rep (DPLL s f a) :: Type -> Type

Methods

from :: DPLL s f a -> Rep (DPLL s f a) x

to :: Rep (DPLL s f a) x -> DPLL s f a

type Rep1 (DPLL s f :: Type -> Type)

Defined in Satyros.DPLL.Effect

type Rep1 (DPLL s f :: Type -> Type) = D1 ('MetaData "DPLL" "Satyros.DPLL.Effect" "satyros-0.3.1.2-BItSMt1Jzej1gr09liIUNH" 'True) (C1 ('MetaCons "DPLL" 'PrefixI 'True) (S1 ('MetaSel ('Just "runDPLL") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 (FreeT (DPLLF f) (State (Storage s))))))

type Rep (DPLL s f a)

Defined in Satyros.DPLL.Effect

type Rep (DPLL s f a) = D1 ('MetaData "DPLL" "Satyros.DPLL.Effect" "satyros-0.3.1.2-BItSMt1Jzej1gr09liIUNH" 'True) (C1 ('MetaCons "DPLL" 'PrefixI 'True) (S1 ('MetaSel ('Just "runDPLL") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (FreeT (DPLLF f) (State (Storage s)) a))))

stepDPLL :: Functor f => DPLL s f a -> Storage s -> (FreeF (DPLLF f) a (DPLL s f a), Storage s)

data DPLLF f r

Constructors

BCPUnitClause Clause Literal r

BCPConflict Clause r

BCPConflictDrivenClause Clause r

BCPComplete

DecisionResult Literal

DecisionComplete

BacktraceExhaustion

BacktraceComplete Clause Literal

InsideDPLL (f r)

Instances

Functor f => Functor (DPLLF f)

Defined in Satyros.DPLL.Effect

Methods

fmap :: (a -> b) -> DPLLF f a -> DPLLF f b

(<$) :: a -> DPLLF f b -> DPLLF f a

(Show1 f, Functor f) => Show1 (DPLLF f)

Defined in Satyros.DPLL.Effect

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> DPLLF f a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [DPLLF f a] -> ShowS

Generic1 (DPLLF f :: Type -> Type)

Defined in Satyros.DPLL.Effect

Associated Types

type Rep1 (DPLLF f) :: k -> Type

Methods

from1 :: forall (a :: k). DPLLF f a -> Rep1 (DPLLF f) a

to1 :: forall (a :: k). Rep1 (DPLLF f) a -> DPLLF f a

Functor f => MonadFree (DPLLF f) (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

wrap :: DPLLF f (DPLL s f a) -> DPLL s f a

(Show r, Show (f r)) => Show (DPLLF f r)

Defined in Satyros.DPLL.Effect

Methods

showsPrec :: Int -> DPLLF f r -> ShowS

show :: DPLLF f r -> String

showList :: [DPLLF f r] -> ShowS

Generic (DPLLF f r)

Defined in Satyros.DPLL.Effect

Associated Types

type Rep (DPLLF f r) :: Type -> Type

Methods

from :: DPLLF f r -> Rep (DPLLF f r) x

to :: Rep (DPLLF f r) x -> DPLLF f r

type Rep1 (DPLLF f :: Type -> Type)

Defined in Satyros.DPLL.Effect

type Rep1 (DPLLF f :: Type -> Type) = D1 ('MetaData "DPLLF" "Satyros.DPLL.Effect" "satyros-0.3.1.2-BItSMt1Jzej1gr09liIUNH" 'False) (((C1 ('MetaCons "BCPUnitClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1)) :+: C1 ('MetaCons "BCPConflict" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1)) :+: (C1 ('MetaCons "BCPConflictDrivenClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1) :+: C1 ('MetaCons "BCPComplete" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DecisionResult" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "DecisionComplete" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BacktraceExhaustion" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BacktraceComplete" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "InsideDPLL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec1 f))))))

type Rep (DPLLF f r)

Defined in Satyros.DPLL.Effect

type Rep (DPLLF f r) = D1 ('MetaData "DPLLF" "Satyros.DPLL.Effect" "satyros-0.3.1.2-BItSMt1Jzej1gr09liIUNH" 'False) (((C1 ('MetaCons "BCPUnitClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 r))) :+: C1 ('MetaCons "BCPConflict" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 r))) :+: (C1 ('MetaCons "BCPConflictDrivenClause" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 r)) :+: C1 ('MetaCons "BCPComplete" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "DecisionResult" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "DecisionComplete" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BacktraceExhaustion" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BacktraceComplete" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Clause) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "InsideDPLL" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (f r)))))))

bcpUnitClause :: Functor f => Clause -> Literal -> DPLL s f ()

bcpConflict :: Functor f => Clause -> DPLL s f ()

bcpConflictDrivenClause :: Functor f => Clause -> DPLL s f ()

bcpComplete :: Functor f => DPLL s f ()

decisionResult :: Functor f => Literal -> DPLL s f ()

decisionComplete :: Functor f => DPLL s f ()

backtraceExhaustion :: Functor f => DPLL s f ()

backtraceComplete :: Functor f => Clause -> Literal -> DPLL s f ()