{-# LANGUAGE BangPatterns, FlexibleContexts, TypeFamilies, CPP, ConstraintKinds #-}{-# LANGUAGE OverloadedStrings #-}{-# LANGUAGE TypeOperators #-}{-# OPTIONS_GHC -Wall #-}------------------------------------------------------------------------------- |-- Module : Data.PseudoBoolean.Megaparsec-- Copyright : (c) Masahiro Sakai 2011-2016-- License : BSD-style-- -- Maintainer : masahiro.sakai@gmail.com-- Portability : non-portable (BangPatterns, FlexibleContexts, TypeFamilies, CPP, ConstraintKinds)---- A parser library for OPB file and 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>-------------------------------------------------------------------------------moduleData.PseudoBoolean.Megaparsec(-- * Parsing OPB filesopbParser ,parseOPBString ,parseOPBByteString ,parseOPBFile -- * Parsing WBO files,wboParser ,parseWBOString ,parseWBOByteString ,parseWBOFile -- * Error type,ParseError )whereimportPreludehiding(sum)importControl.Applicative((<*))importControl.MonadimportData.ByteString.Lazy(ByteString)importqualifiedData.ByteString.Lazy.Char8asBLimportData.Maybe
#if MIN_VERSION_megaparsec(6,0,0)
importData.StringimportData.WordimportData.Void
#endif
importText.Megaparsechiding(ParseError)importqualifiedText.MegaparsecasMP
#if MIN_VERSION_megaparsec(6,0,0)
importText.Megaparsec.Byte
#else
importText.Megaparsec.Prim(MonadParsec())
#endif
importData.PseudoBoolean.Types importData.PseudoBoolean.Internal.TextUtil
#if MIN_VERSION_megaparsec(6,0,0)
typeC e s m =(MonadParsece s m ,Tokens ~Word8,IsString(Tokenss ))char8 ::C e s m =>Char->m Word8char8 :: forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 =Word8 -> m Word8
Token s -> m (Token s)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8) =>
Token s -> m (Token s)
char(Word8 -> m Word8) -> (Char -> Word8) -> Char -> m Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Int -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral(Int -> Word8) -> (Char -> Int) -> Char -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Char -> Int
forall a. Enum a => a -> Int
fromEnum
#else
#if MIN_VERSION_megaparsec(5,0,0)
typeCesm=(MonadParsecesm,Tokens~Char)
#elif MIN_VERSION_megaparsec(4,4,0)
typeCesm=(MonadParsecsmChar)
#else
typeCesm=(MonadParsecsmChar,MonadPlusm)
#endif
char8::Cesm=>Char->mCharchar8=char
#endif
#if MIN_VERSION_megaparsec(7,0,0)
anyChar ::C e s m =>m Word8anyChar :: forall e s (m :: * -> *). C e s m => m Word8
anyChar =m Word8
m (Token s)
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle
#endif
-- | Parser for OPB files
#if MIN_VERSION_megaparsec(6,0,0)
opbParser ::(MonadParsece s m ,Tokens ~Word8,IsString(Tokenss ))=>m Formula
#elif MIN_VERSION_megaparsec(5,0,0)
opbParser::(MonadParsecesm,Tokens~Char)=>mFormula
#elif MIN_VERSION_megaparsec(4,4,0)
opbParser::(MonadParsecsmChar)=>mFormula
#else
opbParser::(MonadParsecsmChar,MonadPlusm)=>mFormula
#endif
opbParser :: forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8, IsString (Tokens s)) =>
m Formula
opbParser =m Formula
forall e s (m :: * -> *). C e s m => m Formula
formula -- | Parser for WBO files
#if MIN_VERSION_megaparsec(6,0,0)
wboParser ::(MonadParsece s m ,Tokens ~Word8,IsString(Tokenss ))=>m SoftFormula
#elif MIN_VERSION_megaparsec(5,0,0)
wboParser::(MonadParsecesm,Tokens~Char)=>mSoftFormula
#elif MIN_VERSION_megaparsec(4,4,0)
wboParser::(MonadParsecsmChar)=>mSoftFormula
#else
wboParser::(MonadParsecsmChar,MonadPlusm)=>mSoftFormula
#endif
wboParser :: forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8, IsString (Tokens s)) =>
m SoftFormula
wboParser =m SoftFormula
forall e s (m :: * -> *). C e s m => m SoftFormula
softformula -- <formula>::= <sequence_of_comments> [<objective>] <sequence_of_comments_or_constraints>formula ::C e s m =>m Formula formula :: forall e s (m :: * -> *). C e s m => m Formula
formula =doMaybe (Int, Int)
h <-m (Int, Int) -> m (Maybe (Int, Int))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optionalm (Int, Int)
forall e s (m :: * -> *). C e s m => m (Int, Int)
hint m ()
forall e s (m :: * -> *). C e s m => m ()
sequence_of_comments Maybe Sum
obj <-m Sum -> m (Maybe Sum)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optionalm Sum
forall e s (m :: * -> *). C e s m => m Sum
objective [Constraint]
cs <-m [Constraint]
forall e s (m :: * -> *). C e s m => m [Constraint]
sequence_of_comments_or_constraints Formula -> m Formula
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Formula -> m Formula) -> Formula -> m Formula
forall a b. (a -> b) -> a -> b
$Formula {pbObjectiveFunction :: Maybe Sum
pbObjectiveFunction =Maybe Sum
obj ,pbConstraints :: [Constraint]
pbConstraints =[Constraint]
cs ,pbNumVars :: Int
pbNumVars =Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe(Maybe Sum -> [Constraint] -> Int
pbComputeNumVars Maybe Sum
obj [Constraint]
cs )(((Int, Int) -> Int) -> Maybe (Int, Int) -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap(Int, Int) -> Int
forall a b. (a, b) -> a
fstMaybe (Int, Int)
h ),pbNumConstraints :: Int
pbNumConstraints =Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe([Constraint] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length[Constraint]
cs )(((Int, Int) -> Int) -> Maybe (Int, Int) -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap(Int, Int) -> Int
forall a b. (a, b) -> b
sndMaybe (Int, Int)
h )}hint ::C e s m =>m (Int,Int)hint :: forall e s (m :: * -> *). C e s m => m (Int, Int)
hint =m (Int, Int) -> m (Int, Int)
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try(m (Int, Int) -> m (Int, Int)) -> m (Int, Int) -> m (Int, Int)
forall a b. (a -> b) -> a -> b
$doWord8
_<-Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
'*'m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace Tokens s
_<-Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
stringTokens s
"#variable="m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace Integer
nv <-m Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer m ()
forall e s (m :: * -> *). C e s m => m ()
oneOrMoreSpace Tokens s
_<-Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
stringTokens s
"#constraint="m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace Integer
nc <-m Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer [Word8]
_<-m Word8 -> m (Tokens s) -> m [Word8]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
manyTillm Word8
forall e s (m :: * -> *). C e s m => m Word8
anyChar m (Tokens s)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8) =>
m (Tokens s)
eol(Int, Int) -> m (Int, Int)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegralInteger
nv ,Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegralInteger
nc )-- <sequence_of_comments>::= <comment> [<sequence_of_comments>]sequence_of_comments ::C e s m =>m ()=m () -> m ()
forall (m :: * -> *) a. MonadPlus m => m a -> m ()
skipManym ()
forall e s (m :: * -> *). C e s m => m ()
comment -- XXX: we allow empty sequence-- <comment>::= "*" <any_sequence_of_characters_other_than_EOL> <EOL>comment ::C e s m =>m ()=doWord8
_<-Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
'*'[Word8]
_<-m Word8 -> m (Tokens s) -> m [Word8]
forall (m :: * -> *) a end. MonadPlus m => m a -> m end -> m [a]
manyTillm Word8
forall e s (m :: * -> *). C e s m => m Word8
anyChar m (Tokens s)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8) =>
m (Tokens s)
eolm ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8) =>
m ()
space-- We relax the grammer and allow spaces in the beggining of next component.() -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return()-- <sequence_of_comments_or_constraints>::= <comment_or_constraint> [<sequence_of_comments_or_constraints>]sequence_of_comments_or_constraints ::C e s m =>m [Constraint ]=do[Maybe Constraint]
xs <-m (Maybe Constraint) -> m [Maybe Constraint]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
manym (Maybe Constraint)
forall e s (m :: * -> *). C e s m => m (Maybe Constraint)
comment_or_constraint -- We relax the grammer and allow spaces in the beginning of next component.[Constraint] -> m [Constraint]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return([Constraint] -> m [Constraint]) -> [Constraint] -> m [Constraint]
forall a b. (a -> b) -> a -> b
$[Maybe Constraint] -> [Constraint]
forall a. [Maybe a] -> [a]
catMaybes[Maybe Constraint]
xs -- <comment_or_constraint>::= <comment>|<constraint>comment_or_constraint ::C e s m =>m (MaybeConstraint )=(m ()
forall e s (m :: * -> *). C e s m => m ()
comment m () -> m (Maybe Constraint) -> m (Maybe Constraint)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>Maybe Constraint -> m (Maybe Constraint)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
returnMaybe Constraint
forall a. Maybe a
Nothing)m (Maybe Constraint)
-> m (Maybe Constraint) -> m (Maybe Constraint)
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>((Constraint -> Maybe Constraint)
-> m Constraint -> m (Maybe Constraint)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftMConstraint -> Maybe Constraint
forall a. a -> Maybe a
Justm Constraint
forall e s (m :: * -> *). C e s m => m Constraint
constraint )-- <objective>::= "min:" <zeroOrMoreSpace> <sum> ";"objective ::C e s m =>m Sum objective :: forall e s (m :: * -> *). C e s m => m Sum
objective =doTokens s
_<-Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
stringTokens s
"min:"m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace Sum
obj <-m Sum
forall e s (m :: * -> *). C e s m => m Sum
sum m ()
forall e s (m :: * -> *). C e s m => m ()
semi Sum -> m Sum
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
returnSum
obj -- <constraint>::= <sum> <relational_operator> <zeroOrMoreSpace> <integer> <zeroOrMoreSpace> ";"constraint ::C e s m =>m Constraint constraint :: forall e s (m :: * -> *). C e s m => m Constraint
constraint =doSum
lhs <-m Sum
forall e s (m :: * -> *). C e s m => m Sum
sum Op
op <-m Op
forall e s (m :: * -> *). C e s m => m Op
relational_operator m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace Integer
rhs <-m Integer
forall e s (m :: * -> *). C e s m => m Integer
integer m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace m ()
forall e s (m :: * -> *). C e s m => m ()
semi Constraint -> m Constraint
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Sum
lhs ,Op
op ,Integer
rhs )-- <sum>::= <weightedterm> | <weightedterm> <sum>sum ::C e s m =>m Sum sum :: forall e s (m :: * -> *). C e s m => m Sum
sum =m WeightedTerm -> m Sum
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
manym WeightedTerm
forall e s (m :: * -> *). C e s m => m WeightedTerm
weightedterm -- we relax the grammer to allow empty sum-- <weightedterm>::= <integer> <oneOrMoreSpace> <term> <oneOrMoreSpace>weightedterm ::C e s m =>m WeightedTerm weightedterm :: forall e s (m :: * -> *). C e s m => m WeightedTerm
weightedterm =doInteger
w <-m Integer
forall e s (m :: * -> *). C e s m => m Integer
integer m ()
forall e s (m :: * -> *). C e s m => m ()
oneOrMoreSpace Term
t <-m Term
forall e s (m :: * -> *). C e s m => m Term
term m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace -- we relax the grammar to allow omitting spaces at the end of <sum>.WeightedTerm -> m WeightedTerm
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Integer
w ,Term
t )-- <integer>::= <unsigned_integer> | "+" <unsigned_integer> | "-" <unsigned_integer>integer ::C e s m =>m Integerinteger :: forall e s (m :: * -> *). C e s m => m Integer
integer =[m Integer] -> m Integer
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum[m Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer ,Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
'+'m Word8 -> m Integer -> m Integer
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>m Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer ,Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
'-'m Word8 -> m Integer -> m Integer
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>(Integer -> Integer) -> m Integer -> m Integer
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftMInteger -> Integer
forall a. Num a => a -> a
negatem Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer ]-- <unsigned_integer>::= <digit> | <digit><unsigned_integer>unsigned_integer ::C e s m =>m Integerunsigned_integer :: forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer =do[Word8]
ds <-m Word8 -> m [Word8]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
somem Word8
m (Token s)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8) =>
m (Token s)
digitChar
#if MIN_VERSION_megaparsec(6,0,0)
Integer -> m Integer
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Integer -> m Integer) -> Integer -> m Integer
forall a b. (a -> b) -> a -> b
$!String -> Integer
readUnsignedInteger ((Word8 -> Char) -> [Word8] -> String
forall a b. (a -> b) -> [a] -> [b]
map(Int -> Char
forall a. Enum a => Int -> a
toEnum(Int -> Char) -> (Word8 -> Int) -> Word8 -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Word8 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral)[Word8]
ds )
#else
return$!readUnsignedIntegerds
#endif
-- <relational_operator>::= ">=" | "="relational_operator ::C e s m =>m Op relational_operator :: forall e s (m :: * -> *). C e s m => m Op
relational_operator =(Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
stringTokens s
">="m (Tokens s) -> m Op -> m Op
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>Op -> m Op
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
returnOp
Ge )m Op -> m Op -> m Op
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>(Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
stringTokens s
"="m (Tokens s) -> m Op -> m Op
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>Op -> m Op
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
returnOp
Eq )-- <variablename>::= "x" <unsigned_integer>variablename ::C e s m =>m Var variablename :: forall e s (m :: * -> *). C e s m => m Int
variablename =doWord8
_<-Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
'x'Integer
i <-m Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer Int -> m Int
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Int -> m Int) -> Int -> m Int
forall a b. (a -> b) -> a -> b
$!Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegralInteger
i -- <oneOrMoreSpace>::= " " [<oneOrMoreSpace>]oneOrMoreSpace ::C e s m =>m ()oneOrMoreSpace :: forall e s (m :: * -> *). C e s m => m ()
oneOrMoreSpace =m Word8 -> m ()
forall (m :: * -> *) a. MonadPlus m => m a -> m ()
skipSome(Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
' ')-- <zeroOrMoreSpace>::= [" " <zeroOrMoreSpace>]zeroOrMoreSpace ::C e s m =>m ()-- zeroOrMoreSpace = skipMany (char8 ' ')zeroOrMoreSpace :: forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace =m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8) =>
m ()
space-- We relax the grammer and allow more type of spacingsemi ::C e s m =>m ()semi :: forall e s (m :: * -> *). C e s m => m ()
semi =Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
';'m Word8 -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>m ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Word8) =>
m ()
space-- We relax the grammer and allow spaces in the beginning of next component.{-
For linear pseudo-Boolean instances, <term> is defined as
<term>::=<variablename>
For non-linear instances, <term> is defined as
<term>::= <oneOrMoreLiterals>
-}term ::C e s m =>m Term term :: forall e s (m :: * -> *). C e s m => m Term
term =m Term
forall e s (m :: * -> *). C e s m => m Term
oneOrMoreLiterals -- <oneOrMoreLiterals>::= <literal> | <literal> <oneOrMoreSpace> <oneOrMoreLiterals>oneOrMoreLiterals ::C e s m =>m [Lit ]oneOrMoreLiterals :: forall e s (m :: * -> *). C e s m => m Term
oneOrMoreLiterals =doInt
l <-m Int
forall e s (m :: * -> *). C e s m => m Int
literal m Term -> m Term -> m Term
forall a. m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus(m Term -> m Term
forall a. m a -> m a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try(m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$m ()
forall e s (m :: * -> *). C e s m => m ()
oneOrMoreSpace m () -> m Term -> m Term
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>(Term -> Term) -> m Term -> m Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM(Int
l Int -> Term -> Term
forall a. a -> [a] -> [a]
:)m Term
forall e s (m :: * -> *). C e s m => m Term
oneOrMoreLiterals )(Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return[Int
l ])-- Note that we cannot use sepBy1.-- In "p `sepBy1` q", p should success whenever q success.-- But it's not the case here.-- <literal>::= <variablename> | "~"<variablename>literal ::C e s m =>m Lit literal :: forall e s (m :: * -> *). C e s m => m Int
literal =m Int
forall e s (m :: * -> *). C e s m => m Int
variablename m Int -> m Int -> m Int
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>(Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
'~'m Word8 -> m Int -> m Int
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>(Int -> Int) -> m Int -> m Int
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftMInt -> Int
forall a. Num a => a -> a
negatem Int
forall e s (m :: * -> *). C e s m => m Int
variablename )
#if MIN_VERSION_megaparsec(7,0,0)
typeParseError =MP.ParseErrorBundleBL.ByteStringVoid
#elif MIN_VERSION_megaparsec(6,0,0)
typeParseError=MP.ParseErrorWord8Void
#elif MIN_VERSION_megaparsec(5,0,0)
typeParseError=MP.ParseErrorCharDec
#else
typeParseError=MP.ParseError
#endif
-- | Parse a OPB format string containing pseudo boolean problem.parseOPBString ::String->String->EitherParseError Formula
#if MIN_VERSION_megaparsec(6,0,0)
parseOPBString :: String -> String -> Either ParseError Formula
parseOPBString String
info String
s =Parsec Void ByteString Formula
-> String -> ByteString -> Either ParseError Formula
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse(Parsec Void ByteString Formula
forall e s (m :: * -> *). C e s m => m Formula
formula Parsec Void ByteString Formula
-> ParsecT Void ByteString Identity ()
-> Parsec Void ByteString Formula
forall a b.
ParsecT Void ByteString Identity a
-> ParsecT Void ByteString Identity b
-> ParsecT Void ByteString Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*ParsecT Void ByteString Identity ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)String
info (String -> ByteString
BL.packString
s )
#else
parseOPBString=parse(formula<*eof)
#endif
-- | Parse a OPB format lazy bytestring containing pseudo boolean problem.parseOPBByteString ::String->ByteString->EitherParseError Formula parseOPBByteString :: String -> ByteString -> Either ParseError Formula
parseOPBByteString =Parsec Void ByteString Formula
-> String -> ByteString -> Either ParseError Formula
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse(Parsec Void ByteString Formula
forall e s (m :: * -> *). C e s m => m Formula
formula Parsec Void ByteString Formula
-> ParsecT Void ByteString Identity ()
-> Parsec Void ByteString Formula
forall a b.
ParsecT Void ByteString Identity a
-> ParsecT Void ByteString Identity b
-> ParsecT Void ByteString Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*ParsecT Void ByteString Identity ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)-- | Parse a OPB file containing pseudo boolean problem.parseOPBFile ::FilePath->IO(EitherParseError Formula )parseOPBFile :: String -> IO (Either ParseError Formula)
parseOPBFile String
filepath =doByteString
s <-String -> IO ByteString
BL.readFileString
filepath Either ParseError Formula -> IO (Either ParseError Formula)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return(Either ParseError Formula -> IO (Either ParseError Formula))
-> Either ParseError Formula -> IO (Either ParseError Formula)
forall a b. (a -> b) -> a -> b
$!Parsec Void ByteString Formula
-> String -> ByteString -> Either ParseError Formula
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse(Parsec Void ByteString Formula
forall e s (m :: * -> *). C e s m => m Formula
formula Parsec Void ByteString Formula
-> ParsecT Void ByteString Identity ()
-> Parsec Void ByteString Formula
forall a b.
ParsecT Void ByteString Identity a
-> ParsecT Void ByteString Identity b
-> ParsecT Void ByteString Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*ParsecT Void ByteString Identity ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)String
filepath ByteString
s -- <softformula>::= <sequence_of_comments> <softheader> <sequence_of_comments_or_constraints>softformula ::C e s m =>m SoftFormula softformula :: forall e s (m :: * -> *). C e s m => m SoftFormula
softformula =doMaybe (Int, Int)
h <-m (Int, Int) -> m (Maybe (Int, Int))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optionalm (Int, Int)
forall e s (m :: * -> *). C e s m => m (Int, Int)
hint m ()
forall e s (m :: * -> *). C e s m => m ()
sequence_of_comments Maybe Integer
top <-m (Maybe Integer)
forall e s (m :: * -> *). C e s m => m (Maybe Integer)
softheader [SoftConstraint]
cs <-m [SoftConstraint]
forall e s (m :: * -> *). C e s m => m [SoftConstraint]
wbo_sequence_of_comments_or_constraints SoftFormula -> m SoftFormula
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(SoftFormula -> m SoftFormula) -> SoftFormula -> m SoftFormula
forall a b. (a -> b) -> a -> b
$SoftFormula {wboTopCost :: Maybe Integer
wboTopCost =Maybe Integer
top ,wboConstraints :: [SoftConstraint]
wboConstraints =[SoftConstraint]
cs ,wboNumVars :: Int
wboNumVars =Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe([SoftConstraint] -> Int
wboComputeNumVars [SoftConstraint]
cs )(((Int, Int) -> Int) -> Maybe (Int, Int) -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap(Int, Int) -> Int
forall a b. (a, b) -> a
fstMaybe (Int, Int)
h ),wboNumConstraints :: Int
wboNumConstraints =Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe([SoftConstraint] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length[SoftConstraint]
cs )(((Int, Int) -> Int) -> Maybe (Int, Int) -> Maybe Int
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap(Int, Int) -> Int
forall a b. (a, b) -> b
sndMaybe (Int, Int)
h )}-- <softheader>::= "soft:" [<unsigned_integer>] ";"softheader ::C e s m =>m (MaybeInteger)=doTokens s
_<-Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
stringTokens s
"soft:"m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace -- XXXMaybe Integer
top <-m Integer -> m (Maybe Integer)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optionalm Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace -- XXXm ()
forall e s (m :: * -> *). C e s m => m ()
semi Maybe Integer -> m (Maybe Integer)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
returnMaybe Integer
top -- <sequence_of_comments_or_constraints>::= <comment_or_constraint> [<sequence_of_comments_or_constraints>]wbo_sequence_of_comments_or_constraints ::C e s m =>m [SoftConstraint ]=do[Maybe SoftConstraint]
xs <-m (Maybe SoftConstraint) -> m [Maybe SoftConstraint]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
manym (Maybe SoftConstraint)
forall e s (m :: * -> *). C e s m => m (Maybe SoftConstraint)
wbo_comment_or_constraint -- XXX: we relax the grammer to allow empty sequence[SoftConstraint] -> m [SoftConstraint]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return([SoftConstraint] -> m [SoftConstraint])
-> [SoftConstraint] -> m [SoftConstraint]
forall a b. (a -> b) -> a -> b
$[Maybe SoftConstraint] -> [SoftConstraint]
forall a. [Maybe a] -> [a]
catMaybes[Maybe SoftConstraint]
xs -- <comment_or_constraint>::= <comment>|<constraint>|<softconstraint>wbo_comment_or_constraint ::C e s m =>m (MaybeSoftConstraint )=(m ()
forall e s (m :: * -> *). C e s m => m ()
comment m () -> m (Maybe SoftConstraint) -> m (Maybe SoftConstraint)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>Maybe SoftConstraint -> m (Maybe SoftConstraint)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
returnMaybe SoftConstraint
forall a. Maybe a
Nothing)m (Maybe SoftConstraint)
-> m (Maybe SoftConstraint) -> m (Maybe SoftConstraint)
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>m (Maybe SoftConstraint)
m wherem :: m (Maybe SoftConstraint)
m =(SoftConstraint -> Maybe SoftConstraint)
-> m SoftConstraint -> m (Maybe SoftConstraint)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftMSoftConstraint -> Maybe SoftConstraint
forall a. a -> Maybe a
Just(m SoftConstraint -> m (Maybe SoftConstraint))
-> m SoftConstraint -> m (Maybe SoftConstraint)
forall a b. (a -> b) -> a -> b
$(m Constraint
forall e s (m :: * -> *). C e s m => m Constraint
constraint m Constraint
-> (Constraint -> m SoftConstraint) -> m SoftConstraint
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=\Constraint
c ->SoftConstraint -> m SoftConstraint
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Maybe Integer
forall a. Maybe a
Nothing,Constraint
c ))m SoftConstraint -> m SoftConstraint -> m SoftConstraint
forall a. m a -> m a -> m a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>m SoftConstraint
forall e s (m :: * -> *). C e s m => m SoftConstraint
softconstraint -- <softconstraint>::= "[" <zeroOrMoreSpace> <unsigned_integer> <zeroOrMoreSpace> "]" <constraint>softconstraint ::C e s m =>m SoftConstraint softconstraint :: forall e s (m :: * -> *). C e s m => m SoftConstraint
softconstraint =doWord8
_<-Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
'['m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace Integer
cost <-m Integer
forall e s (m :: * -> *). C e s m => m Integer
unsigned_integer m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace Word8
_<-Char -> m Word8
forall e s (m :: * -> *). C e s m => Char -> m Word8
char8 Char
']'m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace -- XXXConstraint
c <-m Constraint
forall e s (m :: * -> *). C e s m => m Constraint
constraint SoftConstraint -> m SoftConstraint
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return(Integer -> Maybe Integer
forall a. a -> Maybe a
JustInteger
cost ,Constraint
c )-- | Parse a WBO format string containing weighted boolean optimization problem.parseWBOString ::String->String->EitherParseError SoftFormula
#if MIN_VERSION_megaparsec(6,0,0)
parseWBOString :: String -> String -> Either ParseError SoftFormula
parseWBOString String
info String
s =Parsec Void ByteString SoftFormula
-> String -> ByteString -> Either ParseError SoftFormula
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse(Parsec Void ByteString SoftFormula
forall e s (m :: * -> *). C e s m => m SoftFormula
softformula Parsec Void ByteString SoftFormula
-> ParsecT Void ByteString Identity ()
-> Parsec Void ByteString SoftFormula
forall a b.
ParsecT Void ByteString Identity a
-> ParsecT Void ByteString Identity b
-> ParsecT Void ByteString Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*ParsecT Void ByteString Identity ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)String
info (String -> ByteString
BL.packString
s )
#else
parseWBOString=parse(softformula<*eof)
#endif
-- | Parse a WBO format lazy bytestring containing pseudo boolean problem.parseWBOByteString ::String->ByteString->EitherParseError SoftFormula parseWBOByteString :: String -> ByteString -> Either ParseError SoftFormula
parseWBOByteString =Parsec Void ByteString SoftFormula
-> String -> ByteString -> Either ParseError SoftFormula
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse(Parsec Void ByteString SoftFormula
forall e s (m :: * -> *). C e s m => m SoftFormula
softformula Parsec Void ByteString SoftFormula
-> ParsecT Void ByteString Identity ()
-> Parsec Void ByteString SoftFormula
forall a b.
ParsecT Void ByteString Identity a
-> ParsecT Void ByteString Identity b
-> ParsecT Void ByteString Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*ParsecT Void ByteString Identity ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)-- | Parse a WBO file containing weighted boolean optimization problem.parseWBOFile ::FilePath->IO(EitherParseError SoftFormula )parseWBOFile :: String -> IO (Either ParseError SoftFormula)
parseWBOFile String
filepath =doByteString
s <-String -> IO ByteString
BL.readFileString
filepath Either ParseError SoftFormula -> IO (Either ParseError SoftFormula)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return(Either ParseError SoftFormula
-> IO (Either ParseError SoftFormula))
-> Either ParseError SoftFormula
-> IO (Either ParseError SoftFormula)
forall a b. (a -> b) -> a -> b
$!Parsec Void ByteString SoftFormula
-> String -> ByteString -> Either ParseError SoftFormula
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse(Parsec Void ByteString SoftFormula
forall e s (m :: * -> *). C e s m => m SoftFormula
softformula Parsec Void ByteString SoftFormula
-> ParsecT Void ByteString Identity ()
-> Parsec Void ByteString SoftFormula
forall a b.
ParsecT Void ByteString Identity a
-> ParsecT Void ByteString Identity b
-> ParsecT Void ByteString Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*ParsecT Void ByteString Identity ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)String
filepath ByteString
s