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 Source #
Methods (==) :: Formula -> Formula -> Bool # (/=) :: Formula -> Formula -> Bool #
Data Formula Source #
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 Source #
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 Source #
Methods showsPrec :: Int -> Formula -> ShowS # show :: Formula -> String # showList :: [Formula] -> ShowS #
Generic Formula Source #
Associated Types type Rep Formula :: * -> * # Methods from :: Formula -> Rep Formula x # to :: Rep Formula x -> Formula #
NFData Formula Source #
Methods rnf :: Formula -> () #
Hashable Formula Source #
Methods hashWithSalt :: Int -> Formula -> Int # hash :: Formula -> Int #
type Rep Formula Source #
type Rep Formula = D1 (MetaData "Formula" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.4.0-4HCaSjnIZDVLgZWPJVixs7" False) (C1 (MetaCons "Formula" PrefixI True) ((::) ((::) (S1 (MetaSel (Just Symbol "pbObjectiveFunction") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Sum))) (S1 (MetaSel (Just Symbol "pbConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Constraint]))) ((:*:) (S1 (MetaSel (Just Symbol "pbNumVars") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)) (S1 (MetaSel (Just Symbol "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

Bounded Op Source #
Methods minBound :: Op # maxBound :: Op #
Enum Op Source #
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 Source #
Methods (==) :: Op -> Op -> Bool # (/=) :: Op -> Op -> Bool #
Data Op Source #
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 Source #
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 Source #
Methods showsPrec :: Int -> Op -> ShowS # show :: Op -> String # showList :: [Op] -> ShowS #
Generic Op Source #
Associated Types type Rep Op :: * -> * # Methods from :: Op -> Rep Op x # to :: Rep Op x -> Op #
NFData Op Source #
Methods rnf :: Op -> () #
Hashable Op Source #
Methods hashWithSalt :: Int -> Op -> Int # hash :: Op -> Int #
type Rep Op Source #
type Rep Op = D1 (MetaData "Op" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.4.0-4HCaSjnIZDVLgZWPJVixs7" False) ((:+:) (C1 (MetaCons "Ge" PrefixI False) U1) (C1 (MetaCons "Eq" PrefixI False) U1))

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 Source #
Methods (==) :: SoftFormula -> SoftFormula -> Bool # (/=) :: SoftFormula -> SoftFormula -> Bool #
Data SoftFormula Source #
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 Source #
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 Source #
Methods showsPrec :: Int -> SoftFormula -> ShowS # show :: SoftFormula -> String # showList :: [SoftFormula] -> ShowS #
Generic SoftFormula Source #
Associated Types type Rep SoftFormula :: * -> * # Methods from :: SoftFormula -> Rep SoftFormula x # to :: Rep SoftFormula x -> SoftFormula #
NFData SoftFormula Source #
Methods rnf :: SoftFormula -> () #
Hashable SoftFormula Source #
Methods hashWithSalt :: Int -> SoftFormula -> Int # hash :: SoftFormula -> Int #
type Rep SoftFormula Source #
type Rep SoftFormula = D1 (MetaData "SoftFormula" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.4.0-4HCaSjnIZDVLgZWPJVixs7" False) (C1 (MetaCons "SoftFormula" PrefixI True) ((::) ((::) (S1 (MetaSel (Just Symbol "wboTopCost") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Integer))) (S1 (MetaSel (Just Symbol "wboConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [SoftConstraint]))) ((:*:) (S1 (MetaSel (Just Symbol "wboNumVars") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Int)) (S1 (MetaSel (Just Symbol "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.