Satyros.DPLL.Storage

Documentation

data Storage s

Constructors

Storage

Fields

• _unassignedVariables :: Set Variable
• _clauses :: Vector Clause
• _assignment :: Assignment
• _variableLevels :: [(Maybe Variable, Set Variable)]
• _stdGen :: StdGen
• _theory :: s

Instances

Show s => Show (Storage s)

Defined in Satyros.DPLL.Storage

Methods

showsPrec :: Int -> Storage s -> ShowS

show :: Storage s -> String

showList :: [Storage s] -> ShowS

Generic (Storage s)

Defined in Satyros.DPLL.Storage

Associated Types

type Rep (Storage s) :: Type -> Type

Methods

from :: Storage s -> Rep (Storage s) x

to :: Rep (Storage s) x -> Storage s

RandomGen (Storage s)

Defined in Satyros.DPLL.Storage

Methods

next :: Storage s -> (Int, Storage s)

genWord8 :: Storage s -> (Word8, Storage s)

genWord16 :: Storage s -> (Word16, Storage s)

genWord32 :: Storage s -> (Word32, Storage s)

genWord64 :: Storage s -> (Word64, Storage s)

genWord32R :: Word32 -> Storage s -> (Word32, Storage s)

genWord64R :: Word64 -> Storage s -> (Word64, Storage s)

genShortByteString :: Int -> Storage s -> (ShortByteString, Storage s)

genRange :: Storage s -> (Int, Int)

split :: Storage s -> (Storage s, Storage s)

Generic1 Storage

Defined in Satyros.DPLL.Storage

Associated Types

type Rep1 Storage :: k -> Type

Methods

from1 :: forall (a :: k). Storage a -> Rep1 Storage a

to1 :: forall (a :: k). Rep1 Storage a -> Storage a

HasTheory (Storage s) s

Defined in Satyros.DPLL.Storage

Methods

theory :: Lens' (Storage s) s

HasStdGen (Storage s) StdGen

Defined in Satyros.DPLL.Storage

Methods

stdGen :: Lens' (Storage s) StdGen

HasAssignment (Storage s) Assignment

Defined in Satyros.DPLL.Storage

Methods

assignment :: Lens' (Storage s) Assignment

HasVariableLevels (Storage s) [(Maybe Variable, Set Variable)]

Defined in Satyros.DPLL.Storage

Methods

variableLevels :: Lens' (Storage s) [(Maybe Variable, Set Variable)]

HasUnassignedVariables (Storage s) (Set Variable)

Defined in Satyros.DPLL.Storage

Methods

unassignedVariables :: Lens' (Storage s) (Set Variable)

HasClauses (Storage s) (Vector Clause)

Defined in Satyros.DPLL.Storage

Methods

clauses :: Lens' (Storage s) (Vector Clause)

Functor f => MonadState (Storage s) (DPLL s f)

Defined in Satyros.DPLL.Effect

Methods

get :: DPLL s f (Storage s)

put :: Storage s -> DPLL s f ()

state :: (Storage s -> (a, Storage s)) -> DPLL s f a

type Rep (Storage s)

Defined in Satyros.DPLL.Storage

type Rep (Storage s) = D1 ('MetaData "Storage" "Satyros.DPLL.Storage" "satyros-0.3.1.4-3YwMxGnZD0k1OVgpDx5SHB" 'False) (C1 ('MetaCons "Storage" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_unassignedVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Variable)) :*: (S1 ('MetaSel ('Just "_clauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vector Clause)) :*: S1 ('MetaSel ('Just "_assignment") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assignment))) :*: (S1 ('MetaSel ('Just "_variableLevels") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Maybe Variable, Set Variable)]) :*: (S1 ('MetaSel ('Just "_stdGen") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 StdGen) :*: S1 ('MetaSel ('Just "_theory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s)))))

type Rep1 Storage

Defined in Satyros.DPLL.Storage

type Rep1 Storage = D1 ('MetaData "Storage" "Satyros.DPLL.Storage" "satyros-0.3.1.4-3YwMxGnZD0k1OVgpDx5SHB" 'False) (C1 ('MetaCons "Storage" 'PrefixI 'True) ((S1 ('MetaSel ('Just "_unassignedVariables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Variable)) :*: (S1 ('MetaSel ('Just "_clauses") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vector Clause)) :*: S1 ('MetaSel ('Just "_assignment") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Assignment))) :*: (S1 ('MetaSel ('Just "_variableLevels") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Maybe Variable, Set Variable)]) :*: (S1 ('MetaSel ('Just "_stdGen") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 StdGen) :*: S1 ('MetaSel ('Just "_theory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))))

class HasAssignment s a | s -> a where

Methods

assignment :: Lens' s a

Instances

HasAssignment (Storage s) Assignment

Defined in Satyros.DPLL.Storage

Methods

assignment :: Lens' (Storage s) Assignment

class HasClauses s a | s -> a where

Methods

clauses :: Lens' s a

Instances

HasClauses (Storage s) (Vector Clause)

Defined in Satyros.DPLL.Storage

Methods

clauses :: Lens' (Storage s) (Vector Clause)

class HasStdGen s a | s -> a where

Methods

stdGen :: Lens' s a

Instances

HasStdGen (Storage s) StdGen

Defined in Satyros.DPLL.Storage

Methods

stdGen :: Lens' (Storage s) StdGen

class HasTheory s a | s -> a where

Methods

theory :: Lens' s a

Instances

HasTheory (Storage s) s

Defined in Satyros.DPLL.Storage

Methods

theory :: Lens' (Storage s) s

class HasUnassignedVariables s a | s -> a where

Methods

unassignedVariables :: Lens' s a

Instances

HasUnassignedVariables (Storage s) (Set Variable)

Defined in Satyros.DPLL.Storage

Methods

unassignedVariables :: Lens' (Storage s) (Set Variable)

class HasVariableLevels s a | s -> a where

Methods

variableLevels :: Lens' s a

Instances

HasVariableLevels (Storage s) [(Maybe Variable, Set Variable)]

Defined in Satyros.DPLL.Storage

Methods

variableLevels :: Lens' (Storage s) [(Maybe Variable, Set Variable)]

data StorageInitializationFailure

Constructors

EmptyClause

InitialConflict

initializeStorage :: Formula -> StdGen -> s -> Either StorageInitializationFailure (Storage s)