Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
A shrinkable vector of Clause
- class ClauseManager a where
- data ClauseExtManager
- pushClauseWithKey :: ClauseExtManager -> Clause -> Lit -> IO ()
- getKeyVector :: ClauseExtManager -> IO (UVector 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
.
newManager :: Int -> IO a Source #
getClauseVector :: a -> IO ClauseVector Source #
Manager with an extra Int (used as sort key or blocking literal)
data ClauseExtManager Source #
Clause + Blocking Literal
ClauseManager ClauseExtManager Source # | |
StackFamily ClauseExtManager Clause Source # |
|
SingleStorage ClauseExtManager Int Source # |
|
VecFamily WatcherList Clause Source # |
|
VecFamily ClauseExtManager Clause Source # |
|
pushClauseWithKey :: ClauseExtManager -> Clause -> Lit -> IO () Source #
O(1) inserter
getKeyVector :: ClauseExtManager -> IO (UVector 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
getNthWatcher :: WatcherList -> Lit -> ClauseExtManager Source #
returns the watcher List for Literal l.