mios-1.6.2: A Minisat-based CDCL SAT solver in Haskell

Safe HaskellTrustworthy
LanguageHaskell2010

SAT.Mios.ClausePool

Description

(This is a part of MIOS.) Recycling clauses

Synopsis

Documentation

type ClausePool = Vector ClauseSimpleManager Source #

an immutable Vector of ClauseSimpleManager

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.