| Copyright | © Edward Kmett 2010-2014, Johan Kiviniemi 2013 |
|---|---|
| License | BSD3 |
| Maintainer | Edward Kmett <ekmett@gmail.com> |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Ersatz.Problem
Contents
Description
- data SAT = SAT !Int !Formula !(HashMap (StableName ()) Literal)
- class HasSAT s 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
Minimal complete definition
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 Literal Source
assertFormula :: (MonadState s m, HasSAT s) => Formula -> m () Source
generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal Source
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 -> ByteString Source
literalForall :: (MonadState s m, HasQSAT s) => m Literal Source
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 -> Int Source
dimacsClauses :: t -> Set IntSet Source
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 -> Int Source
qdimacsQuantified :: t -> [Quant] Source
qdimacsClauses :: t -> Set IntSet Source
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 -> Int Source
Arguments
| :: t | |
| -> Int64 | Specified to be 1 ≤ n < 2^63 |
wdimacsClauses :: t -> Set (Int64, IntSet) Source