ToySolver.Text.GCNF

Deprecated: Use ToySolver.FileFormat.CNF instead

Documentation

data GCNF

Group oriented CNF Input Format

This format is used in Group oriented MUS track of the SAT Competition 2011.

References:

• http://www.satcompetition.org/2011/rules.pdf

Constructors

GCNF

Fields

• gcnfNumVars :: !Int

  Nubmer of variables

• gcnfNumClauses :: !Int

  Number of clauses

• gcnfLastGroupIndex :: !GroupIndex

  The last index of a group in the file number of components contained in the file.

• gcnfClauses :: [GClause]

Instances

Eq GCNF

Defined in ToySolver.FileFormat.CNF

Methods

(==) :: GCNF -> GCNF -> Bool

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

Ord GCNF

Defined in ToySolver.FileFormat.CNF

Methods

compare :: GCNF -> GCNF -> Ordering

(<) :: GCNF -> GCNF -> Bool

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

(>) :: GCNF -> GCNF -> Bool

(>=) :: GCNF -> GCNF -> Bool

max :: GCNF -> GCNF -> GCNF

min :: GCNF -> GCNF -> GCNF

Read GCNF

Defined in ToySolver.FileFormat.CNF

Methods

readsPrec :: Int -> ReadS GCNF

readList :: ReadS [GCNF]

readPrec :: ReadPrec GCNF

readListPrec :: ReadPrec [GCNF]

Show GCNF

Defined in ToySolver.FileFormat.CNF

Methods

showsPrec :: Int -> GCNF -> ShowS

show :: GCNF -> String

showList :: [GCNF] -> ShowS

FileFormat GCNF

Defined in ToySolver.FileFormat.CNF

Methods

parse :: ByteString -> Either String GCNF

render :: GCNF -> Builder

type GroupIndex = Int

Component number between 0 and gcnfLastGroupIndex

type GClause = (GroupIndex, PackedClause)

Clause together with component number

Parsing .gcnf files

parseByteString :: ByteString -> Either String GCNF

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

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

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

Generating .gcnf files

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

Write a value into a file.

hPutGCNF :: Handle -> GCNF -> IO ()

Output a GCNF to a Handle.

gcnfBuilder :: GCNF -> Builder

Encode a GCNF to a Builder