module Satyros.DPLL.BCP
  ( bcp
  , bcpUnitClauseHandler
  , bcpConflictRelSATHandler
  ) where

import           Control.Lens             (use, (^?))
import           Control.Monad.Except     (runExceptT, throwError)
import           Control.Monad.Extra      (eitherM, forM_)
import           Control.Monad.Trans      (lift)
import qualified Satyros.CNF              as CNF
import           Satyros.DPLL.Assignment  (valueOfLiteral)
import           Satyros.DPLL.Effect      (DPLL, bcpComplete, bcpConflict,
                                           bcpConflictDrivenClause,
                                           bcpUnitClause)
import           Satyros.DPLL.Storage     (assignment, clauses)
import           Satyros.DPLL.StorageUtil (assignImplicationVariable,
                                           deriveConflictClauseRelSAT)

bcp :: (Functor f) => DPLL s f ()
bcp :: DPLL s f ()
bcp = do
  Vector Clause
cls <- Getting (Vector Clause) (Storage s) (Vector Clause)
-> DPLL s f (Vector Clause)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Vector Clause) (Storage s) (Vector Clause)
forall s a. HasClauses s a => Lens' s a
clauses
  (DPLL s f () -> DPLL s f ())
-> (() -> DPLL s f ())
-> DPLL s f (Either (DPLL s f ()) ())
-> DPLL s f ()
forall (m :: * -> *) a c b.
Monad m =>
(a -> m c) -> (b -> m c) -> m (Either a b) -> m c
eitherM DPLL s f () -> DPLL s f ()
forall a. a -> a
id () -> DPLL s f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DPLL s f (Either (DPLL s f ()) ()) -> DPLL s f ())
-> (ExceptT (DPLL s f ()) (DPLL s f) ()
    -> DPLL s f (Either (DPLL s f ()) ()))
-> ExceptT (DPLL s f ()) (DPLL s f) ()
-> DPLL s f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT (DPLL s f ()) (DPLL s f) ()
-> DPLL s f (Either (DPLL s f ()) ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT (DPLL s f ()) (DPLL s f) () -> DPLL s f ())
-> ExceptT (DPLL s f ()) (DPLL s f) () -> DPLL s f ()
forall a b. (a -> b) -> a -> b
$ do
    Vector Clause
-> (Clause -> ExceptT (DPLL s f ()) (DPLL s f) ())
-> ExceptT (DPLL s f ()) (DPLL s f) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Vector Clause
cls ((Clause -> ExceptT (DPLL s f ()) (DPLL s f) ())
 -> ExceptT (DPLL s f ()) (DPLL s f) ())
-> (Clause -> ExceptT (DPLL s f ()) (DPLL s f) ())
-> ExceptT (DPLL s f ()) (DPLL s f) ()
forall a b. (a -> b) -> a -> b
$ \c :: Clause
c@(CNF.Clause [Literal]
ls') -> do
      Assignment
asgn <- Getting Assignment (Storage s) Assignment
-> ExceptT (DPLL s f ()) (DPLL s f) Assignment
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting Assignment (Storage s) Assignment
forall s a. HasAssignment s a => Lens' s a
assignment
      case (Literal -> Maybe (Maybe Literal) -> Maybe (Maybe Literal))
-> Maybe (Maybe Literal) -> [Literal] -> Maybe (Maybe Literal)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Assignment
-> Literal -> Maybe (Maybe Literal) -> Maybe (Maybe Literal)
go Assignment
asgn) Maybe (Maybe Literal)
forall a. Maybe a
Nothing [Literal]
ls' of
        Maybe (Maybe Literal)
Nothing -> DPLL s f () -> ExceptT (DPLL s f ()) (DPLL s f) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (DPLL s f () -> ExceptT (DPLL s f ()) (DPLL s f) ())
-> DPLL s f () -> ExceptT (DPLL s f ()) (DPLL s f) ()
forall a b. (a -> b) -> a -> b
$ Clause -> DPLL s f ()
forall (f :: * -> *) s. Functor f => Clause -> DPLL s f ()
bcpConflict Clause
c
        Just Maybe Literal
Nothing -> () -> ExceptT (DPLL s f ()) (DPLL s f) ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Just (Just Literal
l) -> DPLL s f () -> ExceptT (DPLL s f ()) (DPLL s f) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (DPLL s f () -> ExceptT (DPLL s f ()) (DPLL s f) ())
-> DPLL s f () -> ExceptT (DPLL s f ()) (DPLL s f) ()
forall a b. (a -> b) -> a -> b
$ do
          Clause -> Literal -> DPLL s f ()
forall (f :: * -> *) s.
Functor f =>
Clause -> Literal -> DPLL s f ()
bcpUnitClause Clause
c Literal
l
          DPLL s f ()
forall (f :: * -> *) s. Functor f => DPLL s f ()
bcp
    DPLL s f () -> ExceptT (DPLL s f ()) (DPLL s f) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift DPLL s f ()
forall (f :: * -> *) s. Functor f => DPLL s f ()
bcpComplete
  where
    go :: Assignment
-> Literal -> Maybe (Maybe Literal) -> Maybe (Maybe Literal)
go Assignment
asgn Literal
l Maybe (Maybe Literal)
rest
      | Just Bool
True <- Maybe Bool
v = Maybe Literal -> Maybe (Maybe Literal)
forall a. a -> Maybe a
Just Maybe Literal
forall a. Maybe a
Nothing
      | Just Bool
False <- Maybe Bool
v = Maybe (Maybe Literal)
rest
      | Maybe (Maybe Literal)
Nothing <- Maybe (Maybe Literal)
rest = Maybe Literal -> Maybe (Maybe Literal)
forall a. a -> Maybe a
Just (Literal -> Maybe Literal
forall a. a -> Maybe a
Just Literal
l)
      | Bool
otherwise = Maybe Literal -> Maybe (Maybe Literal)
forall a. a -> Maybe a
Just Maybe Literal
forall a. Maybe a
Nothing
      where
        v :: Maybe Bool
v = Assignment
asgn Assignment -> Getting (First Bool) Assignment Bool -> Maybe Bool
forall s a. s -> Getting (First a) s a -> Maybe a
^? Literal -> Traversal' Assignment Bool
valueOfLiteral Literal
l

bcpUnitClauseHandler :: (Functor f) => CNF.Clause -> CNF.Literal -> DPLL s f ()
bcpUnitClauseHandler :: Clause -> Literal -> DPLL s f ()
bcpUnitClauseHandler Clause
c Literal
l = Literal -> Clause -> DPLL s f ()
forall (f :: * -> *) s.
Functor f =>
Literal -> Clause -> DPLL s f ()
assignImplicationVariable Literal
l Clause
c

bcpConflictRelSATHandler :: (Functor f) => CNF.Clause -> DPLL s f ()
bcpConflictRelSATHandler :: Clause -> DPLL s f ()
bcpConflictRelSATHandler Clause
c = do
  Clause
cdc <- Clause -> DPLL s f Clause
forall (f :: * -> *) s. Functor f => Clause -> DPLL s f Clause
deriveConflictClauseRelSAT Clause
c
  Clause -> DPLL s f ()
forall (f :: * -> *) s. Functor f => Clause -> DPLL s f ()
bcpConflictDrivenClause Clause
cdc