{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TemplateHaskell        #-}
{-# LANGUAGE ViewPatterns           #-}
module Satyros.DPLL.Storage where

import           Control.Lens            (each, makeFieldsNoPrefix, set, to,
                                          (&), (.~), (^.), (^..), (^?))
import           Control.Monad           (forM_, unless, when)
import           Control.Monad.Except    (throwError)
import           Data.List               (partition)
import qualified Data.Map                as Map
import           Data.Set                (Set)
import qualified Data.Set                as Set
import           Data.Vector             (Vector)
import qualified Data.Vector             as Vector
import           GHC.Generics            (Generic, Generic1)
import qualified Satyros.CNF             as CNF
import           Satyros.DPLL.Assignment (Assignment (Assignment),
                                          valueOfVariable)
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 ((forall x. Storage s -> Rep (Storage s) x)
-> (forall x. Rep (Storage s) x -> Storage s)
-> Generic (Storage s)
forall x. Rep (Storage s) x -> Storage s
forall x. Storage s -> Rep (Storage s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s x. Rep (Storage s) x -> Storage s
forall s x. Storage s -> Rep (Storage s) x
$cto :: forall s x. Rep (Storage s) x -> Storage s
$cfrom :: forall s x. Storage s -> Rep (Storage s) x
Generic, (forall a. Storage a -> Rep1 Storage a)
-> (forall a. Rep1 Storage a -> Storage a) -> Generic1 Storage
forall a. Rep1 Storage a -> Storage a
forall a. Storage a -> Rep1 Storage a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 Storage a -> Storage a
$cfrom1 :: forall a. Storage a -> Rep1 Storage a
Generic1, 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)

data StorageInitializationFailure
  = EmptyClause
  | InitialConflict

initializeStorage :: CNF.Formula -> StdGen -> s -> Either StorageInitializationFailure (Storage s)
initializeStorage :: Formula
-> StdGen -> s -> Either StorageInitializationFailure (Storage s)
initializeStorage Formula
f StdGen
_stdGen s
_theory = do
  Bool
-> Either StorageInitializationFailure ()
-> Either StorageInitializationFailure ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Clause] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Clause]
emptyCs) (Either StorageInitializationFailure ()
 -> Either StorageInitializationFailure ())
-> Either StorageInitializationFailure ()
-> Either StorageInitializationFailure ()
forall a b. (a -> b) -> a -> b
$
    StorageInitializationFailure
-> Either StorageInitializationFailure ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError StorageInitializationFailure
EmptyClause
  [(Variable, (Bool, Maybe Clause))]
-> ((Variable, (Bool, Maybe Clause))
    -> Either StorageInitializationFailure ())
-> Either StorageInitializationFailure ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Variable, (Bool, Maybe Clause))]
initialAssignmentPairs (((Variable, (Bool, Maybe Clause))
  -> Either StorageInitializationFailure ())
 -> Either StorageInitializationFailure ())
-> ((Variable, (Bool, Maybe Clause))
    -> Either StorageInitializationFailure ())
-> Either StorageInitializationFailure ()
forall a b. (a -> b) -> a -> b
$ \(Variable
x, (Bool, Maybe Clause) -> Bool
forall a b. (a, b) -> a
fst -> Bool
b) ->
    Bool
-> Either StorageInitializationFailure ()
-> Either StorageInitializationFailure ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Assignment
_assignment Assignment -> Getting (First Bool) Assignment Bool -> Maybe Bool
forall s a. s -> Getting (First a) s a -> Maybe a
^? Variable -> Traversal' Assignment Bool
valueOfVariable Variable
x Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Bool
not Bool
b)) (Either StorageInitializationFailure ()
 -> Either StorageInitializationFailure ())
-> Either StorageInitializationFailure ()
-> Either StorageInitializationFailure ()
forall a b. (a -> b) -> a -> b
$
      StorageInitializationFailure
-> Either StorageInitializationFailure ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError StorageInitializationFailure
InitialConflict

  Storage s -> Either StorageInitializationFailure (Storage s)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Storage :: forall s.
Set Variable
-> Vector Clause
-> Assignment
-> [(Maybe Variable, Set Variable)]
-> StdGen
-> s
-> Storage s
Storage{s
[(Maybe Variable, Set Variable)]
Set Variable
Vector Clause
StdGen
Assignment
_variableLevels :: [(Maybe Variable, Set Variable)]
_clauses :: Vector Clause
_unassignedVariables :: Set Variable
_assignment :: Assignment
_theory :: s
_stdGen :: StdGen
_theory :: s
_stdGen :: StdGen
_variableLevels :: [(Maybe Variable, Set Variable)]
_assignment :: Assignment
_clauses :: Vector Clause
_unassignedVariables :: Set Variable
..}
  where
    _unassignedVariables :: Set Variable
