{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE TemplateHaskell #-} module Satyros.DPLL.Storage where import Control.Lens (makeFieldsNoPrefix, set, to, (&), (.~), (^.)) import Data.Set (Set) import Data.Vector (Vector) import qualified Satyros.CNF as CNF import Satyros.DPLL.Assignment (Assignment) import System.Random (RandomGen (..), StdGen) data Storage s = Storage { Storage s -> Set Variable _unassignedVariables :: Set CNF.Variable , Storage s -> Vector Clause _clauses :: Vector CNF.Clause , Storage s -> Assignment _assignment :: Assignment , Storage s -> [(Maybe Variable, Set Variable)] _variableLevels :: [(Maybe CNF.Variable, Set CNF.Variable)] , Storage s -> StdGen _stdGen :: StdGen , Storage s -> s _theory :: s } deriving stock (Int -> Storage s -> ShowS [Storage s] -> ShowS Storage s -> String (Int -> Storage s -> ShowS) -> (Storage s -> String) -> ([Storage s] -> ShowS) -> Show (Storage s) forall s. Show s => Int -> Storage s -> ShowS forall s. Show s => [Storage s] -> ShowS forall s. Show s => Storage s -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Storage s] -> ShowS $cshowList :: forall s. Show s => [Storage s] -> ShowS show :: Storage s -> String $cshow :: forall s. Show s => Storage s -> String showsPrec :: Int -> Storage s -> ShowS $cshowsPrec :: forall s. Show s => Int -> Storage s -> ShowS Show) makeFieldsNoPrefix ''Storage instance RandomGen (Storage s) where split :: Storage s -> (Storage s, Storage s) split Storage s s = let (StdGen stdGen0, StdGen stdGen1) = Storage s s Storage s -> Getting (StdGen, StdGen) (Storage s) (StdGen, StdGen) -> (StdGen, StdGen) forall s a. s -> Getting a s a -> a ^. (StdGen -> Const (StdGen, StdGen) StdGen) -> Storage s -> Const (StdGen, StdGen) (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen ((StdGen -> Const (StdGen, StdGen) StdGen) -> Storage s -> Const (StdGen, StdGen) (Storage s)) -> (((StdGen, StdGen) -> Const (StdGen, StdGen) (StdGen, StdGen)) -> StdGen -> Const (StdGen, StdGen) StdGen) -> Getting (StdGen, StdGen) (Storage s) (StdGen, StdGen) forall b c a. (b -> c) -> (a -> b) -> a -> c . (StdGen -> (StdGen, StdGen)) -> ((StdGen, StdGen) -> Const (StdGen, StdGen) (StdGen, StdGen)) -> StdGen -> Const (StdGen, StdGen) StdGen forall (p :: * -> * -> *) (f :: * -> *) s a. (Profunctor p, Contravariant f) => (s -> a) -> Optic' p f s a to StdGen -> (StdGen, StdGen) forall g. RandomGen g => g -> (g, g) split in (Storage s s Storage s -> (Storage s -> Storage s) -> Storage s forall a b. a -> (a -> b) -> b & (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen ((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t .~ StdGen stdGen0, Storage s s Storage s -> (Storage s -> Storage s) -> Storage s forall a b. a -> (a -> b) -> b & (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen ((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t .~ StdGen stdGen1) genWord8 :: Storage s -> (Word8, Storage s) genWord8 Storage s s = (StdGen -> Storage s -> Storage s) -> Storage s -> StdGen -> Storage s forall a b c. (a -> b -> c) -> b -> a -> c flip (((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t set (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen) Storage s s (StdGen -> Storage s) -> (Word8, StdGen) -> (Word8, Storage s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StdGen -> (Word8, StdGen) forall g. RandomGen g => g -> (Word8, g) genWord8 (Storage s s Storage s -> Getting StdGen (Storage s) StdGen -> StdGen forall s a. s -> Getting a s a -> a ^. Getting StdGen (Storage s) StdGen forall s a. HasStdGen s a => Lens' s a stdGen) genWord16 :: Storage s -> (Word16, Storage s) genWord16 Storage s s = (StdGen -> Storage s -> Storage s) -> Storage s -> StdGen -> Storage s forall a b c. (a -> b -> c) -> b -> a -> c flip (((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t set (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen) Storage s s (StdGen -> Storage s) -> (Word16, StdGen) -> (Word16, Storage s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StdGen -> (Word16, StdGen) forall g. RandomGen g => g -> (Word16, g) genWord16 (Storage s s Storage s -> Getting StdGen (Storage s) StdGen -> StdGen forall s a. s -> Getting a s a -> a ^. Getting StdGen (Storage s) StdGen forall s a. HasStdGen s a => Lens' s a stdGen) genWord32 :: Storage s -> (Word32, Storage s) genWord32 Storage s s = (StdGen -> Storage s -> Storage s) -> Storage s -> StdGen -> Storage s forall a b c. (a -> b -> c) -> b -> a -> c flip (((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t set (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen) Storage s s (StdGen -> Storage s) -> (Word32, StdGen) -> (Word32, Storage s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StdGen -> (Word32, StdGen) forall g. RandomGen g => g -> (Word32, g) genWord32 (Storage s s Storage s -> Getting StdGen (Storage s) StdGen -> StdGen forall s a. s -> Getting a s a -> a ^. Getting StdGen (Storage s) StdGen forall s a. HasStdGen s a => Lens' s a stdGen) genWord64 :: Storage s -> (Word64, Storage s) genWord64 Storage s s = (StdGen -> Storage s -> Storage s) -> Storage s -> StdGen -> Storage s forall a b c. (a -> b -> c) -> b -> a -> c flip (((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t set (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen) Storage s s (StdGen -> Storage s) -> (Word64, StdGen) -> (Word64, Storage s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> StdGen -> (Word64, StdGen) forall g. RandomGen g => g -> (Word64, g) genWord64 (Storage s s Storage s -> Getting StdGen (Storage s) StdGen -> StdGen forall s a. s -> Getting a s a -> a ^. Getting StdGen (Storage s) StdGen forall s a. HasStdGen s a => Lens' s a stdGen) genWord32R :: Word32 -> Storage s -> (Word32, Storage s) genWord32R Word32 u Storage s s = (StdGen -> Storage s -> Storage s) -> Storage s -> StdGen -> Storage s forall a b c. (a -> b -> c) -> b -> a -> c flip (((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t set (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen) Storage s s (StdGen -> Storage s) -> (Word32, StdGen) -> (Word32, Storage s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Word32 -> StdGen -> (Word32, StdGen) forall g. RandomGen g => Word32 -> g -> (Word32, g) genWord32R Word32 u (Storage s s Storage s -> Getting StdGen (Storage s) StdGen -> StdGen forall s a. s -> Getting a s a -> a ^. Getting StdGen (Storage s) StdGen forall s a. HasStdGen s a => Lens' s a stdGen) genWord64R :: Word64 -> Storage s -> (Word64, Storage s) genWord64R Word64 u Storage s s = (StdGen -> Storage s -> Storage s) -> Storage s -> StdGen -> Storage s forall a b c. (a -> b -> c) -> b -> a -> c flip (((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t set (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen) Storage s s (StdGen -> Storage s) -> (Word64, StdGen) -> (Word64, Storage s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Word64 -> StdGen -> (Word64, StdGen) forall g. RandomGen g => Word64 -> g -> (Word64, g) genWord64R Word64 u (Storage s s Storage s -> Getting StdGen (Storage s) StdGen -> StdGen forall s a. s -> Getting a s a -> a ^. Getting StdGen (Storage s) StdGen forall s a. HasStdGen s a => Lens' s a stdGen) genShortByteString :: Int -> Storage s -> (ShortByteString, Storage s) genShortByteString Int n Storage s s = (StdGen -> Storage s -> Storage s) -> Storage s -> StdGen -> Storage s forall a b c. (a -> b -> c) -> b -> a -> c flip (((StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s)) -> StdGen -> Storage s -> Storage s forall s t a b. ASetter s t a b -> b -> s -> t set (StdGen -> Identity StdGen) -> Storage s -> Identity (Storage s) forall s a. HasStdGen s a => Lens' s a stdGen) Storage s s (StdGen -> Storage s) -> (ShortByteString, StdGen) -> (ShortByteString, Storage s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Int -> StdGen -> (ShortByteString, StdGen) forall g. RandomGen g => Int -> g -> (ShortByteString, g) genShortByteString Int n (Storage s s Storage s -> Getting StdGen (Storage s) StdGen -> StdGen forall s a. s -> Getting a s a -> a ^. Getting StdGen (Storage s) StdGen forall s a. HasStdGen s a => Lens' s a stdGen)