satyros-0.3.1.4: Step-by-step SAT solver for educational purposes
Safe HaskellNone
LanguageHaskell2010

Satyros.DPLL.Effect

Documentation

newtype DPLL s f a Source #

Constructors

DPLL 

Fields

Instances

Instances details
Generic1 (DPLL s f :: Type -> Type) Source # 
Instance details

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

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

Defined in Satyros.DPLL.Effect

Methods

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

Functor f => Monad (DPLL s f) Source # 
Instance details

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

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

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

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

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

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

Defined in Satyros.DPLL.Effect

type Rep1 (DPLL s f :: Type -> Type) = D1 ('MetaData "DPLL" "Satyros.DPLL.Effect" "satyros-0.3.1.4-3YwMxGnZD0k1OVgpDx5SHB" '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) Source # 
Instance details

Defined in Satyros.DPLL.Effect

type Rep (DPLL s f a) = D1 ('MetaData "DPLL" "Satyros.DPLL.Effect" "satyros-0.3.1.4-3YwMxGnZD0k1OVgpDx5SHB" '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) Source #

data DPLLF f r Source #

Instances

Instances details
Functor f => Functor (DPLLF f) Source # 
Instance details

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

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

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

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

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

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

Defined in Satyros.DPLL.Effect

type Rep1 (DPLLF f :: Type -> Type) = D1 ('MetaData "DPLLF" "Satyros.DPLL.Effect" "satyros-0.3.1.4-3YwMxGnZD0k1OVgpDx5SHB" '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) Source # 
Instance details

Defined in Satyros.DPLL.Effect

type Rep (DPLLF f r) = D1 ('MetaData "DPLLF" "Satyros.DPLL.Effect" "satyros-0.3.1.4-3YwMxGnZD0k1OVgpDx5SHB" '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)))))))