SAT.Mios.Clause

Clause, supporting pointer-based equality

Documentation

data Clause

Fig. 7.(p.11) normal, null (and binary) clause. This matches both of Clause and GClause in MiniSat.

Constructors

Clause

Fields

• learnt :: !Bool

  whether this is a learnt clause , rank :: !Int' -- ^ goodness like LBD; computed in Ranking

• activity :: !Double'

  activity of this clause

• protected :: !Bool'

  protected from reduce

• lits :: !Stack

  which this clause consists of

NullClause

Instances

Eq Clause

The equality on Clause is defined with reallyUnsafePtrEquality.

Methods

(==) :: Clause -> Clause -> Bool

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

Show Clause

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

StackFamily Clause Lit

Clause is a Stackfamilyon literals since literals in it will be discared if satisifed at level = 0.

Methods

newStack :: Int -> IO Clause

pushTo :: Clause -> Lit -> IO ()

popFrom :: Clause -> IO ()

lastOf :: Clause -> IO Lit

shrinkBy :: Clause -> Int -> IO ()

StackFamily ClauseExtManager Clause

ClauseExtManager is a StackFamily on clauses.

Methods

newStack :: Int -> IO ClauseExtManager

pushTo :: ClauseExtManager -> Clause -> IO ()

popFrom :: ClauseExtManager -> IO ()

lastOf :: ClauseExtManager -> IO Clause

shrinkBy :: ClauseExtManager -> Int -> IO ()

SingleStorage Clause Int

Clause is a SingleStorage on the number of literals in it.

Methods

new' :: Int -> IO Clause

get' :: Clause -> IO Int

set' :: Clause -> Int -> IO ()

modify' :: Clause -> (Int -> Int) -> IO ()

VecFamily ClauseVector Clause

ClauseVector is a vector of Clause.

Methods

getNth :: ClauseVector -> Int -> IO Clause

setNth :: ClauseVector -> Int -> Clause -> IO ()

reset :: ClauseVector -> IO ()

asUVector :: ClauseVector -> UVector Int

swapBetween :: ClauseVector -> Int -> Int -> IO ()

modifyNth :: ClauseVector -> (Clause -> Clause) -> Int -> IO ()

newVec :: Int -> Clause -> IO ClauseVector

setAll :: ClauseVector -> Clause -> IO ()

growBy :: ClauseVector -> Int -> IO ClauseVector

asList :: ClauseVector -> IO [Clause]

VecFamily Clause Lit

Clause is a VecFamily of Lit.

Methods

getNth :: Clause -> Int -> IO Lit

setNth :: Clause -> Int -> Lit -> IO ()

reset :: Clause -> IO ()

asUVector :: Clause -> UVector Int

swapBetween :: Clause -> Int -> Int -> IO ()

modifyNth :: Clause -> (Lit -> Lit) -> Int -> IO ()

newVec :: Int -> Lit -> IO Clause

setAll :: Clause -> Lit -> IO ()

growBy :: Clause -> Int -> IO Clause

asList :: Clause -> IO [Lit]

VecFamily WatcherList Clause

WatcherList is an Lit-indexed collection of Clause.

Methods

getNth :: WatcherList -> Int -> IO Clause

setNth :: WatcherList -> Int -> Clause -> IO ()

reset :: WatcherList -> IO ()

asUVector :: WatcherList -> UVector Int

swapBetween :: WatcherList -> Int -> Int -> IO ()

modifyNth :: WatcherList -> (Clause -> Clause) -> Int -> IO ()

newVec :: Int -> Clause -> IO WatcherList

setAll :: WatcherList -> Clause -> IO ()

growBy :: WatcherList -> Int -> IO WatcherList

asList :: WatcherList -> IO [Clause]

VecFamily ClauseExtManager Clause

ClauseExtManager is a collection of Clause

Methods

getNth :: ClauseExtManager -> Int -> IO Clause

setNth :: ClauseExtManager -> Int -> Clause -> IO ()

reset :: ClauseExtManager -> IO ()

asUVector :: ClauseExtManager -> UVector Int

swapBetween :: ClauseExtManager -> Int -> Int -> IO ()

modifyNth :: ClauseExtManager -> (Clause -> Clause) -> Int -> IO ()

newVec :: Int -> Clause -> IO ClauseExtManager

setAll :: ClauseExtManager -> Clause -> IO ()

growBy :: ClauseExtManager -> Int -> IO ClauseExtManager

asList :: ClauseExtManager -> IO [Clause]

newClauseFromStack :: Bool -> Stack -> IO Clause

copies vec and return a new Clause. Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.

Vector of Clause

type ClauseVector = IOVector Clause

Mutable Clause Vector

newClauseVector :: Int -> IO ClauseVector

returns a new ClauseVector.