{-# 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