Data.PseudoBoolean

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

Abstract Syntax

data Formula

Pair of objective function and a list of constraints.

Constructors

Formula

Fields

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

Instances

Eq Formula

Defined in Data.PseudoBoolean.Types

Methods

(==) :: Formula -> Formula -> Bool

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

Data Formula

Defined in Data.PseudoBoolean.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Formula -> c Formula

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Formula

toConstr :: Formula -> Constr

dataTypeOf :: Formula -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Formula)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Formula)

gmapT :: (forall b. Data b => b -> b) -> Formula -> Formula

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Formula -> r

gmapQ :: (forall d. Data d => d -> u) -> Formula -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Formula -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Formula -> m Formula

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Formula -> m Formula

Ord Formula

Defined in Data.PseudoBoolean.Types

Methods

compare :: Formula -> Formula -> Ordering

(<) :: Formula -> Formula -> Bool

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

(>) :: Formula -> Formula -> Bool

(>=) :: Formula -> Formula -> Bool

max :: Formula -> Formula -> Formula

min :: Formula -> Formula -> Formula

Show Formula

Defined in Data.PseudoBoolean.Types

Methods

showsPrec :: Int -> Formula -> ShowS

show :: Formula -> String

showList :: [Formula] -> ShowS

Generic Formula

Defined in Data.PseudoBoolean.Types

Associated Types

type Rep Formula :: * -> *

Methods

from :: Formula -> Rep Formula x

to :: Rep Formula x -> Formula

NFData Formula

Defined in Data.PseudoBoolean.Types

Methods

rnf :: Formula -> ()

Hashable Formula

Defined in Data.PseudoBoolean.Types

Methods

hashWithSalt :: Int -> Formula -> Int

hash :: Formula -> Int

type Rep Formula

Defined in Data.PseudoBoolean.Types

type Rep Formula = D1 (MetaData "Formula" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.7.0-BV4H5TocFKGKViCHvhlkoG" False) (C1 (MetaCons "Formula" PrefixI True) ((S1 (MetaSel (Just "pbObjectiveFunction") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Sum)) :*: S1 (MetaSel (Just "pbConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Constraint])) :*: (S1 (MetaSel (Just "pbNumVars") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :*: S1 (MetaSel (Just "pbNumConstraints") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int))))

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

Defined in Data.PseudoBoolean.Types

Methods

minBound :: Op

maxBound :: Op

Enum Op

Defined in Data.PseudoBoolean.Types

Methods

succ :: Op -> Op

pred :: Op -> Op

toEnum :: Int -> Op

fromEnum :: Op -> Int

enumFrom :: Op -> [Op]

enumFromThen :: Op -> Op -> [Op]

enumFromTo :: Op -> Op -> [Op]

enumFromThenTo :: Op -> Op -> Op -> [Op]

Eq Op

Defined in Data.PseudoBoolean.Types

Methods

(==) :: Op -> Op -> Bool

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

Data Op

Defined in Data.PseudoBoolean.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Op -> c Op

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Op

toConstr :: Op -> Constr

dataTypeOf :: Op -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Op)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Op)

gmapT :: (forall b. Data b => b -> b) -> Op -> Op

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Op -> r

gmapQ :: (forall d. Data d => d -> u) -> Op -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Op -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Op -> m Op

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Op -> m Op

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Op -> m Op

Ord Op

Defined in Data.PseudoBoolean.Types

Methods

compare :: Op -> Op -> Ordering

(<) :: Op -> Op -> Bool

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

(>) :: Op -> Op -> Bool

(>=) :: Op -> Op -> Bool

max :: Op -> Op -> Op

min :: Op -> Op -> Op

Show Op

Defined in Data.PseudoBoolean.Types

Methods

showsPrec :: Int -> Op -> ShowS

show :: Op -> String

showList :: [Op] -> ShowS

Generic Op

Defined in Data.PseudoBoolean.Types

Associated Types

type Rep Op :: * -> *

Methods

