Copyright	(c) Masahiro Sakai 2011-2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Portability	non-portable (BangPatterns)
Safe Haskell	None
Language	Haskell2010

Data.PseudoBoolean

Contents

Abstract Syntax
Parsing OPB files
Parsing WBO files
Generating OPB files
Generating WBO files

Description

A library for parsing/generating OPB/WBO files used in pseudo boolean competition.

References:

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

Synopsis

Abstract Syntax

data Formula Source

Pair of objective function and a list of constraints.

Constructors

Formula
Fields pbObjectiveFunction :: Maybe Sum pbConstraints :: [Constraint] pbNumVars :: !Int pbNumConstraints :: !Int

Instances

Eq Formula
Data Formula
Ord Formula
Show Formula
Generic Formula
NFData Formula
Hashable Formula
Typeable * Formula
type Rep Formula

type Constraint = (Sum, Op, Integer) Source

Lhs, relational operator and rhs.

data Op Source

Relational operators

Constructors

Ge	greater than or equal
Eq	equal

Instances

Bounded Op
Enum Op
Eq Op
Data Op
Ord Op
Show Op
Generic Op
NFData Op
Hashable Op
Typeable * Op
type Rep Op

data SoftFormula Source

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

Constructors

SoftFormula
Fields wboTopCost :: Maybe Integer wboConstraints :: [SoftConstraint] wboNumVars :: !Int wboNumConstraints :: !Int

Instances

Eq SoftFormula
Data SoftFormula
Ord SoftFormula
Show SoftFormula
Generic SoftFormula
NFData SoftFormula
Hashable SoftFormula
Typeable * SoftFormula
type Rep SoftFormula

type SoftConstraint = (Maybe Integer, Constraint) Source

A pair of weight and constraint.

type Sum = [WeightedTerm] Source

Sum of WeightedTerm

type WeightedTerm = (Integer, Term) Source

Coefficient and Term

type Term = [Lit] Source

List of variables interpreted as products

type Lit = Int Source

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

type Var = Int Source

Variable are repserented as positive integers.

Parsing OPB files

These functions are based on Parsec. If you want faster parser, you can also use Data.PseudoBoolean.Attoparsec module.

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

Parse a OPB format string containing pseudo boolean problem.

parseOPBByteString :: SourceName -> ByteString -> Either ParseError Formula Source

Parse a OPB format lazy bytestring containing pseudo boolean problem.

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

Parse a OPB file containing pseudo boolean problem.

Parsing WBO files

These functions are based on Parsec. If you want faster parser, you can also use Data.PseudoBoolean.Attoparsec module.

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

Parse a WBO format string containing weighted boolean optimization problem.

parseWBOByteString :: SourceName -> ByteString -> Either ParseError SoftFormula Source

Parse a WBO format lazy bytestring containing pseudo boolean problem.

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

Parse a WBO file containing weighted boolean optimization problem.

Generating OPB files

toOPBString :: Formula -> String Source

Generate a OPB format string containing pseudo boolean problem.

toOPBByteString :: Formula -> ByteString Source

Generate a OPB format byte-string containing pseudo boolean problem.

writeOPBFile :: FilePath -> Formula -> IO () Source

Output a OPB file containing pseudo boolean problem.

hPutOPB :: Handle -> Formula -> IO () Source

Output a OPB file to a Handle using hPutBuilder.

It is recommended that the Handle is set to binary and BlockBuffering mode. See hSetBinaryMode and hSetBuffering.

This function is more efficient than hPut . toOPBByteString because in many cases no buffer allocation has to be done.

Generating WBO files

toWBOString :: SoftFormula -> String Source

Generate a WBO format string containing weighted boolean optimization problem.

toWBOByteString :: SoftFormula -> ByteString Source

Generate a WBO format byte-string containing weighted boolean optimization problem.

writeWBOFile :: FilePath -> SoftFormula -> IO () Source

Output a WBO file containing weighted boolean optimization problem.

hPutWBO :: Handle -> SoftFormula -> IO () Source

Output a WBO file to a Handle using hPutBuilder.

It is recommended that the Handle is set to binary and BlockBuffering mode. See hSetBinaryMode and hSetBuffering.

This function is more efficient than hPut . toWBOByteString because in many cases no buffer allocation has to be done.