{-# 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.Extra         (nubOrd, 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 = Set Literal
nonRecursiveConflictSet
      | Bool
otherwise = Set Literal
nonRecursiveConflictSet 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
        nonRecursiveConflictSet :: Set Literal
nonRecursiveConflictSet = [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
        ([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] -> [Literal]
forall a. Ord a => [a] -> [a]
nubOrd -> [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 -> Literal
CNF.negateLiteral 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 (Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> (Literal -> Bool) -> Literal -> Bool -> Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
/= Literal
l) (Literal -> Bool -> Bool) -> (Literal -> Bool) -> Literal -> Bool
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (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