Copyright	(c) Masahiro Sakai 2016-2018
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	provisional
Portability	non-portable
Safe Haskell	None
Language	Haskell2010
Extensions	BangPatterns OverloadedStrings

ToySolver.FileFormat.CNF

Contents

FileFormat class
CNF format
WCNF formats
GCNF format
QDIMACS format
Re-exports

Description

Reader and Writer for DIMACS CNF and family of similar formats.

Synopsis

module ToySolver.FileFormat.Base
data CNF = CNF {
- cnfNumVars :: !Int
- cnfNumClauses :: !Int
- cnfClauses :: [PackedClause]
}
data WCNF = WCNF {
- wcnfNumVars :: !Int
- wcnfNumClauses :: !Int
- wcnfTopCost :: !Weight
- wcnfClauses :: [WeightedClause]
}
type WeightedClause = (Weight, PackedClause)
type Weight = Integer
newtype NewWCNF = NewWCNF {
- nwcnfClauses :: [NewWeightedClause]
}
data SomeWCNF
- = SomeWCNFOld WCNF
- | SomeWCNFNew NewWCNF
data GCNF = GCNF {
- gcnfNumVars :: !Int
- gcnfNumClauses :: !Int
- gcnfLastGroupIndex :: !GroupIndex
- gcnfClauses :: [GClause]
}
type GroupIndex = Int
type GClause = (GroupIndex, PackedClause)
data QDimacs = QDimacs {
- qdimacsNumVars :: !Int
- qdimacsNumClauses :: !Int
- qdimacsPrefix :: [QuantSet]
- qdimacsMatrix :: [PackedClause]
}
data Quantifier
- = E
- | A
type QuantSet = (Quantifier, [Atom])
type Atom = Var
type Lit = Int
type Clause = [Lit]
type PackedClause = Vector PackedLit
packClause :: Clause -> PackedClause
unpackClause :: PackedClause -> Clause

FileFormat class

module ToySolver.FileFormat.Base

CNF format

data CNF Source #

DIMACS CNF format

Constructors

CNF
Fields cnfNumVars :: !Int Number of variables cnfNumClauses :: !Int Number of clauses cnfClauses :: [PackedClause] Clauses

Instances

Instances details

Eq CNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: CNF -> CNF -> Bool # (/=) :: CNF -> CNF -> Bool #
Ord CNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods compare :: CNF -> CNF -> Ordering # (<) :: CNF -> CNF -> Bool # (<=) :: CNF -> CNF -> Bool # (>) :: CNF -> CNF -> Bool # (>=) :: CNF -> CNF -> Bool # max :: CNF -> CNF -> CNF # min :: CNF -> CNF -> CNF #
Read CNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS CNF # readList :: ReadS [CNF] # readPrec :: ReadPrec CNF # readListPrec :: ReadPrec [CNF] #
Show CNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> CNF -> ShowS # show :: CNF -> String # showList :: [CNF] -> ShowS #
FileFormat CNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods parse :: ByteString -> Either String CNF Source # render :: CNF -> Builder Source #

WCNF formats

(Old) WCNF format

data WCNF Source #

WCNF format for representing partial weighted Max-SAT problems.

This format is used for for MAX-SAT evaluations.

References:

http://maxsat.ia.udl.cat/requirements/

Constructors

WCNF
Fields wcnfNumVars :: !Int Number of variables wcnfNumClauses :: !Int Number of (weighted) clauses wcnfTopCost :: !Weight Hard clauses have weight equal or greater than "top". We assure that "top" is a weight always greater than the sum of the weights of violated soft clauses in the solution. wcnfClauses :: [WeightedClause] Weighted clauses

Instances

Instances details

Eq WCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: WCNF -> WCNF -> Bool # (/=) :: WCNF -> WCNF -> Bool #
Ord WCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods compare :: WCNF -> WCNF -> Ordering # (<) :: WCNF -> WCNF -> Bool # (<=) :: WCNF -> WCNF -> Bool # (>) :: WCNF -> WCNF -> Bool # (>=) :: WCNF -> WCNF -> Bool # max :: WCNF -> WCNF -> WCNF # min :: WCNF -> WCNF -> WCNF #
Read WCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS WCNF # readList :: ReadS [WCNF] # readPrec :: ReadPrec WCNF # readListPrec :: ReadPrec [WCNF] #
Show WCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> WCNF -> ShowS # show :: WCNF -> String # showList :: [WCNF] -> ShowS #
FileFormat WCNF Source #	Note that `parse` also accepts new WCNF files and (unweighted) CNF files and converts them into `WCNF`.
Instance details Defined in ToySolver.FileFormat.CNF Methods parse :: ByteString -> Either String WCNF Source # render :: WCNF -> Builder Source #

type WeightedClause = (Weight, PackedClause) Source #

Weighted clauses

type Weight = Integer Source #

Weigths must be greater than or equal to 1, and smaller than 2^63.

New WCNF format

newtype NewWCNF Source #

New WCNF file format

This format is used for for MAX-SAT evaluations >=2020.

References:

https://maxsat-evaluations.github.io/2021/format.html

Constructors

NewWCNF
Fields nwcnfClauses :: [NewWeightedClause] Weighted clauses

Instances

Instances details

