Text.PBFile

A parser library for .opb file and .wbo files used by PB Competition.

References:

• Input/Output Format and Solver Requirements for the Competitions of Pseudo-Boolean Solvers http://www.cril.univ-artois.fr/PB11/format.pdf

Abstract Syntax

type Formula = (Maybe Sum, [Constraint])

Pair of objective function and a list of constraints.

type Constraint = (Sum, Op, Integer)

Lhs, relational operator and rhs.

data Op

Relational operators

Constructors

Ge

greater than or equal

Eq

equal

Instances

Bounded Op

Enum Op

Eq Op

Ord Op

Show Op

type SoftFormula = (Maybe Integer, [SoftConstraint])

A pair of top cost and a list of soft constraints.

type SoftConstraint = (Maybe Integer, Constraint)

A pair of weight and constraint.

type Sum = [WeightedTerm]

Sum of WeightedTerm

type WeightedTerm = (Integer, Term)

Coefficient and Term

type Term = [Lit]

List of variables interpreted as products

type Lit = Int

Positive (resp. negative) literal is represented as a positive (resp. negative) integer.

type Var = Int

Variable are repserented positive integer.

Parsing .opb files

parseOPBString :: SourceName -> String -> Either ParseError Formula

Parse a .opb file containing pseudo boolean problem.

parseOPBFile :: FilePath -> IO (Either ParseError Formula)

Parse a .opb format string containing pseudo boolean problem.

Parsing .wbo files

parseWBOString :: SourceName -> String -> Either ParseError SoftFormula

Parse a .wbo file containing weighted boolean optimization problem.

parseWBOFile :: FilePath -> IO (Either ParseError SoftFormula)

Parse a .wbo format string containing weighted boolean optimization problem.

Show .opb files

showOPB :: Formula -> ShowS

Show .wbo files

showWBO :: SoftFormula -> ShowS

Utility

pbNumVars :: Formula -> Int

wboNumVars :: SoftFormula -> Int