Safe Haskell | None |
---|---|
Language | Haskell2010 |
PureSAT
Contents
Synopsis
- data Solver s
- newSolver :: ST s (Solver s)
- newtype Lit = MkLit Int
- newLit :: Solver s -> ST s Lit
- boostScore :: Solver s -> Lit -> ST s ()
- neg :: Lit -> Lit
- addClause :: Solver s -> [Lit] -> ST s Bool
- solve :: Solver s -> ST s Bool
- simplify :: Solver s -> ST s Bool
- modelValue :: Solver s -> Lit -> ST s Bool
- num_vars :: Solver s -> ST s Int
- num_clauses :: Solver s -> ST s Int
- num_learnts :: Solver s -> ST s Int
- num_learnt_literals :: Solver s -> ST s Int
- num_conflicts :: Solver s -> ST s Int
- num_restarts :: Solver s -> ST s Int
Documentation
Literals
Constructors
MkLit Int |
Instances
Show Lit | |
Eq Lit | |
Ord Lit | |
Prim Lit | |
Defined in PureSAT.LitVar Methods sizeOfType# :: Proxy Lit -> Int# alignmentOfType# :: Proxy Lit -> Int# alignment# :: Lit -> Int# indexByteArray# :: ByteArray# -> Int# -> Lit readByteArray# :: MutableByteArray# s -> Int# -> State# s -> (# State# s, Lit #) writeByteArray# :: MutableByteArray# s -> Int# -> Lit -> State# s -> State# s setByteArray# :: MutableByteArray# s -> Int# -> Int# -> Lit -> State# s -> State# s indexOffAddr# :: Addr# -> Int# -> Lit readOffAddr# :: Addr# -> Int# -> State# s -> (# State# s, Lit #) writeOffAddr# :: Addr# -> Int# -> Lit -> State# s -> State# s setOffAddr# :: Addr# -> Int# -> Int# -> Lit -> State# s -> State# s |
Statistics
num_clauses :: Solver s -> ST s Int Source #
num_learnts :: Solver s -> ST s Int Source #
num_learnt_literals :: Solver s -> ST s Int Source #
num_conflicts :: Solver s -> ST s Int Source #
num_restarts :: Solver s -> ST s Int Source #