Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
(This is a part of MIOS.) Recycling clauses
Synopsis
- type ClausePool = Vector ClauseSimpleManager
- newClausePool :: Int -> IO ClausePool
- makeClauseFromStack :: ClausePool -> Stack -> IO Clause
- putBackToPool :: ClausePool -> Clause -> IO ()
Documentation
type ClausePool = Vector ClauseSimpleManager Source #
an immutable Vector of ClauseSimpleManager
newClausePool :: Int -> IO ClausePool Source #
returns a new ClausePool
makeClauseFromStack :: ClausePool -> Stack -> IO Clause Source #
If a nice candidate as a learnt is stored, return it. Otherwise allocate a new clause in heap then return it.
putBackToPool :: ClausePool -> Clause -> IO () Source #
Note: only not-too-large and learnt clauses are recycled.