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