{-# 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 #-}