Copyright | (c) Masahiro Sakai 2016 |
---|---|
License | BSD-style |
Maintainer | masahiro.sakai@gmail.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Deprecated: Use ToySolver.FileFormat.CNF instead
Synopsis
- data QDimacs = QDimacs {
- qdimacsNumVars :: !Int
- qdimacsNumClauses :: !Int
- qdimacsPrefix :: [QuantSet]
- qdimacsMatrix :: [PackedClause]
- data Quantifier
- type QuantSet = (Quantifier, [Atom])
- type Atom = Var
- type Lit = Int
- type Clause = [Lit]
- type PackedClause = Vector Lit
- packClause :: Clause -> PackedClause
- unpackClause :: PackedClause -> Clause
- parseFile :: (FileFormat a, MonadIO m) => FilePath -> m (Either String a)
- parseByteString :: ByteString -> Either String QDimacs
- writeFile :: (FileFormat a, MonadIO m) => FilePath -> a -> m ()
- hPutQDimacs :: Handle -> QDimacs -> IO ()
- qdimacsBuilder :: QDimacs -> Builder
Documentation
QDIMACS format
Quantified boolean expression in prenex normal form,
consisting of a sequence of quantifiers (qdimacsPrefix
) and
a quantifier-free CNF part (qdimacsMatrix
).
References:
- QDIMACS standard Ver. 1.1 http://www.qbflib.org/qdimacs.html
QDimacs | |
|
data Quantifier Source #
Quantifier
Instances
type QuantSet = (Quantifier, [Atom]) Source #
Quantified set of variables
Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).
type PackedClause = Vector Lit Source #
packClause :: Clause -> PackedClause Source #
unpackClause :: PackedClause -> Clause Source #
parseFile :: (FileFormat a, MonadIO m) => FilePath -> m (Either String a) Source #
Parse a file but returns an error message when parsing fails.
parseByteString :: ByteString -> Either String QDimacs Source #
Parse a QDimacs file but returns an error message when parsing fails.