ToySolver.Text.QDimacs

Deprecated: Use ToySolver.FileFormat.CNF instead

Documentation

data QDimacs

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

Constructors

QDimacs

Fields

• qdimacsNumVars :: !Int

  Number of variables

• qdimacsNumClauses :: !Int

  Number of clauses

• qdimacsPrefix :: [QuantSet]

  Sequence of quantifiers

• qdimacsMatrix :: [PackedClause]

  Clauses

Instances

Eq QDimacs

Defined in ToySolver.FileFormat.CNF

Methods

(==) :: QDimacs -> QDimacs -> Bool

(/=) :: QDimacs -> QDimacs -> Bool

Ord QDimacs

Defined in ToySolver.FileFormat.CNF

Methods

compare :: QDimacs -> QDimacs -> Ordering

(<) :: QDimacs -> QDimacs -> Bool

(<=) :: QDimacs -> QDimacs -> Bool

(>) :: QDimacs -> QDimacs -> Bool

(>=) :: QDimacs -> QDimacs -> Bool

max :: QDimacs -> QDimacs -> QDimacs

min :: QDimacs -> QDimacs -> QDimacs

Read QDimacs

Defined in ToySolver.FileFormat.CNF

Methods

readsPrec :: Int -> ReadS QDimacs

readList :: ReadS [QDimacs]

readPrec :: ReadPrec QDimacs

readListPrec :: ReadPrec [QDimacs]

Show QDimacs

Defined in ToySolver.FileFormat.CNF

Methods

showsPrec :: Int -> QDimacs -> ShowS

show :: QDimacs -> String

showList :: [QDimacs] -> ShowS

FileFormat QDimacs

Defined in ToySolver.FileFormat.CNF

Methods

parse :: ByteString -> Either String QDimacs

render :: QDimacs -> Builder

data Quantifier

Quantifier

Constructors

E

existential quantifier (∃)

A

universal quantifier (∀)

Instances

Bounded Quantifier

Defined in ToySolver.FileFormat.CNF

Methods

minBound :: Quantifier

maxBound :: Quantifier

Enum Quantifier

Defined in ToySolver.FileFormat.CNF

Methods

succ :: Quantifier -> Quantifier

pred :: Quantifier -> Quantifier

toEnum :: Int -> Quantifier

fromEnum :: Quantifier -> Int

enumFrom :: Quantifier -> [Quantifier]

enumFromThen :: Quantifier -> Quantifier -> [Quantifier]

enumFromTo :: Quantifier -> Quantifier -> [Quantifier]

enumFromThenTo :: Quantifier -> Quantifier -> Quantifier -> [Quantifier]

Eq Quantifier

Defined in ToySolver.FileFormat.CNF

Methods

(==) :: Quantifier -> Quantifier -> Bool

(/=) :: Quantifier -> Quantifier -> Bool

Ord Quantifier

Defined in ToySolver.FileFormat.CNF

Methods

compare :: Quantifier -> Quantifier -> Ordering

(<) :: Quantifier -> Quantifier -> Bool

(<=) :: Quantifier -> Quantifier -> Bool

(>) :: Quantifier -> Quantifier -> Bool

(>=) :: Quantifier -> Quantifier -> Bool

max :: Quantifier -> Quantifier -> Quantifier

min :: Quantifier -> Quantifier -> Quantifier

Read Quantifier

Defined in ToySolver.FileFormat.CNF

Methods

readsPrec :: Int -> ReadS Quantifier

readList :: ReadS [Quantifier]

readPrec :: ReadPrec Quantifier

readListPrec :: ReadPrec [Quantifier]

Show Quantifier

Defined in ToySolver.FileFormat.CNF

Methods

showsPrec :: Int -> Quantifier -> ShowS

show :: Quantifier -> String

showList :: [Quantifier] -> ShowS

type QuantSet = (Quantifier, [Atom])

Quantified set of variables

type Atom = Var

Synonym of Var

type Lit = Int

Positive (resp. negative) literals are represented as positive (resp. negative) integers. (DIMACS format).

type Clause = [Lit]

Disjunction of Lit.

type PackedClause = Vector PackedLit

packClause :: Clause -> PackedClause

unpackClause :: PackedClause -> Clause

parseFile :: (FileFormat a, MonadIO m) => FilePath -> m (Either String a)

Parse a file but returns an error message when parsing fails.

parseByteString :: ByteString -> Either String QDimacs

Parse a QDimacs file but returns an error message when parsing fails.

Generating .qdimacs files

writeFile :: (FileFormat a, MonadIO m) => FilePath -> a -> m ()

Write a value into a file.

hPutQDimacs :: Handle -> QDimacs -> IO ()

Output a QDimacs to a Handle.

qdimacsBuilder :: QDimacs -> Builder

Encode a QDimacs to a Builder