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