Satyros.DPLL.Effect

Documentation

newtype DPLL s f a

Constructors

DPLL

Fields

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

Instances

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

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

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

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

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

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

bcpConflictDrivenClause :: Functor f => Clause -> 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 ()