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