Copyright	(c) Masahiro Sakai 2011-2015
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Portability	non-portable (BangPatterns)
Safe Haskell	Safe-Inferred
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

data Formula = Formula {
- pbObjectiveFunction :: Maybe Sum
- pbConstraints :: [Constraint]
- pbNumVars :: !Int
- pbNumConstraints :: !Int
}
type Constraint = (Sum, Op, Integer)
data Op
- = Ge
- | Eq
data SoftFormula = SoftFormula {
- wboTopCost :: Maybe Integer
- wboConstraints :: [SoftConstraint]
- wboNumVars :: !Int
- wboNumConstraints :: !Int
}
type SoftConstraint = (Maybe Integer, Constraint)
type Sum = [WeightedTerm]
type WeightedTerm = (Integer, Term)
type Term = [Lit]
type Lit = Int
type Var = Int
parseOPBString :: SourceName -> String -> Either ParseError Formula
parseOPBByteString :: SourceName -> ByteString -> Either ParseError Formula
parseOPBFile :: FilePath -> IO (Either ParseError Formula)
parseWBOString :: SourceName -> String -> Either ParseError SoftFormula
parseWBOByteString :: SourceName -> ByteString -> Either ParseError SoftFormula
parseWBOFile :: FilePath -> IO (Either ParseError SoftFormula)
toOPBString :: Formula -> String
toOPBByteString :: Formula -> ByteString
writeOPBFile :: FilePath -> Formula -> IO ()
hPutOPB :: Handle -> Formula -> IO ()
toWBOString :: SoftFormula -> String
toWBOByteString :: SoftFormula -> ByteString
writeWBOFile :: FilePath -> SoftFormula -> IO ()
hPutWBO :: Handle -> SoftFormula -> IO ()

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

Instances details

Data Formula Source #
Instance details 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 :: forall r r'. (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 #
Generic Formula Source #
Instance details Defined in Data.PseudoBoolean.Types Associated Types type Rep Formula :: Type -> Type # Methods from :: Formula -> Rep Formula x # to :: Rep Formula x -> Formula #
Read Formula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods readsPrec :: Int -> ReadS Formula # readList :: ReadS [Formula] # readPrec :: ReadPrec Formula # readListPrec :: ReadPrec [Formula] #
Show Formula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods showsPrec :: Int -> Formula -> ShowS # show :: Formula -> String # showList :: [Formula] -> ShowS #
NFData Formula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods rnf :: Formula -> () #
Eq Formula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods (==) :: Formula -> Formula -> Bool # (/=) :: Formula -> Formula -> Bool #
Ord Formula Source #
Instance details 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 #
Hashable Formula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods hashWithSalt :: Int -> Formula -> Int # hash :: Formula -> Int #
type Rep Formula Source #
Instance details Defined in Data.PseudoBoolean.Types type Rep Formula = D1 ('MetaData "Formula" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.11.0-8xMFhwmpT0y1DimHaW4rhk" '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) Source #

Lhs, relational operator and rhs.

data Op Source #

Relational operators

Constructors

Ge	greater than or equal
Eq	equal

Instances

Instances details

Data Op Source #
Instance details 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 :: forall r r'. (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 #
Bounded Op Source #
Instance details Defined in Data.PseudoBoolean.Types Methods minBound :: Op # maxBound :: Op #
Enum Op Source #
Instance details 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] #
Generic Op Source #
Instance details Defined in Data.PseudoBoolean.Types Associated Types type Rep Op :: Type -> Type # Methods from :: Op -> Rep Op x # to :: Rep Op x -> Op #
Read Op Source #
Instance details Defined in Data.PseudoBoolean.Types Methods readsPrec :: Int -> ReadS Op # readList :: ReadS [Op] # readPrec :: ReadPrec Op # readListPrec :: ReadPrec [Op] #
Show Op Source #
Instance details Defined in Data.PseudoBoolean.Types Methods showsPrec :: Int -> Op -> ShowS # show :: Op -> String # showList :: [Op] -> ShowS #
NFData Op Source #
Instance details Defined in Data.PseudoBoolean.Types Methods rnf :: Op -> () #
Eq Op Source #
Instance details Defined in Data.PseudoBoolean.Types Methods (==) :: Op -> Op -> Bool # (/=) :: Op -> Op -> Bool #
Ord Op Source #
Instance details 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 #
Hashable Op Source #
Instance details Defined in Data.PseudoBoolean.Types Methods hashWithSalt :: Int -> Op -> Int # hash :: Op -> Int #
type Rep Op Source #
Instance details Defined in Data.PseudoBoolean.Types type Rep Op = D1 ('MetaData "Op" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.11.0-8xMFhwmpT0y1DimHaW4rhk" 'False) (C1 ('MetaCons "Ge" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Eq" 'PrefixI 'False) (U1 :: Type -> Type))

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

Instances details

Data SoftFormula Source #
Instance details 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 :: forall r r'. (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 #
Generic SoftFormula Source #
Instance details Defined in Data.PseudoBoolean.Types Associated Types type Rep SoftFormula :: Type -> Type # Methods from :: SoftFormula -> Rep SoftFormula x # to :: Rep SoftFormula x -> SoftFormula #
Read SoftFormula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods readsPrec :: Int -> ReadS SoftFormula # readList :: ReadS [SoftFormula] # readPrec :: ReadPrec SoftFormula # readListPrec :: ReadPrec [SoftFormula] #
Show SoftFormula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods showsPrec :: Int -> SoftFormula -> ShowS # show :: SoftFormula -> String # showList :: [SoftFormula] -> ShowS #
NFData SoftFormula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods rnf :: SoftFormula -> () #
Eq SoftFormula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods (==) :: SoftFormula -> SoftFormula -> Bool # (/=) :: SoftFormula -> SoftFormula -> Bool #
Ord SoftFormula Source #
Instance details 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 #
Hashable SoftFormula Source #
Instance details Defined in Data.PseudoBoolean.Types Methods hashWithSalt :: Int -> SoftFormula -> Int # hash :: SoftFormula -> Int #
type Rep SoftFormula Source #
Instance details Defined in Data.PseudoBoolean.Types type Rep SoftFormula = D1 ('MetaData "SoftFormula" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.11.0-8xMFhwmpT0y1DimHaW4rhk" '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) 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.