| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
SAT.Mios.Clause
Contents
Description
Clause, supporting pointer-based equality
- data Clause
- = Clause {
- learnt :: !Bool
- activity :: !DoubleSingleton
- protected :: !BoolSingleton
- 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?
Constructors
| Clause | |
Fields
| |
| NullClause | |
Instances
| 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 Clauses