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 |
- 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
- class QDIMACS t where
- class WDIMACS t where
- 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 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
.
dimacsComments :: t -> [ByteString] Source #
dimacsNumVariables :: t -> Int Source #
dimacsClauses :: t -> Seq IntSet Source #
class QDIMACS t where Source #
QDIMACS file format pretty printer
This is used to generate the problem statement for a given QSAT
Solver
.
qdimacsComments :: t -> [ByteString] Source #
qdimacsNumVariables :: t -> Int Source #
qdimacsQuantified :: t -> [Quant] Source #
qdimacsClauses :: t -> Seq IntSet Source #
class WDIMACS t where Source #
WDIMACS file format pretty printer
This is used to generate the problem statement for a given MaxSAT
Solver
(TODO).
wdimacsComments :: t -> [ByteString] Source #
wdimacsNumVariables :: t -> Int Source #
:: t | |
-> Int64 | Specified to be 1 ≤ n < 2^63 |