_unassignedVariables = Set Variable
allVariables Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Variable
initiallyAssignedVs
    _clauses :: Vector Clause
_clauses = [Clause] -> Vector Clause
forall a. [a] -> Vector a
Vector.fromList [Clause]
nonunitCs
    _assignment :: Assignment
_assignment = Map Variable (Bool, Maybe Clause) -> Assignment
Assignment (Map Variable (Bool, Maybe Clause) -> Assignment)
-> Map Variable (Bool, Maybe Clause) -> Assignment
forall a b. (a -> b) -> a -> b
$ [(Variable, (Bool, Maybe Clause))]
-> Map Variable (Bool, Maybe Clause)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Variable, (Bool, Maybe Clause))]
initialAssignmentPairs
    _variableLevels :: [(Maybe Variable, Set Variable)]
_variableLevels = [(Maybe Variable
forall a. Maybe a
Nothing, Set Variable
initiallyAssignedVs)]

    allVariables :: Set Variable
allVariables = [Variable] -> Set Variable
forall a. Ord a => [a] -> Set a
Set.fromList ([Variable] -> Set Variable) -> [Variable] -> Set Variable
forall a b. (a -> b) -> a -> b
$ (Word -> Variable) -> [Word] -> [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Word -> Variable
CNF.Variable [Word
1..Word
mv]
    CNF.Variable Word
mv = Formula -> Variable
CNF.maxVariableInFormula Formula
f

    initiallyAssignedVs :: Set Variable
initiallyAssignedVs = [Variable] -> Set Variable
forall a. Ord a => [a] -> Set a
Set.fromList ([Variable] -> Set Variable) -> [Variable] -> Set Variable
forall a b. (a -> b) -> a -> b
$ ((Variable, (Bool, Maybe Clause)) -> Variable)
-> [(Variable, (Bool, Maybe Clause))] -> [Variable]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable, (Bool, Maybe Clause)) -> Variable
forall a b. (a, b) -> a
fst [(Variable, (Bool, Maybe Clause))]
initialAssignmentPairs
    initialAssignmentPairs :: [(Variable, (Bool, Maybe Clause))]
initialAssignmentPairs =
      [(Variable
v, (Positivity
pos Positivity -> Getting Bool Positivity Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool Positivity Bool
Iso' Positivity Bool
CNF.isPositive, Maybe Clause
forall a. Maybe a
Nothing)) | CNF.Literal Positivity
pos Variable
v <- [Literal]
cnfLits]
    cnfLits :: [Literal]
cnfLits = [Clause]
unitCs [Clause] -> Getting (Endo [Literal]) [Clause] Literal -> [Literal]
forall s a. s -> Getting (Endo [a]) s a -> [a]
^.. (Clause -> Const (Endo [Literal]) Clause)
-> [Clause] -> Const (Endo [Literal]) [Clause]
forall s t a b. Each s t a b => Traversal s t a b
each ((Clause -> Const (Endo [Literal]) Clause)
 -> [Clause] -> Const (Endo [Literal]) [Clause])
-> ((Literal -> Const (Endo [Literal]) Literal)
    -> Clause -> Const (Endo [Literal]) Clause)
-> Getting (Endo [Literal]) [Clause] Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Literal] -> Const (Endo [Literal]) [Literal])
-> Clause -> Const (Endo [Literal]) Clause
Iso' Clause [Literal]
CNF.literalsOfClause (([Literal] -> Const (Endo [Literal]) [Literal])
 -> Clause -> Const (Endo [Literal]) Clause)
-> ((Literal -> Const (Endo [Literal]) Literal)
    -> [Literal] -> Const (Endo [Literal]) [Literal])
-> (Literal -> Const (Endo [Literal]) Literal)
-> Clause
-> Const (Endo [Literal]) Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Literal -> Const (Endo [Literal]) Literal)
-> [Literal] -> Const (Endo [Literal]) [Literal]
forall s t a b. Each s t a b => Traversal s t a b
each

    ([Clause]
unitCs, [Clause]
nonunitCs) = (Clause -> Bool) -> [Clause] -> ([Clause], [Clause])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Clause -> Bool
CNF.unitClause [Clause]
nonemptyCs
    ([Clause]
emptyCs, [Clause]
nonemptyCs) = (Clause -> Bool) -> [Clause] -> ([Clause], [Clause])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Clause -> Bool
CNF.emptyClause [Clause]
cs
    cs :: [Clause]
cs = Formula
f Formula -> Getting [Clause] Formula [Clause] -> [Clause]
forall s a. s -> Getting a s a -> a
^. Getting [Clause] Formula [Clause]
Iso' Formula [Clause]
CNF.clausesOfFormula