Copyright | (c) Masahiro Sakai 2011-2015 |
---|---|
License | BSD-style |
Maintainer | masahiro.sakai@gmail.com |
Portability | non-portable (BangPatterns) |
Safe Haskell | Safe |
Language | Haskell2010 |
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
- 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
Pair of objective function and a list of constraints.
Formula | |
|
Instances
Eq Formula Source # | |
Data Formula Source # | |
Defined in Data.PseudoBoolean.Types 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 # | |
Read Formula Source # | |
Show Formula Source # | |
Generic Formula Source # | |
NFData Formula Source # | |
Defined in Data.PseudoBoolean.Types | |
Hashable Formula Source # | |
Defined in Data.PseudoBoolean.Types | |
type Rep Formula Source # | |
Defined in Data.PseudoBoolean.Types type Rep Formula = D1 (MetaData "Formula" "Data.PseudoBoolean.Types" "pseudo-boolean-0.1.9.0-6u1UD8KWgvYHZ3w7B8IdP5" 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)))) |
Relational operators
Instances
Bounded Op Source # | |
Enum Op Source # | |
Eq Op Source # | |
Data Op Source # | |
Defined in Data.PseudoBoolean.Types 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 # 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 # | |
Read Op Source # | |
Show Op Source # | |
Generic Op Source # | |
NFData Op Source # | |
Defined in Data.PseudoBoolean.Types | |
Hashable Op Source # | |
Defined in Data.PseudoBoolean.Types | |
type Rep Op Source # | |
data SoftFormula Source #
A pair of top cost and a list of soft constraints.
SoftFormula | |
|
Instances
type SoftConstraint = (Maybe Integer, Constraint) Source #
A pair of weight and constraint.
type Sum = [WeightedTerm] Source #
Sum of WeightedTerm
Positive (resp. negative) literals are represented as positive (resp. negative) 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.