SAT.Solver.Mios.ClauseManager

A shrinkable VectorFamily of Clause

higher level interface for ClauseVector

class ClauseManager a where

resizable clause vector

Minimal complete definition

newManager, numberOfClauses, clearManager, shrinkManager, getClauseVector, pushClause

Methods

newManager :: Int -> IO a

numberOfClauses :: a -> IO Int

clearManager :: a -> IO ()

shrinkManager :: a -> Int -> IO ()

getClauseVector :: a -> IO ClauseVector

pushClause :: a -> Clause -> IO ()

Instances

ClauseManager ClauseExtManager

Methods

newManager :: Int -> IO ClauseExtManager

numberOfClauses :: ClauseExtManager -> IO Int

clearManager :: ClauseExtManager -> IO ()

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

getClauseVector :: ClauseExtManager -> IO ClauseVector

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

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

data ClauseExtManager

Clause + Blocking Literal

Instances

ClauseManager ClauseExtManager

Methods

newManager :: Int -> IO ClauseExtManager

numberOfClauses :: ClauseExtManager -> IO Int

clearManager :: ClauseExtManager -> IO ()

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

getClauseVector :: ClauseExtManager -> IO ClauseVector

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

VectorFamily WatcherList Clause

Methods

clear :: WatcherList -> IO ()

dump :: String -> WatcherList -> IO String

asVec :: WatcherList -> IOVector Int

asList :: WatcherList -> IO [Clause]

VectorFamily ClauseExtManager Clause

Methods

clear :: ClauseExtManager -> IO ()

dump :: String -> ClauseExtManager -> IO String

asVec :: ClauseExtManager -> IOVector Int

asList :: ClauseExtManager -> IO [Clause]

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

O(1) inserter

getKeyVector :: ClauseExtManager -> IO Vec

returns the associated Int vector

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

sets the expire flag to a clause

WatcherList

type WatcherList = Vector ClauseExtManager

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 :: ClauseManager for Literal l

garbageCollect :: WatcherList -> IO ()

purges all expirable clauses in WatcherList