| Portability | non-portable |
|---|---|
| Stability | experimental |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Safe Haskell | None |
Ersatz.Problem
Contents
Description
- data SAT = SAT !Int !Formula !(HashMap (StableName ()) Literal)
- class HasSAT t where
- runSAT :: StateT SAT m a -> m (a, SAT)
- runSAT' :: StateT SAT Identity a -> (a, SAT)
- dimacsSAT :: StateT SAT Identity a -> ByteString
- literalExists :: (MonadState s m, HasSAT s) => m Literal
- assertFormula :: (MonadState s m, HasSAT s) => Formula -> m ()
- generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal
- data QSAT = QSAT !IntSet SAT
- class HasSAT t => HasQSAT t where
- runQSAT :: StateT QSAT m a -> m (a, QSAT)
- runQSAT' :: StateT QSAT Identity a -> (a, QSAT)
- qdimacsQSAT :: StateT QSAT Identity a -> ByteString
- literalForall :: (MonadState s m, HasQSAT s) => m Literal
- class DIMACS t where
- dimacsComments :: t -> [ByteString]
- dimacsNumVariables :: t -> Int
- dimacsClauses :: t -> Set IntSet
- class QDIMACS t where
- qdimacsComments :: t -> [ByteString]
- qdimacsNumVariables :: t -> Int
- qdimacsQuantified :: t -> [Quant]
- qdimacsClauses :: t -> Set IntSet
- class WDIMACS t where
- wdimacsComments :: t -> [ByteString]
- wdimacsNumVariables :: t -> Int
- wdimacsTopWeight :: t -> Int64
- wdimacsClauses :: t -> Set (Int64, IntSet)
- dimacs :: DIMACS t => t -> Builder
- qdimacs :: QDIMACS t => t -> Builder
- wdimacs :: WDIMACS t => t -> Builder
SAT
runSAT :: StateT SAT m a -> m (a, SAT)Source
Run a SAT-generating state computation. Useful e.g. in ghci for
disambiguating the type of a MonadState, HasSAT value.
runSAT' :: StateT SAT Identity a -> (a, SAT)Source
Run a SAT-generating state computation in the Identity monad. Useful
e.g. in ghci for disambiguating the type of a MonadState, HasSAT value.
literalExists :: (MonadState s m, HasSAT s) => m LiteralSource
assertFormula :: (MonadState s m, HasSAT s) => Formula -> m ()Source
generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m LiteralSource
QSAT
A (quantified) boolean formula.
runQSAT :: StateT QSAT m a -> m (a, QSAT)Source
Run a QSAT-generating state computation. Useful e.g. in ghci for
disambiguating the type of a MonadState, HasQSAT value.
runQSAT' :: StateT QSAT Identity a -> (a, QSAT)Source
Run a QSAT-generating state computation in the Identity monad. Useful
e.g. in ghci for disambiguating the type of a MonadState, HasQSAT value.
qdimacsQSAT :: StateT QSAT Identity a -> ByteStringSource
literalForall :: (MonadState s m, HasQSAT s) => m LiteralSource
DIMACS pretty printing
DIMACS file format pretty printer
This is used to generate the problem statement for a given SAT Solver.
Methods
dimacsComments :: t -> [ByteString]Source
dimacsNumVariables :: t -> IntSource
dimacsClauses :: t -> Set IntSetSource
QDIMACS file format pretty printer
This is used to generate the problem statement for a given QSAT Solver.
Methods
qdimacsComments :: t -> [ByteString]Source
qdimacsNumVariables :: t -> IntSource
qdimacsQuantified :: t -> [Quant]Source
qdimacsClauses :: t -> Set IntSetSource
WDIMACS file format pretty printer
This is used to generate the problem statement for a given MaxSAT Solver (TODO).
Methods
wdimacsComments :: t -> [ByteString]Source
wdimacsNumVariables :: t -> IntSource
Arguments
| :: t | |
| -> Int64 | Specified to be 1 ≤ n < 2^63 |
wdimacsClauses :: t -> Set (Int64, IntSet)Source