SAT.Mios.ClauseManager

A shrinkable vector of Clause

higher level interface for ClauseVector

class ClauseManager a where

Resizable vector of Clause.

Minimal complete definition

newManager, getClauseVector

Methods

newManager :: Int -> IO a

getClauseVector :: a -> IO ClauseVector

Instances

ClauseManager ClauseExtManager

ClauseExtManager is a ClauseManager

Methods

newManager :: Int -> IO ClauseExtManager

getClauseVector :: ClauseExtManager -> IO ClauseVector

Manager with an extra Int (used as sort key or blocking literal)

data ClauseExtManager

Clause + Blocking Literal

Instances

ClauseManager ClauseExtManager

ClauseExtManager is a ClauseManager

Methods

newManager :: Int -> IO ClauseExtManager

getClauseVector :: ClauseExtManager -> IO ClauseVector

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 ClauseExtManager Int

ClauseExtManager is a SingleStorage on the numeber of clauses in it.

Methods

new' :: Int -> IO ClauseExtManager

get' :: ClauseExtManager -> IO Int

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

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

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]

pushClauseWithKey :: ClauseExtManager -> Clause -> Lit -> IO ()

O(1) inserter

getKeyVector :: ClauseExtManager -> IO (UVector Int)

returns the associated Int vector, which holds blocking literals.

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

sets the expire flag to a clause.

WatcherList

type WatcherList = Vector ClauseExtManager

Immutable Vector of ClauseExtManager

newWatcherList :: Int -> Int -> IO WatcherList

n is the number of Var, m is default size of each watcher list. | For n vars, we need [0 .. 2 + 2 * n - 1] slots, namely 2 * (n + 1)-length vector

getNthWatcher :: WatcherList -> Lit -> ClauseExtManager

returns the watcher List for Literal l.