{-# LANGUAGE ViewPatterns #-}
module Satyros.DPLL.Backtrace where

import           Control.Lens             (each, to, (&), (^.), (^..))
import           Data.List                (find)
import           Data.Maybe               (fromJust)
import qualified Data.Set                 as Set
import qualified Satyros.CNF              as CNF
import           Satyros.DPLL.Effect      (DPLL, backtraceComplete,
                                           backtraceExhaustion)
import           Satyros.DPLL.StorageUtil (assignFailureDrivenVariable,
                                           dropIrrelevantLevels, dropLevel,
                                           learnClause, levelToSet)
import           System.Random.Stateful   (StateGenM (StateGenM), randomRM)

backtrace :: (Functor f) => CNF.Clause -> DPLL s f ()
backtrace :: Clause -> DPLL s f ()
backtrace Clause
cdc = do
  Clause -> DPLL s f ()
forall (f :: * -> *) s. Functor f => Clause -> DPLL s f ()
learnClause Clause
cdc
  Clause -> DPLL s f ()
forall (f :: * -> *) s. Functor f => Clause -> DPLL s f ()
dropIrrelevantLevels Clause
cdc
  Maybe (Maybe Variable, Set Variable)
mayLv <- DPLL s f (Maybe (Maybe Variable, Set Variable))
forall (f :: * -> *) s.
Functor f =>
DPLL s f (Maybe (Maybe Variable, Set Variable))
dropLevel
  case Maybe (Maybe Variable, Set Variable)
mayLv of
    Just ((Maybe Variable, Set Variable) -> Set Variable
levelToSet -> Set Variable
lvSet) -> do
      let
        revertibleXs :: Set Variable
revertibleXs =
          Clause
cdc
          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
& Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Variable
lvSet
          (Set Variable -> Set Variable)
-> ([Variable] -> Set Variable) -> [Variable] -> Set Variable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Variable] -> Set Variable
forall a. Ord a => [a] -> Set a
Set.fromList
      Int
i <- (Int, Int) -> StateGenM (Storage s) -> DPLL s f Int
forall g r (m :: * -> *) a.
(RandomGenM g r m, Random a) =>
(a, a) -> g -> m a
randomRM (Int
0, Set Variable -> Int
forall a. Set a -> Int
Set.size Set Variable
revertibleXs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) StateGenM (Storage s)
forall g. StateGenM g
StateGenM
      let
        x :: Variable
x = Int -> Set Variable -> Variable
forall a. Int -> Set a -> a
Set.elemAt Int
i Set Variable
revertibleXs
        l :: Literal
l = Clause
cdc Clause -> Getting [Literal] Clause [Literal] -> [Literal]
forall s a. s -> Getting a s a -> a
^. Getting [Literal] Clause [Literal]
Iso' Clause [Literal]
CNF.literalsOfClause [Literal] -> ([Literal] -> Literal) -> Literal
forall a b. a -> (a -> b) -> b
& Maybe Literal -> Literal
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Literal -> Literal)
-> ([Literal] -> Maybe Literal) -> [Literal] -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Literal -> Bool) -> [Literal] -> Maybe Literal
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Variable -> Variable -> Bool
forall a. Eq a => a -> a -> Bool
== Variable
x) (Variable -> Bool) -> (Literal -> Variable) -> Literal -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Literal -> Variable
CNF.literalToVariable)
      Clause -> Literal -> DPLL s f ()
forall (f :: * -> *) s.
Functor f =>
Clause -> Literal -> DPLL s f ()
backtraceComplete Clause
cdc Literal
l
    Maybe (Maybe Variable, Set Variable)
Nothing -> DPLL s f ()
forall (f :: * -> *) s. Functor f => DPLL s f ()
backtraceExhaustion

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