SAT.Mios.Vec

(This is a part of MIOS.) Abstraction Layer for Mutable Vectors

Vector class and type

class VecFamily v a | v -> a where

The interface on vectors.

Minimal complete definition

getNth, setNth

Methods

getNth :: v -> Int -> IO a

returns the n-th value.

setNth :: v -> Int -> a -> IO ()

sets the n-th value.

reset :: v -> IO ()

erases all elements in it.

swapBetween :: v -> Int -> Int -> IO ()

returns the n-th value (index starts from zero in any case). | swaps two elements.

modifyNth :: v -> (a -> a) -> Int -> IO ()

calls the update function.

newVec :: Int -> a -> IO v

returns a new vector.

setAll :: v -> a -> IO ()

sets all elements.

growBy :: v -> Int -> IO v

extends the size of stack by n; note: values in new elements aren't initialized maybe.

asList :: v -> IO [a]

converts to a list.

Instances

VecFamily ClauseVector Clause

ClauseVector is a vector of Clause.

Defined in SAT.Mios.Clause

Methods

getNth :: ClauseVector -> Int -> IO Clause

setNth :: ClauseVector -> Int -> Clause -> IO ()

reset :: ClauseVector -> IO ()

swapBetween :: ClauseVector -> Int -> Int -> IO ()

modifyNth :: ClauseVector -> (Clause -> Clause) -> Int -> IO ()

newVec :: Int -> Clause -> IO ClauseVector

setAll :: ClauseVector -> Clause -> IO ()

growBy :: ClauseVector -> Int -> IO ClauseVector

asList :: ClauseVector -> IO [Clause]

VecFamily Clause Lit

Clause is a VecFamily of Lit.

Defined in SAT.Mios.Clause

Methods

getNth :: Clause -> Int -> IO Lit

setNth :: Clause -> Int -> Lit -> IO ()

reset :: Clause -> IO ()

swapBetween :: Clause -> Int -> Int -> IO ()

modifyNth :: Clause -> (Lit -> Lit) -> Int -> IO ()

newVec :: Int -> Lit -> IO Clause

setAll :: Clause -> Lit -> IO ()

growBy :: Clause -> Int -> IO Clause

asList :: Clause -> IO [Lit]

VecFamily WatcherList Clause

WatcherList is an Lit-indexed collection of Clause.

Defined in SAT.Mios.ClauseManager

Methods

getNth :: WatcherList -> Int -> IO Clause

setNth :: WatcherList -> Int -> Clause -> IO ()

reset :: WatcherList -> IO ()

swapBetween :: WatcherList -> Int -> Int -> IO ()

modifyNth :: WatcherList -> (Clause -> Clause) -> Int -> IO ()

newVec :: Int -> Clause -> IO WatcherList

setAll :: WatcherList -> Clause -> IO ()

growBy :: WatcherList -> Int -> IO WatcherList

asList :: WatcherList -> IO [Clause]

VecFamily ClauseExtManager Clause

ClauseExtManager is a collection of Clause

Defined in SAT.Mios.ClauseManager

Methods

getNth :: ClauseExtManager -> Int -> IO Clause

setNth :: ClauseExtManager -> Int -> Clause -> IO ()

reset :: ClauseExtManager -> IO ()

swapBetween :: ClauseExtManager -> Int -> Int -> IO ()

modifyNth :: ClauseExtManager -> (Clause -> Clause) -> Int -> IO ()

newVec :: Int -> Clause -> IO ClauseExtManager

setAll :: ClauseExtManager -> Clause -> IO ()

growBy :: ClauseExtManager -> Int -> IO ClauseExtManager

asList :: ClauseExtManager -> IO [Clause]

data family Vec a

Another abstraction layer on Vector which reserves zero element for internal use. Note: If you want to use the 0-th element, use UVector Int.

Instances

data Vec Double

Defined in SAT.Mios.Vec

data Vec Double = ByteArrayDouble (MutableByteArray RealWorld)

data Vec Int

Defined in SAT.Mios.Vec

data Vec Int = ByteArrayInt (MutableByteArray RealWorld)

