Safe Haskell	Trustworthy
Language	Haskell2010

SAT.Mios.ClauseManager

Contents

higher level interface for ClauseVector
Simple Clause Manager
Manager with an extra Int (used as sort key or blocking literal)
WatcherList

Description

(This is a part of MIOS.) A shrinkable vector of Clause

Synopsis

class ClauseManager a where
data ClauseSimpleManager
data ClauseExtManager
pushClauseWithKey :: ClauseExtManager -> Clause -> Lit -> IO ()
getKeyVector :: ClauseExtManager -> IO (Vec Int)
markClause :: ClauseExtManager -> Clause -> IO ()
type WatcherList = Vector ClauseExtManager
newWatcherList :: Int -> Int -> IO WatcherList
getNthWatcher :: WatcherList -> Lit -> ClauseExtManager

higher level interface for ClauseVector

class ClauseManager a where Source #

Resizable vector of Clause.

Minimal complete definition

newManager, getClauseVector

Methods

newManager :: Int -> IO a Source #

getClauseVector :: a -> IO ClauseVector Source #

Instances

ClauseManager ClauseExtManager Source #	`ClauseExtManager` is a `ClauseManager`
Instance details Defined in SAT.Mios.ClauseManager Methods newManager :: Int -> IO ClauseExtManager Source # getClauseVector :: ClauseExtManager -> IO ClauseVector Source #
ClauseManager ClauseSimpleManager Source #	`ClauseSimpleManager` is a `ClauseManager`
Instance details Defined in SAT.Mios.ClauseManager Methods newManager :: Int -> IO ClauseSimpleManager Source # getClauseVector :: ClauseSimpleManager -> IO ClauseVector Source #

Simple Clause Manager

data ClauseSimpleManager Source #

Clause + Blocking Literal

Instances

ClauseManager ClauseSimpleManager Source #	`ClauseSimpleManager` is a `ClauseManager`
Instance details Defined in SAT.Mios.ClauseManager Methods newManager :: Int -> IO ClauseSimpleManager Source # getClauseVector :: ClauseSimpleManager -> IO ClauseVector Source #
StackFamily ClauseSimpleManager Clause Source #	`ClauseSimpleManager` is a `StackFamily` on clauses.
Instance details Defined in SAT.Mios.ClauseManager Methods newStack :: Int -> IO ClauseSimpleManager Source # pushTo :: ClauseSimpleManager -> Clause -> IO () Source # popFrom :: ClauseSimpleManager -> IO () Source # lastOf :: ClauseSimpleManager -> IO Clause Source # shrinkBy :: ClauseSimpleManager -> Int -> IO () Source #
SingleStorage ClauseSimpleManager Int Source #	`ClauseSimpleManager` is a `SingleStorage` on the number of clauses in it.
Instance details Defined in SAT.Mios.ClauseManager Methods new' :: Int -> IO ClauseSimpleManager Source # get' :: ClauseSimpleManager -> IO Int Source # set' :: ClauseSimpleManager -> Int -> IO () Source # modify' :: ClauseSimpleManager -> (Int -> Int) -> IO () Source #

Manager with an extra Int (used as sort key or blocking literal)

data ClauseExtManager Source #

Clause + Blocking Literal

Instances

ClauseManager ClauseExtManager Source #	`ClauseExtManager` is a `ClauseManager`
Instance details Defined in SAT.Mios.ClauseManager Methods newManager :: Int -> IO ClauseExtManager Source # getClauseVector :: ClauseExtManager -> IO ClauseVector Source #
StackFamily ClauseExtManager Clause Source #	`ClauseExtManager` is a `StackFamily` on clauses.
Instance details Defined in SAT.Mios.ClauseManager Methods newStack :: Int -> IO ClauseExtManager Source # pushTo :: ClauseExtManager -> Clause -> IO () Source # popFrom :: ClauseExtManager -> IO () Source # lastOf :: ClauseExtManager -> IO Clause Source # shrinkBy :: ClauseExtManager -> Int -> IO () Source #
SingleStorage ClauseExtManager Int Source #	`ClauseExtManager` is a `SingleStorage` on the number of clauses in it.
Instance details Defined in SAT.Mios.ClauseManager Methods new' :: Int -> IO ClauseExtManager Source # get' :: ClauseExtManager -> IO Int Source # set' :: ClauseExtManager -> Int -> IO () Source # modify' :: ClauseExtManager -> (Int -> Int) -> IO () Source #
VecFamily WatcherList Clause Source #	`WatcherList` is an `Lit`-indexed collection of `Clause`.
Instance details Defined in SAT.Mios.ClauseManager Methods getNth :: WatcherList -> Int -> IO Clause Source # setNth :: WatcherList -> Int -> Clause -> IO () Source # reset :: WatcherList -> IO () Source # swapBetween :: WatcherList -> Int -> Int -> IO () Source # modifyNth :: WatcherList -> (Clause -> Clause) -> Int -> IO () Source # newVec :: Int -> Clause -> IO WatcherList Source # setAll :: WatcherList -> Clause -> IO () Source # growBy :: WatcherList -> Int -> IO WatcherList Source # asList :: WatcherList -> IO [Clause] Source #
VecFamily ClauseExtManager Clause Source #	`ClauseExtManager` is a collection of `Clause`
Instance details Defined in SAT.Mios.ClauseManager Methods getNth :: ClauseExtManager -> Int -> IO Clause Source # setNth :: ClauseExtManager -> Int -> Clause -> IO () Source # reset :: ClauseExtManager -> IO () Source # swapBetween :: ClauseExtManager -> Int -> Int -> IO () Source # modifyNth :: ClauseExtManager -> (Clause -> Clause) -> Int -> IO () Source # newVec :: Int -> Clause -> IO ClauseExtManager Source # setAll :: ClauseExtManager -> Clause -> IO () Source # growBy :: ClauseExtManager -> Int -> IO ClauseExtManager Source # asList :: ClauseExtManager -> IO [Clause] Source #

pushClauseWithKey :: ClauseExtManager -> Clause -> Lit -> IO () Source #

O(1) inserter

getKeyVector :: ClauseExtManager -> IO (Vec Int) Source #

returns the associated Int vector, which holds blocking literals.

markClause :: ClauseExtManager -> Clause -> IO () Source #

sets the expire flag to a clause.

WatcherList

type WatcherList = Vector ClauseExtManager Source #

Immutable Vector of ClauseExtManager

newWatcherList :: Int -> Int -> IO WatcherList Source #

n is the number of Var, m is default size of each watcher list. | For n vars, we need [0 .. 2 + 2 * n - 1] slots, namely 2 * (n + 1)-length vector FIXME: sometimes n > 1M

getNthWatcher :: WatcherList -> Lit -> ClauseExtManager Source #

returns the watcher List for Literal l.