Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
Clause, a data supporting pointer-based equality
- data Clause
- = Clause {
- learnt :: !Bool
- activity :: !DoubleSingleton
- protected :: !BoolSingleton
- lbd :: !IntSingleton
- lits :: !Vec
- | NullClause
- = Clause {
- shrinkClause :: Int -> Clause -> IO ()
- newClauseFromVec :: Bool -> Vec -> IO Clause
- sizeOfClause :: Clause -> IO Int
- type ClauseVector = IOVector Clause
- newClauseVector :: Int -> IO ClauseVector
- getNthClause :: ClauseVector -> Int -> IO Clause
- setNthClause :: ClauseVector -> Int -> Clause -> IO ()
- swapClauses :: ClauseVector -> Int -> Int -> IO ()
Documentation
Fig. 7.(p.11)
clause, null, binary clause.
This matches both of Clause
and GClause
in MiniSat
TODO: GADTs is better?
Clause | |
| |
NullClause |
Eq Clause Source # | The equality on |
Show Clause Source # | |
VectorFamily ClauseVector Clause Source # | |
VectorFamily Clause Lit Source # | supports a restricted set of |
VectorFamily WatcherList Clause Source # | |
VectorFamily ClauseExtManager Clause Source # | |
shrinkClause :: Int -> Clause -> IO () Source #
drop the last N literals in a Clause
to eliminate unsatisfied literals
newClauseFromVec :: Bool -> Vec -> IO Clause Source #
copies vec and return a new Clause
Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.
sizeOfClause :: Clause -> IO Int Source #
returns the number of literals in a clause, even if the given clause is a binary clause
Vector of Clause
newClauseVector :: Int -> IO ClauseVector Source #
returns a new ClauseVector
getNthClause :: ClauseVector -> Int -> IO Clause Source #
returns the nth Clause
setNthClause :: ClauseVector -> Int -> Clause -> IO () Source #
sets the nth Clause
swapClauses :: ClauseVector -> Int -> Int -> IO () Source #
swaps the two Clause
s