Eq NewWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: NewWCNF -> NewWCNF -> Bool # (/=) :: NewWCNF -> NewWCNF -> Bool #
Ord NewWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods compare :: NewWCNF -> NewWCNF -> Ordering # (<) :: NewWCNF -> NewWCNF -> Bool # (<=) :: NewWCNF -> NewWCNF -> Bool # (>) :: NewWCNF -> NewWCNF -> Bool # (>=) :: NewWCNF -> NewWCNF -> Bool # max :: NewWCNF -> NewWCNF -> NewWCNF # min :: NewWCNF -> NewWCNF -> NewWCNF #
Read NewWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS NewWCNF # readList :: ReadS [NewWCNF] # readPrec :: ReadPrec NewWCNF # readListPrec :: ReadPrec [NewWCNF] #
Show NewWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> NewWCNF -> ShowS # show :: NewWCNF -> String # showList :: [NewWCNF] -> ShowS #
FileFormat NewWCNF Source #	Note that `parse` also accepts (old) WCNF files and (unweighted) CNF files and converts them into `NewWCNF`.
Instance details Defined in ToySolver.FileFormat.CNF Methods parse :: ByteString -> Either String NewWCNF Source # render :: NewWCNF -> Builder Source #

Old or new WCNF

data SomeWCNF Source #

Constructors

SomeWCNFOld WCNF
SomeWCNFNew NewWCNF

Instances

Instances details

Eq SomeWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: SomeWCNF -> SomeWCNF -> Bool # (/=) :: SomeWCNF -> SomeWCNF -> Bool #
Ord SomeWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods compare :: SomeWCNF -> SomeWCNF -> Ordering # (<) :: SomeWCNF -> SomeWCNF -> Bool # (<=) :: SomeWCNF -> SomeWCNF -> Bool # (>) :: SomeWCNF -> SomeWCNF -> Bool # (>=) :: SomeWCNF -> SomeWCNF -> Bool # max :: SomeWCNF -> SomeWCNF -> SomeWCNF # min :: SomeWCNF -> SomeWCNF -> SomeWCNF #
Read SomeWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS SomeWCNF # readList :: ReadS [SomeWCNF] # readPrec :: ReadPrec SomeWCNF # readListPrec :: ReadPrec [SomeWCNF] #
Show SomeWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> SomeWCNF -> ShowS # show :: SomeWCNF -> String # showList :: [SomeWCNF] -> ShowS #
FileFormat SomeWCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods parse :: ByteString -> Either String SomeWCNF Source # render :: SomeWCNF -> Builder Source #

GCNF format

data GCNF Source #

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

Instances details

Eq GCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: GCNF -> GCNF -> Bool # (/=) :: GCNF -> GCNF -> Bool #
Ord GCNF Source #
Instance details 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 Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS GCNF # readList :: ReadS [GCNF] # readPrec :: ReadPrec GCNF # readListPrec :: ReadPrec [GCNF] #
Show GCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> GCNF -> ShowS # show :: GCNF -> String # showList :: [GCNF] -> ShowS #
FileFormat GCNF Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods parse :: ByteString -> Either String GCNF Source # render :: GCNF -> Builder Source #

type GroupIndex = Int Source #

Component number between 0 and gcnfLastGroupIndex

type GClause = (GroupIndex, PackedClause) Source #

Clause together with component number

QDIMACS format

data QDimacs Source #

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

Instances details

Eq QDimacs Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: QDimacs -> QDimacs -> Bool # (/=) :: QDimacs -> QDimacs -> Bool #
Ord QDimacs Source #
Instance details 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 Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS QDimacs # readList :: ReadS [QDimacs] # readPrec :: ReadPrec QDimacs # readListPrec :: ReadPrec [QDimacs] #
Show QDimacs Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> QDimacs -> ShowS # show :: QDimacs -> String # showList :: [QDimacs] -> ShowS #
FileFormat QDimacs Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods parse :: ByteString -> Either String QDimacs Source # render :: QDimacs -> Builder Source #

data Quantifier Source #

Quantifier

Constructors

E	existential quantifier (∃)
A	universal quantifier (∀)

Instances

Instances details

Bounded Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods minBound :: Quantifier # maxBound :: Quantifier #
Enum Quantifier Source #
Instance details 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 Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods (==) :: Quantifier -> Quantifier -> Bool # (/=) :: Quantifier -> Quantifier -> Bool #
Ord Quantifier Source #
Instance details 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 Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods readsPrec :: Int -> ReadS Quantifier # readList :: ReadS [Quantifier] # readPrec :: ReadPrec Quantifier # readListPrec :: ReadPrec [Quantifier] #
Show Quantifier Source #
Instance details Defined in ToySolver.FileFormat.CNF Methods showsPrec :: Int -> Quantifier -> ShowS # show :: Quantifier -> String # showList :: [Quantifier] -> ShowS #

type QuantSet = (Quantifier, [Atom]) Source #

Quantified set of variables

type Atom = Var Source #

Synonym of Var

Re-exports

type Lit = Int Source #

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

type Clause = [Lit] Source #

Disjunction of Lit.

type PackedClause = Vector PackedLit Source #

packClause :: Clause -> PackedClause Source #

unpackClause :: PackedClause -> Clause Source #