puresat-0.1: Pure Haskell SAT-solver
Safe HaskellNone
LanguageHaskell2010

PureSAT

Contents

Synopsis

Documentation

data Solver s #

newSolver :: ST s (Solver s) #

newtype Lit #

Constructors

MkLit Int 

Instances

Instances details
Show Lit 
Instance details

Defined in PureSAT.LitVar

Methods

showsPrec :: Int -> Lit -> ShowS

show :: Lit -> String

showList :: [Lit] -> ShowS

Eq Lit 
Instance details

Defined in PureSAT.LitVar

Methods

(==) :: Lit -> Lit -> Bool

(/=) :: Lit -> Lit -> Bool

Ord Lit 
Instance details

Defined in PureSAT.LitVar

Methods

compare :: Lit -> Lit -> Ordering

(<) :: Lit -> Lit -> Bool

(<=) :: Lit -> Lit -> Bool

(>) :: Lit -> Lit -> Bool

(>=) :: Lit -> Lit -> Bool

max :: Lit -> Lit -> Lit

min :: Lit -> Lit -> Lit

Prim Lit 
Instance details

Defined in PureSAT.LitVar

Methods

sizeOfType# :: Proxy Lit -> Int#

sizeOf# :: 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

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 #

Statistics

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 #