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

PureSAT.Main

Contents

Synopsis

Documentation

data Solver s Source #

Solver

newSolver :: ST s (Solver s) Source #

Create new solver

newtype Lit Source #

Literals

Constructors

MkLit Int 

Instances

Instances details
Show Lit Source # 
Instance details

Defined in PureSAT.LitVar

Methods

showsPrec :: Int -> Lit -> ShowS

show :: Lit -> String

showList :: [Lit] -> ShowS

Eq Lit Source # 
Instance details

Defined in PureSAT.LitVar

Methods

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

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

Ord Lit Source # 
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 Source # 
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 Source #

Create fresh literal

boostScore :: Solver s -> Lit -> ST s () Source #

neg :: Lit -> Lit Source #

Negate literal

addClause :: Solver s -> [Lit] -> ST s Bool Source #

solve :: Solver s -> ST s Bool Source #

simplify :: Solver s -> ST s Bool Source #

Simplify solver

modelValue :: Solver s -> Lit -> ST s Bool Source #

Lookup model value

Statistics

num_vars :: Solver s -> ST s Int Source #

num_clauses :: Solver s -> ST s Int Source #

num_learnts :: Solver s -> ST s Int Source #

num_restarts :: Solver s -> ST s Int Source #