{-# LANGUAGE ViewPatterns #-} module Satyros.DPLL.StorageUtil where import Control.Lens (_2, _Just, _Nothing, _Right, each, failing, filtered, ix, like, re, takingWhile, to, use, uses, (%=), (&), (.=), (<|), (^.), (^..), (|>)) import Data.Either (partitionEithers) import Data.List (partition) import Data.Set (Set) import qualified Data.Set as Set import qualified Satyros.CNF as CNF import Satyros.DPLL.Assignment (assignVariable, eraseVariables, parentsOfLiteral) import Satyros.DPLL.Effect (DPLL) import Satyros.DPLL.Storage (assignment, clauses, unassignedVariables, variableLevels) assignDecisionVariable :: (Functor f) => CNF.Literal -> DPLL s f () assignDecisionVariable :: Literal -> DPLL s f () assignDecisionVariable l :: Literal l@(CNF.Literal Positivity _ Variable x) = do ([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s) forall s a. HasVariableLevels s a => Lens' s a variableLevels (([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s)) -> ([(Maybe Variable, Set Variable)] -> [(Maybe Variable, Set Variable)]) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= ((Variable -> Maybe Variable forall a. a -> Maybe a Just Variable x, Set Variable forall a. Set a Set.empty) (Maybe Variable, Set Variable) -> [(Maybe Variable, Set Variable)] -> [(Maybe Variable, Set Variable)] forall s a. Cons s s a a => a -> s -> s <|) (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall s a. HasUnassignedVariables s a => Lens' s a unassignedVariables ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> (Set Variable -> Set Variable) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Variable -> Set Variable -> Set Variable forall a. Ord a => a -> Set a -> Set a Set.delete Variable x (Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s) forall s a. HasAssignment s a => Lens' s a assignment ((Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s)) -> (Assignment -> Assignment) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Literal -> Maybe Clause -> Assignment -> Assignment assignVariable Literal l Maybe Clause forall a. Maybe a Nothing assignImplicationVariable :: (Functor f) => CNF.Literal -> CNF.Clause -> DPLL s f () assignImplicationVariable :: Literal -> Clause -> DPLL s f () assignImplicationVariable l :: Literal l@(CNF.Literal Positivity _ Variable x) Clause c = do ([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s) forall s a. HasVariableLevels s a => Lens' s a variableLevels (([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s)) -> ((Set Variable -> Identity (Set Variable)) -> [(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall b c a. (b -> c) -> (a -> b) -> a -> c . Index [(Maybe Variable, Set Variable)] -> Traversal' [(Maybe Variable, Set Variable)] (IxValue [(Maybe Variable, Set Variable)]) forall m. Ixed m => Index m -> Traversal' m (IxValue m) ix Index [(Maybe Variable, Set Variable)] 0 (((Maybe Variable, Set Variable) -> Identity (Maybe Variable, Set Variable)) -> [(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> ((Set Variable -> Identity (Set Variable)) -> (Maybe Variable, Set Variable) -> Identity (Maybe Variable, Set Variable)) -> (Set Variable -> Identity (Set Variable)) -> [(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Set Variable -> Identity (Set Variable)) -> (Maybe Variable, Set Variable) -> Identity (Maybe Variable, Set Variable) forall s t a b. Field2 s t a b => Lens s t a b _2 ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> (Set Variable -> Set Variable) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Variable -> Set Variable -> Set Variable forall a. Ord a => a -> Set a -> Set a Set.insert Variable x (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall s a. HasUnassignedVariables s a => Lens' s a unassignedVariables ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> (Set Variable -> Set Variable) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Variable -> Set Variable -> Set Variable forall a. Ord a => a -> Set a -> Set a Set.delete Variable x (Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s) forall s a. HasAssignment s a => Lens' s a assignment ((Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s)) -> (Assignment -> Assignment) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Literal -> Maybe Clause -> Assignment -> Assignment assignVariable Literal l (Clause -> Maybe Clause forall a. a -> Maybe a Just Clause c) assignFailureDrivenVariable :: (Functor f) => CNF.Literal -> CNF.Clause -> DPLL s f () assignFailureDrivenVariable :: Literal -> Clause -> DPLL s f () assignFailureDrivenVariable l :: Literal l@(CNF.Literal Positivity _ Variable x) Clause c = do ([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s) forall s a. HasVariableLevels s a => Lens' s a variableLevels (([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s)) -> ([(Maybe Variable, Set Variable)] -> [(Maybe Variable, Set Variable)]) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= ((Maybe Variable forall a. Maybe a Nothing, Variable -> Set Variable forall a. a -> Set a Set.singleton Variable x) (Maybe Variable, Set Variable) -> [(Maybe Variable, Set Variable)] -> [(Maybe Variable, Set Variable)] forall s a. Cons s s a a => a -> s -> s <|) (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall s a. HasUnassignedVariables s a => Lens' s a unassignedVariables ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> (Set Variable -> Set Variable) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Variable -> Set Variable -> Set Variable forall a. Ord a => a -> Set a -> Set a Set.delete Variable x (Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s) forall s a. HasAssignment s a => Lens' s a assignment ((Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s)) -> (Assignment -> Assignment) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Literal -> Maybe Clause -> Assignment -> Assignment assignVariable Literal l (Clause -> Maybe Clause forall a. a -> Maybe a Just Clause c) eraseCurrentImplicationVariables :: (Functor f) => DPLL s f () eraseCurrentImplicationVariables :: DPLL s f () eraseCurrentImplicationVariables = do Set Variable xs <- Getting (Set Variable) (Storage s) (Set Variable) -> DPLL s f (Set Variable) forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a use (([(Maybe Variable, Set Variable)] -> Const (Set Variable) [(Maybe Variable, Set Variable)]) -> Storage s -> Const (Set Variable) (Storage s) forall s a. HasVariableLevels s a => Lens' s a variableLevels (([(Maybe Variable, Set Variable)] -> Const (Set Variable) [(Maybe Variable, Set Variable)]) -> Storage s -> Const (Set Variable) (Storage s)) -> ((Set Variable -> Const (Set Variable) (Set Variable)) -> [(Maybe Variable, Set Variable)] -> Const (Set Variable) [(Maybe Variable, Set Variable)]) -> Getting (Set Variable) (Storage s) (Set Variable) forall b c a. (b -> c) -> (a -> b) -> a -> c . ([(Maybe Variable, Set Variable)] -> (Maybe Variable, Set Variable)) -> Optic' (->) (Const (Set Variable)) [(Maybe Variable, Set Variable)] (Maybe Variable, Set Variable) forall (p :: * -> * -> *) (f :: * -> *) s a. (Profunctor p, Contravariant f) => (s -> a) -> Optic' p f s a to [(Maybe Variable, Set Variable)] -> (Maybe Variable, Set Variable) forall a. [a] -> a head Optic' (->) (Const (Set Variable)) [(Maybe Variable, Set Variable)] (Maybe Variable, Set Variable) -> ((Set Variable -> Const (Set Variable) (Set Variable)) -> (Maybe Variable, Set Variable) -> Const (Set Variable) (Maybe Variable, Set Variable)) -> (Set Variable -> Const (Set Variable) (Set Variable)) -> [(Maybe Variable, Set Variable)] -> Const (Set Variable) [(Maybe Variable, Set Variable)] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Set Variable -> Const (Set Variable) (Set Variable)) -> (Maybe Variable, Set Variable) -> Const (Set Variable) (Maybe Variable, Set Variable) forall s t a b. Field2 s t a b => Lens s t a b _2) ([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s) forall s a. HasVariableLevels s a => Lens' s a variableLevels (([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s)) -> ((Set Variable -> Identity (Set Variable)) -> [(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall b c a. (b -> c) -> (a -> b) -> a -> c . Index [(Maybe Variable, Set Variable)] -> Traversal' [(Maybe Variable, Set Variable)] (IxValue [(Maybe Variable, Set Variable)]) forall m. Ixed m => Index m -> Traversal' m (IxValue m) ix Index [(Maybe Variable, Set Variable)] 0 (((Maybe Variable, Set Variable) -> Identity (Maybe Variable, Set Variable)) -> [(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> ((Set Variable -> Identity (Set Variable)) -> (Maybe Variable, Set Variable) -> Identity (Maybe Variable, Set Variable)) -> (Set Variable -> Identity (Set Variable)) -> [(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Set Variable -> Identity (Set Variable)) -> (Maybe Variable, Set Variable) -> Identity (Maybe Variable, Set Variable) forall s t a b. Field2 s t a b => Lens s t a b _2 ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> Set Variable -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> b -> m () .= Set Variable forall a. Set a Set.empty (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall s a. HasUnassignedVariables s a => Lens' s a unassignedVariables ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> (Set Variable -> Set Variable) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Set Variable -> Set Variable -> Set Variable forall a. Ord a => Set a -> Set a -> Set a Set.union Set Variable xs (Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s) forall s a. HasAssignment s a => Lens' s a assignment ((Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s)) -> (Assignment -> Assignment) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Set Variable -> Assignment -> Assignment eraseVariables Set Variable xs learnClause :: (Functor f) => CNF.Clause -> DPLL s f () learnClause :: Clause -> DPLL s f () learnClause Clause c = do (Vector Clause -> Identity (Vector Clause)) -> Storage s -> Identity (Storage s) forall s a. HasClauses s a => Lens' s a clauses ((Vector Clause -> Identity (Vector Clause)) -> Storage s -> Identity (Storage s)) -> (Vector Clause -> Vector Clause) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= (Vector Clause -> Clause -> Vector Clause forall s a. Snoc s s a a => s -> a -> s |> Clause c) dropLevel :: (Functor f) => DPLL s f (Maybe (Maybe CNF.Variable, Set CNF.Variable)) dropLevel :: DPLL s f (Maybe (Maybe Variable, Set Variable)) dropLevel = do [(Maybe Variable, Set Variable)] lvs <- Getting [(Maybe Variable, Set Variable)] (Storage s) [(Maybe Variable, Set Variable)] -> DPLL s f [(Maybe Variable, Set Variable)] forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a use Getting [(Maybe Variable, Set Variable)] (Storage s) [(Maybe Variable, Set Variable)] forall s a. HasVariableLevels s a => Lens' s a variableLevels case [(Maybe Variable, Set Variable)] lvs of [] -> Maybe (Maybe Variable, Set Variable) -> DPLL s f (Maybe (Maybe Variable, Set Variable)) forall (f :: * -> *) a. Applicative f => a -> f a pure Maybe (Maybe Variable, Set Variable) forall a. Maybe a Nothing [(Maybe Variable, Set Variable) _] -> Maybe (Maybe Variable, Set Variable) -> DPLL s f (Maybe (Maybe Variable, Set Variable)) forall (f :: * -> *) a. Applicative f => a -> f a pure Maybe (Maybe Variable, Set Variable) forall a. Maybe a Nothing h :: (Maybe Variable, Set Variable) h@((Maybe Variable, Set Variable) -> Set Variable levelToSet -> Set Variable xs) : [(Maybe Variable, Set Variable)] t -> do ([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s) forall s a. HasVariableLevels s a => Lens' s a variableLevels (([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s)) -> [(Maybe Variable, Set Variable)] -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> b -> m () .= [(Maybe Variable, Set Variable)] t (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall s a. HasUnassignedVariables s a => Lens' s a unassignedVariables ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> (Set Variable -> Set Variable) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Set Variable -> Set Variable -> Set Variable forall a. Ord a => Set a -> Set a -> Set a Set.union Set Variable xs (Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s) forall s a. HasAssignment s a => Lens' s a assignment ((Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s)) -> (Assignment -> Assignment) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Set Variable -> Assignment -> Assignment eraseVariables Set Variable xs Maybe (Maybe Variable, Set Variable) -> DPLL s f (Maybe (Maybe Variable, Set Variable)) forall (f :: * -> *) a. Applicative f => a -> f a pure (Maybe (Maybe Variable, Set Variable) -> DPLL s f (Maybe (Maybe Variable, Set Variable))) -> Maybe (Maybe Variable, Set Variable) -> DPLL s f (Maybe (Maybe Variable, Set Variable)) forall a b. (a -> b) -> a -> b $ (Maybe Variable, Set Variable) -> Maybe (Maybe Variable, Set Variable) forall a. a -> Maybe a Just (Maybe Variable, Set Variable) h dropIrrelevantLevels :: (Functor f) => CNF.Clause -> DPLL s f () dropIrrelevantLevels :: Clause -> DPLL s f () dropIrrelevantLevels Clause c = do let cxs :: Set Variable cxs = Clause c Clause -> Getting (Endo [Variable]) Clause Variable -> [Variable] forall s a. s -> Getting (Endo [a]) s a -> [a] ^.. ([Literal] -> Const (Endo [Variable]) [Literal]) -> Clause -> Const (Endo [Variable]) Clause Iso' Clause [Literal] CNF.literalsOfClause (([Literal] -> Const (Endo [Variable]) [Literal]) -> Clause -> Const (Endo [Variable]) Clause) -> ((Variable -> Const (Endo [Variable]) Variable) -> [Literal] -> Const (Endo [Variable]) [Literal]) -> Getting (Endo [Variable]) Clause Variable forall b c a. (b -> c) -> (a -> b) -> a -> c . (Literal -> Const (Endo [Variable]) Literal) -> [Literal] -> Const (Endo [Variable]) [Literal] forall s t a b. Each s t a b => Traversal s t a b each ((Literal -> Const (Endo [Variable]) Literal) -> [Literal] -> Const (Endo [Variable]) [Literal]) -> ((Variable -> Const (Endo [Variable]) Variable) -> Literal -> Const (Endo [Variable]) Literal) -> (Variable -> Const (Endo [Variable]) Variable) -> [Literal] -> Const (Endo [Variable]) [Literal] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Literal -> Variable) -> (Variable -> Const (Endo [Variable]) Variable) -> Literal -> Const (Endo [Variable]) Literal forall (p :: * -> * -> *) (f :: * -> *) s a. (Profunctor p, Contravariant f) => (s -> a) -> Optic' p f s a to Literal -> Variable CNF.literalToVariable [Variable] -> ([Variable] -> Set Variable) -> Set Variable forall a b. a -> (a -> b) -> b & [Variable] -> Set Variable forall a. Ord a => [a] -> Set a Set.fromList [Set Variable] lvs <- LensLike' (Const [Set Variable]) (Storage s) [(Maybe Variable, Set Variable)] -> ([(Maybe Variable, Set Variable)] -> [Set Variable]) -> DPLL s f [Set Variable] forall s (m :: * -> *) r a. MonadState s m => LensLike' (Const r) s a -> (a -> r) -> m r uses LensLike' (Const [Set Variable]) (Storage s) [(Maybe Variable, Set Variable)] forall s a. HasVariableLevels s a => Lens' s a variableLevels ([(Maybe Variable, Set Variable)] -> Getting (Endo [Set Variable]) [(Maybe Variable, Set Variable)] (Set Variable) -> [Set Variable] forall s a. s -> Getting (Endo [a]) s a -> [a] ^.. (Set Variable -> Bool) -> Over (->) (TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable)) [(Maybe Variable, Set Variable)] [(Maybe Variable, Set Variable)] (Set Variable) (Set Variable) -> Getting (Endo [Set Variable]) [(Maybe Variable, Set Variable)] (Set Variable) forall (p :: * -> * -> *) (f :: * -> *) a s t. (Conjoined p, Applicative f) => (a -> Bool) -> Over p (TakingWhile p f a a) s t a a -> Over p f s t a a takingWhile (Set Variable -> Set Variable -> Bool forall a. Ord a => Set a -> Set a -> Bool Set.disjoint Set Variable cxs) (((Maybe Variable, Set Variable) -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) (Maybe Variable, Set Variable)) -> [(Maybe Variable, Set Variable)] -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) [(Maybe Variable, Set Variable)] forall s t a b. Each s t a b => Traversal s t a b each (((Maybe Variable, Set Variable) -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) (Maybe Variable, Set Variable)) -> [(Maybe Variable, Set Variable)] -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) [(Maybe Variable, Set Variable)]) -> ((Set Variable -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) (Set Variable)) -> (Maybe Variable, Set Variable) -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) (Maybe Variable, Set Variable)) -> Over (->) (TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable)) [(Maybe Variable, Set Variable)] [(Maybe Variable, Set Variable)] (Set Variable) (Set Variable) forall b c a. (b -> c) -> (a -> b) -> a -> c . ((Maybe Variable, Set Variable) -> Set Variable) -> (Set Variable -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) (Set Variable)) -> (Maybe Variable, Set Variable) -> TakingWhile (->) (Const (Endo [Set Variable])) (Set Variable) (Set Variable) (Maybe Variable, Set Variable) forall (p :: * -> * -> *) (f :: * -> *) s a. (Profunctor p, Contravariant f) => (s -> a) -> Optic' p f s a to (Maybe Variable, Set Variable) -> Set Variable levelToSet)) ([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s) forall s a. HasVariableLevels s a => Lens' s a variableLevels (([(Maybe Variable, Set Variable)] -> Identity [(Maybe Variable, Set Variable)]) -> Storage s -> Identity (Storage s)) -> ([(Maybe Variable, Set Variable)] -> [(Maybe Variable, Set Variable)]) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Int -> [(Maybe Variable, Set Variable)] -> [(Maybe Variable, Set Variable)] forall a. Int -> [a] -> [a] drop ([Set Variable] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [Set Variable] lvs) let xs :: Set Variable xs = [Set Variable] -> Set Variable forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a Set.unions [Set Variable] lvs (Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s) forall s a. HasUnassignedVariables s a => Lens' s a unassignedVariables ((Set Variable -> Identity (Set Variable)) -> Storage s -> Identity (Storage s)) -> (Set Variable -> Set Variable) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Set Variable -> Set Variable -> Set Variable forall a. Ord a => Set a -> Set a -> Set a Set.union Set Variable xs (Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s) forall s a. HasAssignment s a => Lens' s a assignment ((Assignment -> Identity Assignment) -> Storage s -> Identity (Storage s)) -> (Assignment -> Assignment) -> DPLL s f () forall s (m :: * -> *) a b. MonadState s m => ASetter s s a b -> (a -> b) -> m () %= Set Variable -> Assignment -> Assignment eraseVariables Set Variable xs deriveConflictClauseRelSAT :: (Functor f) => CNF.Clause -> DPLL s f CNF.Clause deriveConflictClauseRelSAT :: Clause -> DPLL s f Clause deriveConflictClauseRelSAT Clause c = do Assignment asgn <- Getting Assignment (Storage s) Assignment -> 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 (Maybe Variable _, Set Variable vl) <- LensLike' (Const (Maybe Variable, Set Variable)) (Storage s) [(Maybe Variable, Set Variable)] -> ([(Maybe Variable, Set Variable)] -> (Maybe Variable, Set Variable)) -> DPLL s f (Maybe Variable, Set Variable) forall s (m :: * -> *) r a. MonadState s m => LensLike' (Const r) s a -> (a -> r) -> m r uses LensLike' (Const (Maybe Variable, Set Variable)) (Storage s) [(Maybe Variable, Set Variable)] forall s a. HasVariableLevels s a => Lens' s a variableLevels [(Maybe Variable, Set Variable)] -> (Maybe Variable, Set Variable) forall a. [a] -> a head Clause -> DPLL s f Clause forall (f :: * -> *) a. Applicative f => a -> f a pure (Clause -> DPLL s f Clause) -> ([Literal] -> Clause) -> [Literal] -> DPLL s f Clause forall b c a. (b -> c) -> (a -> b) -> a -> c . [Literal] -> Clause CNF.Clause ([Literal] -> Clause) -> ([Literal] -> [Literal]) -> [Literal] -> Clause forall b c a. (b -> c) -> (a -> b) -> a -> c . Set Literal -> [Literal] forall a. Set a -> [a] Set.toList (Set Literal -> [Literal]) -> ([Literal] -> Set Literal) -> [Literal] -> [Literal] forall b c a. (b -> c) -> (a -> b) -> a -> c . Assignment -> Set Variable -> [Literal] -> Set Literal go Assignment asgn Set Variable vl ([Literal] -> DPLL s f Clause) -> [Literal] -> DPLL s f Clause forall a b. (a -> b) -> a -> b $ Clause c Clause -> Getting [Literal] Clause [Literal] -> [Literal] forall s a. s -> Getting a s a -> a ^. Getting [Literal] Clause [Literal] Iso' Clause [Literal] CNF.literalsOfClause where go :: Assignment -> Set Variable -> [Literal] -> Set Literal go Assignment asgn Set Variable vl [Literal] ls | [Literal] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Literal] psAtCurrent = [Literal] -> Set Literal forall a. Ord a => [a] -> Set a Set.fromList [Literal] lsWithoutP Set Literal -> Set Literal -> Set Literal forall a. Semigroup a => a -> a -> a <> [Literal] -> Set Literal forall a. Ord a => [a] -> Set a Set.fromList [Literal] psAtLower | Bool otherwise = [Literal] -> Set Literal forall a. Ord a => [a] -> Set a Set.fromList [Literal] lsWithoutP Set Literal -> Set Literal -> Set Literal forall a. Semigroup a => a -> a -> a <> [Literal] -> Set Literal forall a. Ord a => [a] -> Set a Set.fromList [Literal] psAtLower Set Literal -> Set Literal -> Set Literal forall a. Semigroup a => a -> a -> a <> Assignment -> Set Variable -> [Literal] -> Set Literal go Assignment asgn Set Variable vl [Literal] psAtCurrent where ([Literal] psAtCurrent, [Literal] psAtLower) = (Literal -> Bool) -> [Literal] -> ([Literal], [Literal]) forall a. (a -> Bool) -> [a] -> ([a], [a]) partition ((Variable -> Set Variable -> Bool forall a. Ord a => a -> Set a -> Bool `Set.member` Set Variable vl) (Variable -> Bool) -> (Literal -> Variable) -> Literal -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . Literal -> Variable CNF.literalToVariable) [Literal] ps ([Literal] lsWithoutP, [Literal] ps) = [Either Literal Literal] -> ([Literal], [Literal]) forall a b. [Either a b] -> ([a], [b]) partitionEithers ([Either Literal Literal] -> ([Literal], [Literal])) -> ((Literal -> [Either Literal Literal]) -> [Either Literal Literal]) -> (Literal -> [Either Literal Literal]) -> ([Literal], [Literal]) forall b c a. (b -> c) -> (a -> b) -> a -> c . ((Literal -> [Either Literal Literal]) -> [Literal] -> [Either Literal Literal]) -> [Literal] -> (Literal -> [Either Literal Literal]) -> [Either Literal Literal] forall a b c. (a -> b -> c) -> b -> a -> c flip (Literal -> [Either Literal Literal]) -> [Literal] -> [Either Literal Literal] forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b] concatMap [Literal] ls ((Literal -> [Either Literal Literal]) -> ([Literal], [Literal])) -> (Literal -> [Either Literal Literal]) -> ([Literal], [Literal]) forall a b. (a -> b) -> a -> b $ \Literal l -> Assignment asgn Assignment -> Getting (Endo [Either Literal Literal]) Assignment (Either Literal Literal) -> [Either Literal Literal] forall s a. s -> Getting (Endo [a]) s a -> [a] ^.. Literal -> Traversal' Assignment (Maybe Clause) parentsOfLiteral Literal l ((Maybe Clause -> Const (Endo [Either Literal Literal]) (Maybe Clause)) -> Assignment -> Const (Endo [Either Literal Literal]) Assignment) -> ((Either Literal Literal -> Const (Endo [Either Literal Literal]) (Either Literal Literal)) -> Maybe Clause -> Const (Endo [Either Literal Literal]) (Maybe Clause)) -> Getting (Endo [Either Literal Literal]) Assignment (Either Literal Literal) forall b c a. (b -> c) -> (a -> b) -> a -> c . Traversing (->) (Const (Endo [Either Literal Literal])) (Maybe Clause) (Maybe Clause) (Either Literal Literal) (Either Literal Literal) -> ((Either Literal Literal -> Const (Endo [Either Literal Literal]) (Either Literal Literal)) -> Maybe Clause -> Const (Endo [Either Literal Literal]) (Maybe Clause)) -> (Either Literal Literal -> Const (Endo [Either Literal Literal]) (Either Literal Literal)) -> Maybe Clause -> Const (Endo [Either Literal Literal]) (Maybe Clause) forall (p :: * -> * -> *) (f :: * -> *) s t a b. (Conjoined p, Applicative f) => Traversing p f s t a b -> Over p f s t a b -> Over p f s t a b failing ((Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Clause) -> Maybe Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) (Maybe Clause) forall a b. Prism (Maybe a) (Maybe b) a b _Just ((Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Clause) -> Maybe Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) (Maybe Clause)) -> ((Either Literal Literal -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) (Either Literal Literal)) -> Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Clause) -> Traversing (->) (Const (Endo [Either Literal Literal])) (Maybe Clause) (Maybe Clause) (Either Literal Literal) (Either Literal Literal) forall b c a. (b -> c) -> (a -> b) -> a -> c . Literal -> (Literal -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Literal) -> Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Clause forall (f :: * -> *). Applicative f => Literal -> (Literal -> f Literal) -> Clause -> f Clause literalsInParentsOf Literal l ((Literal -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Literal) -> Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Clause) -> ((Either Literal Literal -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) (Either Literal Literal)) -> Literal -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Literal) -> (Either Literal Literal -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) (Either Literal Literal)) -> Clause -> BazaarT (->) (Const (Endo [Either Literal Literal])) (Either Literal Literal) (Either Literal Literal) Clause forall b c a. (b -> c) -> (a -> b) -> a -> c . AReview (Either Literal Literal) Literal -> Getter Literal (Either Literal Literal) forall t b. AReview t b -> Getter b t re AReview (Either Literal Literal) Literal forall c a b. Prism (Either c a) (Either c b) a b _Right) ((() -> Const (Endo [Either Literal Literal]) ()) -> Maybe Clause -> Const (Endo [Either Literal Literal]) (Maybe Clause) forall a. Prism' (Maybe a) () _Nothing ((() -> Const (Endo [Either Literal Literal]) ()) -> Maybe Clause -> Const (Endo [Either Literal Literal]) (Maybe Clause)) -> ((Either Literal Literal -> Const (Endo [Either Literal Literal]) (Either Literal Literal)) -> () -> Const (Endo [Either Literal Literal]) ()) -> (Either Literal Literal -> Const (Endo [Either Literal Literal]) (Either Literal Literal)) -> Maybe Clause -> Const (Endo [Either Literal Literal]) (Maybe Clause) forall b c a. (b -> c) -> (a -> b) -> a -> c . Either Literal Literal -> (Either Literal Literal -> Const (Endo [Either Literal Literal]) (Either Literal Literal)) -> () -> Const (Endo [Either Literal Literal]) () forall (p :: * -> * -> *) (f :: * -> *) a s. (Profunctor p, Contravariant f, Functor f) => a -> Optic' p f s a like (Literal -> Either Literal Literal forall a b. a -> Either a b Left Literal l)) literalsInParentsOf :: Literal -> (Literal -> f Literal) -> Clause -> f Clause literalsInParentsOf Literal l = ([Literal] -> f [Literal]) -> Clause -> f Clause Iso' Clause [Literal] CNF.literalsOfClause (([Literal] -> f [Literal]) -> Clause -> f Clause) -> ((Literal -> f Literal) -> [Literal] -> f [Literal]) -> (Literal -> f Literal) -> Clause -> f Clause forall b c a. (b -> c) -> (a -> b) -> a -> c . (Literal -> f Literal) -> [Literal] -> f [Literal] forall s t a b. Each s t a b => Traversal s t a b each ((Literal -> f Literal) -> [Literal] -> f [Literal]) -> ((Literal -> f Literal) -> Literal -> f Literal) -> (Literal -> f Literal) -> [Literal] -> f [Literal] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Literal -> Bool) -> (Literal -> f Literal) -> Literal -> f Literal forall (p :: * -> * -> *) (f :: * -> *) a. (Choice p, Applicative f) => (a -> Bool) -> Optic' p f a a filtered (Literal -> Literal -> Bool forall a. Eq a => a -> a -> Bool /= Literal -> Literal CNF.negateLiteral Literal l) levelToSet :: (Maybe CNF.Variable, Set CNF.Variable) -> Set CNF.Variable levelToSet :: (Maybe Variable, Set Variable) -> Set Variable levelToSet (Maybe Variable dx, Set Variable xs) = Set Variable -> (Variable -> Set Variable) -> Maybe Variable -> Set Variable forall b a. b -> (a -> b) -> Maybe a -> b maybe Set Variable forall a. Set a Set.empty Variable -> Set Variable forall a. a -> Set a Set.singleton Maybe Variable dx Set Variable -> Set Variable -> Set Variable forall a. Semigroup a => a -> a -> a <> Set Variable xs