Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
(This is a part of MIOS.) Clause, supporting pointer-based equality
- data Clause
- newClauseFromStack :: Bool -> Stack -> IO Clause
- type ClauseVector = IOVector Clause
- newClauseVector :: Int -> IO ClauseVector
Documentation
Fig. 7.(p.11)
normal, null (and binary) clause.
This matches both of Clause
and GClause
in MiniSat.
Eq Clause Source # | The equality on |
Show Clause Source # | |
StackFamily Clause Lit Source # |
|
StackFamily ClauseExtManager Clause Source # |
|
StackFamily ClauseSimpleManager Clause Source # |
|
SingleStorage Clause Int Source # |
|
VecFamily ClauseVector Clause Source # |
|
VecFamily Clause Lit Source # | |
VecFamily WatcherList Clause Source # |
|
VecFamily ClauseExtManager Clause Source # |
|
newClauseFromStack :: Bool -> Stack -> IO Clause Source #
copies vec and return a new Clause
.
Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.
Vector of Clause
newClauseVector :: Int -> IO ClauseVector Source #
returns a new ClauseVector
.