from :: Op -> Rep Op x

to :: Rep Op x -> Op

NFData Op

Defined in Data.PseudoBoolean.Types

Methods

rnf :: Op -> ()

Hashable Op

Defined in Data.PseudoBoolean.Types

Methods

hashWithSalt :: Int -> Op -> Int

hash :: Op -> Int

type Rep Op

Defined in Data.PseudoBoolean.Types

type Rep Op = D1 (MetaData "Op" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.7.0-BV4H5TocFKGKViCHvhlkoG" False) (C1 (MetaCons "Ge" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "Eq" PrefixI False) (U1 :: * -> *))

data SoftFormula

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

Defined in Data.PseudoBoolean.Types

Methods

(==) :: SoftFormula -> SoftFormula -> Bool

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

Data SoftFormula

Defined in Data.PseudoBoolean.Types

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SoftFormula -> c SoftFormula

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SoftFormula

toConstr :: SoftFormula -> Constr

dataTypeOf :: SoftFormula -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SoftFormula)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SoftFormula)

gmapT :: (forall b. Data b => b -> b) -> SoftFormula -> SoftFormula

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SoftFormula -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SoftFormula -> r

gmapQ :: (forall d. Data d => d -> u) -> SoftFormula -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SoftFormula -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SoftFormula -> m SoftFormula

Ord SoftFormula

Defined in Data.PseudoBoolean.Types

Methods

compare :: SoftFormula -> SoftFormula -> Ordering

(<) :: SoftFormula -> SoftFormula -> Bool

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

(>) :: SoftFormula -> SoftFormula -> Bool

(>=) :: SoftFormula -> SoftFormula -> Bool

max :: SoftFormula -> SoftFormula -> SoftFormula

min :: SoftFormula -> SoftFormula -> SoftFormula

Show SoftFormula

Defined in Data.PseudoBoolean.Types

Methods

showsPrec :: Int -> SoftFormula -> ShowS

show :: SoftFormula -> String

showList :: [SoftFormula] -> ShowS

Generic SoftFormula

Defined in Data.PseudoBoolean.Types

Associated Types

type Rep SoftFormula :: * -> *

Methods

from :: SoftFormula -> Rep SoftFormula x

to :: Rep SoftFormula x -> SoftFormula

NFData SoftFormula

Defined in Data.PseudoBoolean.Types

Methods

rnf :: SoftFormula -> ()

Hashable SoftFormula

Defined in Data.PseudoBoolean.Types

Methods

hashWithSalt :: Int -> SoftFormula -> Int

hash :: SoftFormula -> Int

type Rep SoftFormula

Defined in Data.PseudoBoolean.Types

type Rep SoftFormula = D1 (MetaData "SoftFormula" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.7.0-BV4H5TocFKGKViCHvhlkoG" False) (C1 (MetaCons "SoftFormula" PrefixI True) ((S1 (MetaSel (Just "wboTopCost") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Integer)) :*: S1 (MetaSel (Just "wboConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [SoftConstraint])) :*: (S1 (MetaSel (Just "wboNumVars") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int) :*: S1 (MetaSel (Just "wboNumConstraints") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int))))

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) literals are represented as positive (resp. negative) integers.

type Var = Int

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

Parse a OPB format string containing pseudo boolean problem.

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

Parse a OPB format lazy bytestring containing pseudo boolean problem.

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

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

Parse a WBO format string containing weighted boolean optimization problem.

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

Parse a WBO format lazy bytestring containing pseudo boolean problem.

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

Parse a WBO file containing weighted boolean optimization problem.

Generating OPB files

toOPBString :: Formula -> String

Generate a OPB format string containing pseudo boolean problem.

toOPBByteString :: Formula -> ByteString

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

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

Output a OPB file containing pseudo boolean problem.

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

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

Generate a WBO format string containing weighted boolean optimization problem.

toWBOByteString :: SoftFormula -> ByteString

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

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

Output a WBO file containing weighted boolean optimization problem.

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

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.