SingleStorage

class SingleStorage s t | s -> t where

Interface for single (one-length vector) mutable data

Minimal complete definition

get', set'

Methods

new' :: t -> IO s

allocates and returns an new data.

get' :: s -> IO t

gets the value.

set' :: s -> t -> IO ()

sets the value.

modify' :: s -> (t -> t) -> IO ()

calls an update function on it.

Instances

SingleStorage Bool' Bool

Defined in SAT.Mios.Vec

Methods

new' :: Bool -> IO Bool'

get' :: Bool' -> IO Bool

set' :: Bool' -> Bool -> IO ()

modify' :: Bool' -> (Bool -> Bool) -> IO ()

SingleStorage Clause Int

Clause is a SingleStorage on the number of literals in it.

Defined in SAT.Mios.Clause

Methods

new' :: Int -> IO Clause

get' :: Clause -> IO Int

set' :: Clause -> Int -> IO ()

modify' :: Clause -> (Int -> Int) -> IO ()

SingleStorage ClauseExtManager Int

ClauseExtManager is a SingleStorage on the number of clauses in it.

Defined in SAT.Mios.ClauseManager

Methods

new' :: Int -> IO ClauseExtManager

get' :: ClauseExtManager -> IO Int

set' :: ClauseExtManager -> Int -> IO ()

modify' :: ClauseExtManager -> (Int -> Int) -> IO ()

SingleStorage ClauseSimpleManager Int

ClauseSimpleManager is a SingleStorage on the number of clauses in it.

Defined in SAT.Mios.ClauseManager

Methods

new' :: Int -> IO ClauseSimpleManager

get' :: ClauseSimpleManager -> IO Int

set' :: ClauseSimpleManager -> Int -> IO ()

modify' :: ClauseSimpleManager -> (Int -> Int) -> IO ()

type Bool' = IOVector Bool

Mutable Bool

type Double' = ByteArrayDouble

Mutable Double

type Int' = ByteArrayInt

Mutable Int Note: Int' is identical to Stack

Stack

class SingleStorage s Int => StackFamily s t | s -> t where

Interface on stacks

Methods

newStack :: Int -> IO s

returns a new stack.

pushTo :: s -> t -> IO ()

pushs an value to the tail of the stack.

popFrom :: s -> IO ()

pops the last element.

lastOf :: s -> IO t

peeks the last element.

shrinkBy :: s -> Int -> IO ()

shrinks the stack.

Instances

StackFamily Clause Lit

Clause is a Stackfamilyon literals since literals in it will be discared if satisifed at level = 0.

Defined in SAT.Mios.Clause

Methods

newStack :: Int -> IO Clause

pushTo :: Clause -> Lit -> IO ()

popFrom :: Clause -> IO ()

lastOf :: Clause -> IO Lit

shrinkBy :: Clause -> Int -> IO ()

StackFamily ClauseExtManager Clause

ClauseExtManager is a StackFamily on clauses.

Defined in SAT.Mios.ClauseManager

Methods

newStack :: Int -> IO ClauseExtManager

pushTo :: ClauseExtManager -> Clause -> IO ()

popFrom :: ClauseExtManager -> IO ()

lastOf :: ClauseExtManager -> IO Clause

shrinkBy :: ClauseExtManager -> Int -> IO ()

StackFamily ClauseSimpleManager Clause

ClauseSimpleManager is a StackFamily on clauses.

Defined in SAT.Mios.ClauseManager

Methods

newStack :: Int -> IO ClauseSimpleManager

pushTo :: ClauseSimpleManager -> Clause -> IO ()

popFrom :: ClauseSimpleManager -> IO ()

lastOf :: ClauseSimpleManager -> IO Clause

shrinkBy :: ClauseSimpleManager -> Int -> IO ()

type Stack = Vec Int

Stack of Int, an alias of Vec Int

newStackFromList :: [Int] -> IO Stack

returns a new Stack from [Int].

realLength :: Vec Int -> Int

returns the number of allocated slots

sortStack :: Stack -> IO ()

sort the content of a stack, in small-to-large order.