{-# LANGUAGE QuantifiedConstraints #-} module Satyros.DPLL.Effect where import Control.Monad.State.Strict (MonadState, State, runState) import Control.Monad.Trans.Free (FreeF, FreeT (FreeT, runFreeT), MonadFree (wrap), hoistFreeT) import Data.Bifunctor (first) import Data.Functor.Classes (Show1 (liftShowsPrec), showsBinaryWith, showsPrec1, showsUnaryWith) import Data.Functor.Const (Const (Const)) import GHC.Generics (Generic, Generic1) import qualified Satyros.CNF as CNF import Satyros.DPLL.Storage (Storage) import Satyros.Util (showsTernaryWith) newtype DPLL s f a = DPLL{ DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a runDPLL :: FreeT (DPLLF f) (State (Storage s)) a } deriving stock ((forall x. DPLL s f a -> Rep (DPLL s f a) x) -> (forall x. Rep (DPLL s f a) x -> DPLL s f a) -> Generic (DPLL s f a) forall x. Rep (DPLL s f a) x -> DPLL s f a forall x. DPLL s f a -> Rep (DPLL s f a) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall s (f :: * -> *) a x. Rep (DPLL s f a) x -> DPLL s f a forall s (f :: * -> *) a x. DPLL s f a -> Rep (DPLL s f a) x $cto :: forall s (f :: * -> *) a x. Rep (DPLL s f a) x -> DPLL s f a $cfrom :: forall s (f :: * -> *) a x. DPLL s f a -> Rep (DPLL s f a) x Generic, (forall a. DPLL s f a -> Rep1 (DPLL s f) a) -> (forall a. Rep1 (DPLL s f) a -> DPLL s f a) -> Generic1 (DPLL s f) forall a. Rep1 (DPLL s f) a -> DPLL s f a forall a. DPLL s f a -> Rep1 (DPLL s f) a forall k (f :: k -> *). (forall (a :: k). f a -> Rep1 f a) -> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f forall s (f :: * -> *) a. Rep1 (DPLL s f) a -> DPLL s f a forall s (f :: * -> *) a. DPLL s f a -> Rep1 (DPLL s f) a $cto1 :: forall s (f :: * -> *) a. Rep1 (DPLL s f) a -> DPLL s f a $cfrom1 :: forall s (f :: * -> *) a. DPLL s f a -> Rep1 (DPLL s f) a Generic1) deriving newtype (a -> DPLL s f b -> DPLL s f a (a -> b) -> DPLL s f a -> DPLL s f b (forall a b. (a -> b) -> DPLL s f a -> DPLL s f b) -> (forall a b. a -> DPLL s f b -> DPLL s f a) -> Functor (DPLL s f) forall a b. a -> DPLL s f b -> DPLL s f a forall a b. (a -> b) -> DPLL s f a -> DPLL s f b forall s (f :: * -> *) a b. Functor f => a -> DPLL s f b -> DPLL s f a forall s (f :: * -> *) a b. Functor f => (a -> b) -> DPLL s f a -> DPLL s f b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> DPLL s f b -> DPLL s f a $c<$ :: forall s (f :: * -> *) a b. Functor f => a -> DPLL s f b -> DPLL s f a fmap :: (a -> b) -> DPLL s f a -> DPLL s f b $cfmap :: forall s (f :: * -> *) a b. Functor f => (a -> b) -> DPLL s f a -> DPLL s f b Functor, Functor (DPLL s f) a -> DPLL s f a Functor (DPLL s f) -> (forall a. a -> DPLL s f a) -> (forall a b. DPLL s f (a -> b) -> DPLL s f a -> DPLL s f b) -> (forall a b c. (a -> b -> c) -> DPLL s f a -> DPLL s f b -> DPLL s f c) -> (forall a b. DPLL s f a -> DPLL s f b -> DPLL s f b) -> (forall a b. DPLL s f a -> DPLL s f b -> DPLL s f a) -> Applicative (DPLL s f) DPLL s f a -> DPLL s f b -> DPLL s f b DPLL s f a -> DPLL s f b -> DPLL s f a DPLL s f (a -> b) -> DPLL s f a -> DPLL s f b (a -> b -> c) -> DPLL s f a -> DPLL s f b -> DPLL s f c forall a. a -> DPLL s f a forall a b. DPLL s f a -> DPLL s f b -> DPLL s f a forall a b. DPLL s f a -> DPLL s f b -> DPLL s f b forall a b. DPLL s f (a -> b) -> DPLL s f a -> DPLL s f b forall a b c. (a -> b -> c) -> DPLL s f a -> DPLL s f b -> DPLL s f c forall s (f :: * -> *). Functor f => Functor (DPLL s f) forall s (f :: * -> *) a. Functor f => a -> DPLL s f a forall s (f :: * -> *) a b. Functor f => DPLL s f a -> DPLL s f b -> DPLL s f a forall s (f :: * -> *) a b. Functor f => DPLL s f a -> DPLL s f b -> DPLL s f b forall s (f :: * -> *) a b. Functor f => DPLL s f (a -> b) -> DPLL s f a -> DPLL s f b forall s (f :: * -> *) a b c. Functor f => (a -> b -> c) -> DPLL s f a -> DPLL s f b -> DPLL s f c forall (f :: * -> *). Functor f -> (forall a. a -> f a) -> (forall a b. f (a -> b) -> f a -> f b) -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c) -> (forall a b. f a -> f b -> f b) -> (forall a b. f a -> f b -> f a) -> Applicative f <* :: DPLL s f a -> DPLL s f b -> DPLL s f a $c<* :: forall s (f :: * -> *) a b. Functor f => DPLL s f a -> DPLL s f b -> DPLL s f a *> :: DPLL s f a -> DPLL s f b -> DPLL s f b $c*> :: forall s (f :: * -> *) a b. Functor f => DPLL s f a -> DPLL s f b -> DPLL s f b liftA2 :: (a -> b -> c) -> DPLL s f a -> DPLL s f b -> DPLL s f c $cliftA2 :: forall s (f :: * -> *) a b c. Functor f => (a -> b -> c) -> DPLL s f a -> DPLL s f b -> DPLL s f c <*> :: DPLL s f (a -> b) -> DPLL s f a -> DPLL s f b $c<*> :: forall s (f :: * -> *) a b. Functor f => DPLL s f (a -> b) -> DPLL s f a -> DPLL s f b pure :: a -> DPLL s f a $cpure :: forall s (f :: * -> *) a. Functor f => a -> DPLL s f a $cp1Applicative :: forall s (f :: * -> *). Functor f => Functor (DPLL s f) Applicative, Applicative (DPLL s f) a -> DPLL s f a Applicative (DPLL s f) -> (forall a b. DPLL s f a -> (a -> DPLL s f b) -> DPLL s f b) -> (forall a b. DPLL s f a -> DPLL s f b -> DPLL s f b) -> (forall a. a -> DPLL s f a) -> Monad (DPLL s f) 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 forall a. a -> DPLL s f a forall a b. DPLL s f a -> DPLL s f b -> DPLL s f b forall a b. DPLL s f a -> (a -> DPLL s f b) -> DPLL s f b forall s (f :: * -> *). Functor f => Applicative (DPLL s f) forall s (f :: * -> *) a. Functor f => a -> DPLL s f a forall s (f :: * -> *) a b. Functor f => DPLL s f a -> DPLL s f b -> DPLL s f b forall s (f :: * -> *) a b. Functor f => DPLL s f a -> (a -> DPLL s f b) -> DPLL s f b forall (m :: * -> *). Applicative m -> (forall a b. m a -> (a -> m b) -> m b) -> (forall a b. m a -> m b -> m b) -> (forall a. a -> m a) -> Monad m return :: a -> DPLL s f a $creturn :: forall s (f :: * -> *) a. Functor f => a -> DPLL s f a >> :: DPLL s f a -> DPLL s f b -> DPLL s f b $c>> :: forall s (f :: * -> *) a b. Functor f => DPLL s f a -> DPLL s f b -> DPLL s f b >>= :: DPLL s f a -> (a -> DPLL s f b) -> DPLL s f b $c>>= :: forall s (f :: * -> *) a b. Functor f => DPLL s f a -> (a -> DPLL s f b) -> DPLL s f b $cp1Monad :: forall s (f :: * -> *). Functor f => Applicative (DPLL s f) Monad, MonadState (Storage s)) instance (Functor f) => MonadFree (DPLLF f) (DPLL s f) where wrap :: DPLLF f (DPLL s f a) -> DPLL s f a wrap (BCPUnitClause Clause c Literal l DPLL s f a r) = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ Clause -> Literal -> FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. Clause -> Literal -> r -> DPLLF f r BCPUnitClause Clause c Literal l (FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a)) -> FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall a b. (a -> b) -> a -> b $ DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a forall s (f :: * -> *) a. DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a runDPLL DPLL s f a r wrap (BCPConflict Clause c DPLL s f a r) = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ Clause -> FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. Clause -> r -> DPLLF f r BCPConflict Clause c (FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a)) -> FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall a b. (a -> b) -> a -> b $ DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a forall s (f :: * -> *) a. DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a runDPLL DPLL s f a r wrap (BCPConflictDrivenClause Clause c DPLL s f a r) = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ Clause -> FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. Clause -> r -> DPLLF f r BCPConflictDrivenClause Clause c (FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a)) -> FreeT (DPLLF f) (State (Storage s)) a -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall a b. (a -> b) -> a -> b $ DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a forall s (f :: * -> *) a. DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a runDPLL DPLL s f a r wrap DPLLF f (DPLL s f a) BCPComplete = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. DPLLF f r BCPComplete wrap (DecisionResult Literal l) = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ Literal -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. Literal -> DPLLF f r DecisionResult Literal l wrap DPLLF f (DPLL s f a) DecisionComplete = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. DPLLF f r DecisionComplete wrap DPLLF f (DPLL s f a) BacktraceExhaustion = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. DPLLF f r BacktraceExhaustion wrap (BacktraceComplete Clause c Literal l) = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ Clause -> Literal -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. Clause -> Literal -> DPLLF f r BacktraceComplete Clause c Literal l wrap (InsideDPLL f (DPLL s f a) inner) = FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL (FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> FreeT (DPLLF f) (State (Storage s)) a forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a forall a b. (a -> b) -> a -> b $ f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) r. f r -> DPLLF f r InsideDPLL (f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a)) -> f (FreeT (DPLLF f) (State (Storage s)) a) -> DPLLF f (FreeT (DPLLF f) (State (Storage s)) a) forall a b. (a -> b) -> a -> b $ (DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a) -> f (DPLL s f a) -> f (FreeT (DPLLF f) (State (Storage s)) a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a forall s (f :: * -> *) a. DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a runDPLL f (DPLL s f a) inner {-# INLINE wrap #-} instance (Show1 f, Functor f) => Show1 (DPLL s f) where liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> DPLL s f a -> ShowS liftShowsPrec Int -> a -> ShowS sp [a] -> ShowS slp Int d = (Int -> FreeT (DPLLF f) (Const [Char]) a -> ShowS) -> [Char] -> Int -> FreeT (DPLLF f) (Const [Char]) a -> ShowS forall a. (Int -> a -> ShowS) -> [Char] -> Int -> a -> ShowS showsUnaryWith ((Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> FreeT (DPLLF f) (Const [Char]) a -> ShowS forall (f :: * -> *) a. Show1 f => (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS liftShowsPrec Int -> a -> ShowS sp [a] -> ShowS slp) [Char] "DPLL" Int d (FreeT (DPLLF f) (Const [Char]) a -> ShowS) -> (DPLL s f a -> FreeT (DPLLF f) (Const [Char]) a) -> DPLL s f a -> ShowS forall b c a. (b -> c) -> (a -> b) -> a -> c . (forall a. State (Storage s) a -> Const [Char] a) -> FreeT (DPLLF f) (State (Storage s)) a -> FreeT (DPLLF f) (Const [Char]) a forall (m :: * -> *) (f :: * -> *) (n :: * -> *) b. (Monad m, Functor f) => (forall a. m a -> n a) -> FreeT f m b -> FreeT f n b hoistFreeT (Const [Char] a -> State (Storage s) a -> Const [Char] a forall a b. a -> b -> a const (Const [Char] a -> State (Storage s) a -> Const [Char] a) -> Const [Char] a -> State (Storage s) a -> Const [Char] a forall a b. (a -> b) -> a -> b $ [Char] -> Const [Char] a forall k a (b :: k). a -> Const a b Const [Char] "<stateful computation>") (FreeT (DPLLF f) (State (Storage s)) a -> FreeT (DPLLF f) (Const [Char]) a) -> (DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a) -> DPLL s f a -> FreeT (DPLLF f) (Const [Char]) a forall b c a. (b -> c) -> (a -> b) -> a -> c . DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a forall s (f :: * -> *) a. DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a runDPLL {-# INLINE liftShowsPrec #-} instance (Show1 f, Functor f, Show a) => Show (DPLL s f a) where showsPrec :: Int -> DPLL s f a -> ShowS showsPrec = Int -> DPLL s f a -> ShowS forall (f :: * -> *) a. (Show1 f, Show a) => Int -> f a -> ShowS showsPrec1 {-# INLINE showsPrec #-} stepDPLL :: (Functor f) => DPLL s f a -> Storage s -> (FreeF (DPLLF f) a (DPLL s f a), Storage s) stepDPLL :: DPLL s f a -> Storage s -> (FreeF (DPLLF f) a (DPLL s f a), Storage s) stepDPLL DPLL s f a d Storage s s = (FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a) -> FreeF (DPLLF f) a (DPLL s f a)) -> (FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a), Storage s) -> (FreeF (DPLLF f) a (DPLL s f a), Storage s) forall (p :: * -> * -> *) a b c. Bifunctor p => (a -> b) -> p a c -> p b c first ((FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a) -> FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a) -> FreeF (DPLLF f) a (DPLL s f a) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b fmap FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a forall s (f :: * -> *) a. FreeT (DPLLF f) (State (Storage s)) a -> DPLL s f a DPLL) ((FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a), Storage s) -> (FreeF (DPLLF f) a (DPLL s f a), Storage s)) -> (FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a), Storage s) -> (FreeF (DPLLF f) a (DPLL s f a), Storage s) forall a b. (a -> b) -> a -> b $ State (Storage s) (FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a)) -> Storage s -> (FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a), Storage s) forall s a. State s a -> s -> (a, s) runState (FreeT (DPLLF f) (State (Storage s)) a -> State (Storage s) (FreeF (DPLLF f) a (FreeT (DPLLF f) (State (Storage s)) a)) forall (f :: * -> *) (m :: * -> *) a. FreeT f m a -> m (FreeF f a (FreeT f m a)) runFreeT (DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a forall s (f :: * -> *) a. DPLL s f a -> FreeT (DPLLF f) (State (Storage s)) a runDPLL DPLL s f a d)) Storage s s {-# INLINE stepDPLL #-} data DPLLF f r = BCPUnitClause CNF.Clause CNF.Literal r | BCPConflict CNF.Clause r | BCPConflictDrivenClause CNF.Clause r | BCPComplete | DecisionResult CNF.Literal | DecisionComplete | BacktraceExhaustion | BacktraceComplete CNF.Clause CNF.Literal | InsideDPLL (f r) deriving stock ((forall x. DPLLF f r -> Rep (DPLLF f r) x) -> (forall x. Rep (DPLLF f r) x -> DPLLF f r) -> Generic (DPLLF f r) forall x. Rep (DPLLF f r) x -> DPLLF f r forall x. DPLLF f r -> Rep (DPLLF f r) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall (f :: * -> *) r x. Rep (DPLLF f r) x -> DPLLF f r forall (f :: * -> *) r x. DPLLF f r -> Rep (DPLLF f r) x $cto :: forall (f :: * -> *) r x. Rep (DPLLF f r) x -> DPLLF f r $cfrom :: forall (f :: * -> *) r x. DPLLF f r -> Rep (DPLLF f r) x Generic, (forall a. DPLLF f a -> Rep1 (DPLLF f) a) -> (forall a. Rep1 (DPLLF f) a -> DPLLF f a) -> Generic1 (DPLLF f) forall a. Rep1 (DPLLF f) a -> DPLLF f a forall a. DPLLF f a -> Rep1 (DPLLF f) a forall k (f :: k -> *). (forall (a :: k). f a -> Rep1 f a) -> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f forall (f :: * -> *) a. Rep1 (DPLLF f) a -> DPLLF f a forall (f :: * -> *) a. DPLLF f a -> Rep1 (DPLLF f) a $cto1 :: forall (f :: * -> *) a. Rep1 (DPLLF f) a -> DPLLF f a $cfrom1 :: forall (f :: * -> *) a. DPLLF f a -> Rep1 (DPLLF f) a Generic1, Int -> DPLLF f r -> ShowS [DPLLF f r] -> ShowS DPLLF f r -> [Char] (Int -> DPLLF f r -> ShowS) -> (DPLLF f r -> [Char]) -> ([DPLLF f r] -> ShowS) -> Show (DPLLF f r) forall a. (Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a forall (f :: * -> *) r. (Show r, Show (f r)) => Int -> DPLLF f r -> ShowS forall (f :: * -> *) r. (Show r, Show (f r)) => [DPLLF f r] -> ShowS forall (f :: * -> *) r. (Show r, Show (f r)) => DPLLF f r -> [Char] showList :: [DPLLF f r] -> ShowS $cshowList :: forall (f :: * -> *) r. (Show r, Show (f r)) => [DPLLF f r] -> ShowS show :: DPLLF f r -> [Char] $cshow :: forall (f :: * -> *) r. (Show r, Show (f r)) => DPLLF f r -> [Char] showsPrec :: Int -> DPLLF f r -> ShowS $cshowsPrec :: forall (f :: * -> *) r. (Show r, Show (f r)) => Int -> DPLLF f r -> ShowS Show, a -> DPLLF f b -> DPLLF f a (a -> b) -> DPLLF f a -> DPLLF f b (forall a b. (a -> b) -> DPLLF f a -> DPLLF f b) -> (forall a b. a -> DPLLF f b -> DPLLF f a) -> Functor (DPLLF f) forall a b. a -> DPLLF f b -> DPLLF f a forall a b. (a -> b) -> DPLLF f a -> DPLLF f b forall (f :: * -> *) a b. Functor f => a -> DPLLF f b -> DPLLF f a forall (f :: * -> *) a b. Functor f => (a -> b) -> DPLLF f a -> DPLLF f b forall (f :: * -> *). (forall a b. (a -> b) -> f a -> f b) -> (forall a b. a -> f b -> f a) -> Functor f <$ :: a -> DPLLF f b -> DPLLF f a $c<$ :: forall (f :: * -> *) a b. Functor f => a -> DPLLF f b -> DPLLF f a fmap :: (a -> b) -> DPLLF f a -> DPLLF f b $cfmap :: forall (f :: * -> *) a b. Functor f => (a -> b) -> DPLLF f a -> DPLLF f b Functor) instance (Show1 f, Functor f) => Show1 (DPLLF f) where liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> DPLLF f a -> ShowS liftShowsPrec Int -> a -> ShowS sp [a] -> ShowS _ Int d (BCPUnitClause Clause c Literal l a r) = (Int -> Clause -> ShowS) -> (Int -> Literal -> ShowS) -> (Int -> a -> ShowS) -> [Char] -> Int -> Clause -> Literal -> a -> ShowS forall a b c. (Int -> a -> ShowS) -> (Int -> b -> ShowS) -> (Int -> c -> ShowS) -> [Char] -> Int -> a -> b -> c -> ShowS showsTernaryWith Int -> Clause -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec Int -> Literal -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec Int -> a -> ShowS sp [Char] "BCPUnitClause" Int d Clause c Literal l a r liftShowsPrec Int -> a -> ShowS sp [a] -> ShowS _ Int d (BCPConflict Clause c a r) = (Int -> Clause -> ShowS) -> (Int -> a -> ShowS) -> [Char] -> Int -> Clause -> a -> ShowS forall a b. (Int -> a -> ShowS) -> (Int -> b -> ShowS) -> [Char] -> Int -> a -> b -> ShowS showsBinaryWith Int -> Clause -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec Int -> a -> ShowS sp [Char] "BCPConflict" Int d Clause c a r liftShowsPrec Int -> a -> ShowS sp [a] -> ShowS _ Int d (BCPConflictDrivenClause Clause c a r) = (Int -> Clause -> ShowS) -> (Int -> a -> ShowS) -> [Char] -> Int -> Clause -> a -> ShowS forall a b. (Int -> a -> ShowS) -> (Int -> b -> ShowS) -> [Char] -> Int -> a -> b -> ShowS showsBinaryWith Int -> Clause -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec Int -> a -> ShowS sp [Char] "BCPConflictDrivenClause" Int d Clause c a r liftShowsPrec Int -> a -> ShowS _ [a] -> ShowS _ Int _ DPLLF f a BCPComplete = [Char] -> ShowS showString [Char] "BCPComplete" liftShowsPrec Int -> a -> ShowS _ [a] -> ShowS _ Int d (DecisionResult Literal l) = (Int -> Literal -> ShowS) -> [Char] -> Int -> Literal -> ShowS forall a. (Int -> a -> ShowS) -> [Char] -> Int -> a -> ShowS showsUnaryWith Int -> Literal -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec [Char] "DecisionResult" Int d Literal l liftShowsPrec Int -> a -> ShowS _ [a] -> ShowS _ Int _ DPLLF f a DecisionComplete = [Char] -> ShowS showString [Char] "DecisionComplete" liftShowsPrec Int -> a -> ShowS _ [a] -> ShowS _ Int _ DPLLF f a BacktraceExhaustion = [Char] -> ShowS showString [Char] "BacktraceExhaustion" liftShowsPrec Int -> a -> ShowS _ [a] -> ShowS _ Int d (BacktraceComplete Clause c Literal l) = (Int -> Clause -> ShowS) -> (Int -> Literal -> ShowS) -> [Char] -> Int -> Clause -> Literal -> ShowS forall a b. (Int -> a -> ShowS) -> (Int -> b -> ShowS) -> [Char] -> Int -> a -> b -> ShowS showsBinaryWith Int -> Clause -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec Int -> Literal -> ShowS forall a. Show a => Int -> a -> ShowS showsPrec [Char] "BacktraceComplete" Int d Clause c Literal l liftShowsPrec Int -> a -> ShowS sp [a] -> ShowS lsp Int d (InsideDPLL f a inner) = (Int -> f a -> ShowS) -> [Char] -> Int -> f a -> ShowS forall a. (Int -> a -> ShowS) -> [Char] -> Int -> a -> ShowS showsUnaryWith ((Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS forall (f :: * -> *) a. Show1 f => (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> f a -> ShowS liftShowsPrec Int -> a -> ShowS sp [a] -> ShowS lsp) [Char] "InsideDPLL" Int d f a inner {-# INLINE liftShowsPrec #-} bcpUnitClause :: (Functor f) => CNF.Clause -> CNF.Literal -> DPLL s f () bcpUnitClause :: Clause -> Literal -> DPLL s f () bcpUnitClause Clause c Literal l = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (DPLL s f ()) -> DPLL s f ()) -> (DPLL s f () -> DPLLF f (DPLL s f ())) -> DPLL s f () -> DPLL s f () forall b c a. (b -> c) -> (a -> b) -> a -> c . Clause -> Literal -> DPLL s f () -> DPLLF f (DPLL s f ()) forall (f :: * -> *) r. Clause -> Literal -> r -> DPLLF f r BCPUnitClause Clause c Literal l (DPLL s f () -> DPLL s f ()) -> DPLL s f () -> DPLL s f () forall a b. (a -> b) -> a -> b $ () -> DPLL s f () forall (f :: * -> *) a. Applicative f => a -> f a pure () {-# INLINE bcpUnitClause #-} bcpConflict :: (Functor f) => CNF.Clause -> DPLL s f () bcpConflict :: Clause -> DPLL s f () bcpConflict Clause c = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (DPLL s f ()) -> DPLL s f ()) -> (DPLL s f () -> DPLLF f (DPLL s f ())) -> DPLL s f () -> DPLL s f () forall b c a. (b -> c) -> (a -> b) -> a -> c . Clause -> DPLL s f () -> DPLLF f (DPLL s f ()) forall (f :: * -> *) r. Clause -> r -> DPLLF f r BCPConflict Clause c (DPLL s f () -> DPLL s f ()) -> DPLL s f () -> DPLL s f () forall a b. (a -> b) -> a -> b $ () -> DPLL s f () forall (f :: * -> *) a. Applicative f => a -> f a pure () {-# INLINE bcpConflict #-} bcpConflictDrivenClause :: (Functor f) => CNF.Clause -> DPLL s f () bcpConflictDrivenClause :: Clause -> DPLL s f () bcpConflictDrivenClause Clause c = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (DPLL s f ()) -> DPLL s f ()) -> (DPLL s f () -> DPLLF f (DPLL s f ())) -> DPLL s f () -> DPLL s f () forall b c a. (b -> c) -> (a -> b) -> a -> c . Clause -> DPLL s f () -> DPLLF f (DPLL s f ()) forall (f :: * -> *) r. Clause -> r -> DPLLF f r BCPConflictDrivenClause Clause c (DPLL s f () -> DPLL s f ()) -> DPLL s f () -> DPLL s f () forall a b. (a -> b) -> a -> b $ () -> DPLL s f () forall (f :: * -> *) a. Applicative f => a -> f a pure () {-# INLINE bcpConflictDrivenClause #-} bcpComplete :: (Functor f) => DPLL s f () bcpComplete :: DPLL s f () bcpComplete = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap DPLLF f (DPLL s f ()) forall (f :: * -> *) r. DPLLF f r BCPComplete {-# INLINE bcpComplete #-} decisionResult :: (Functor f) => CNF.Literal -> DPLL s f () decisionResult :: Literal -> DPLL s f () decisionResult = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (DPLL s f ()) -> DPLL s f ()) -> (Literal -> DPLLF f (DPLL s f ())) -> Literal -> DPLL s f () forall b c a. (b -> c) -> (a -> b) -> a -> c . Literal -> DPLLF f (DPLL s f ()) forall (f :: * -> *) r. Literal -> DPLLF f r DecisionResult {-# INLINE decisionResult #-} decisionComplete :: (Functor f) => DPLL s f () decisionComplete :: DPLL s f () decisionComplete = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap DPLLF f (DPLL s f ()) forall (f :: * -> *) r. DPLLF f r DecisionComplete {-# INLINE decisionComplete #-} backtraceExhaustion :: (Functor f) => DPLL s f () backtraceExhaustion :: DPLL s f () backtraceExhaustion = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap DPLLF f (DPLL s f ()) forall (f :: * -> *) r. DPLLF f r BacktraceExhaustion {-# INLINE backtraceExhaustion #-} backtraceComplete :: (Functor f) => CNF.Clause -> CNF.Literal -> DPLL s f () backtraceComplete :: Clause -> Literal -> DPLL s f () backtraceComplete Clause c = DPLLF f (DPLL s f ()) -> DPLL s f () forall (f :: * -> *) (m :: * -> *) a. MonadFree f m => f (m a) -> m a wrap (DPLLF f (DPLL s f ()) -> DPLL s f ()) -> (Literal -> DPLLF f (DPLL s f ())) -> Literal -> DPLL s f () forall b c a. (b -> c) -> (a -> b) -> a -> c . Clause -> Literal -> DPLLF f (DPLL s f ()) forall (f :: * -> *) r. Clause -> Literal -> DPLLF f r BacktraceComplete Clause c {-# INLINE backtraceComplete #-}