module Data.PseudoBoolean.Megaparsec
(
opbParser
, parseOPBString
, parseOPBByteString
, parseOPBFile
, wboParser
, parseWBOString
, parseWBOByteString
, parseWBOFile
) where
import Prelude hiding (sum)
import Control.Applicative ((<*))
import Control.Monad
import Data.ByteString.Lazy (ByteString)
import qualified Data.ByteString.Lazy as BL
import Data.Maybe
import Text.Megaparsec
import Text.Megaparsec.Prim (MonadParsec ())
import Data.PseudoBoolean.Types
import Data.PseudoBoolean.Internal.TextUtil
#if MIN_VERSION_megaparsec(5,0,0)
type C e s m = (MonadParsec e s m, Token s ~ Char)
#else
type C e s m = (MonadParsec s m Char)
#endif
#if MIN_VERSION_megaparsec(5,0,0)
opbParser :: (MonadParsec e s m, Token s ~ Char) => m Formula
#else
opbParser :: (MonadParsec s m Char) => m Formula
#endif
opbParser = formula
#if MIN_VERSION_megaparsec(5,0,0)
wboParser :: (MonadParsec e s m, Token s ~ Char) => m SoftFormula
#else
wboParser :: (MonadParsec s m Char) => m SoftFormula
#endif
wboParser = softformula
formula :: C e s m => m Formula
formula = do
h <- optional hint
sequence_of_comments
obj <- optional objective
cs <- sequence_of_comments_or_constraints
return $
Formula
{ pbObjectiveFunction = obj
, pbConstraints = cs
, pbNumVars = fromMaybe (pbComputeNumVars obj cs) (fmap fst h)
, pbNumConstraints = fromMaybe (length cs) (fmap snd h)
}
hint :: C e s m => m (Int,Int)
hint = try $ do
_ <- char '*'
zeroOrMoreSpace
_ <- string "#variable="
zeroOrMoreSpace
nv <- unsigned_integer
oneOrMoreSpace
_ <- string "#constraint="
zeroOrMoreSpace
nc <- unsigned_integer
_ <- manyTill anyChar eol
return (fromIntegral nv, fromIntegral nc)
sequence_of_comments :: C e s m => m ()
sequence_of_comments = skipMany comment
comment :: C e s m => m ()
comment = do
_ <- char '*'
_ <- manyTill anyChar eol
space
return ()
sequence_of_comments_or_constraints :: C e s m => m [Constraint]
sequence_of_comments_or_constraints = do
xs <- many comment_or_constraint
return $ catMaybes xs
comment_or_constraint :: C e s m => m (Maybe Constraint)
comment_or_constraint =
(comment >> return Nothing) <|> (liftM Just constraint)
objective :: C e s m => m Sum
objective = do
_ <- string "min:"
zeroOrMoreSpace
obj <- sum
semi
return obj
constraint :: C e s m => m Constraint
constraint = do
lhs <- sum
op <- relational_operator
zeroOrMoreSpace
rhs <- integer
zeroOrMoreSpace
semi
return (lhs, op, rhs)
sum :: C e s m => m Sum
sum = some weightedterm
weightedterm :: C e s m => m WeightedTerm
weightedterm = do
w <- integer
oneOrMoreSpace
t <- term
zeroOrMoreSpace
return (w,t)
integer :: C e s m => m Integer
integer = msum
[ unsigned_integer
, char '+' >> unsigned_integer
, char '-' >> liftM negate unsigned_integer
]
unsigned_integer :: C e s m => m Integer
unsigned_integer = do
ds <- some digitChar
return $! readUnsignedInteger ds
relational_operator :: C e s m => m Op
relational_operator = (string ">=" >> return Ge) <|> (string "=" >> return Eq)
variablename :: C e s m => m Var
variablename = do
_ <- char 'x'
i <- unsigned_integer
return $! fromIntegral i
oneOrMoreSpace :: C e s m => m ()
oneOrMoreSpace = skipSome (char ' ')
zeroOrMoreSpace :: C e s m => m ()
zeroOrMoreSpace = space
semi :: C e s m => m ()
semi = char ';' >> space
term :: C e s m => m Term
term = oneOrMoreLiterals
oneOrMoreLiterals :: C e s m => m [Lit]
oneOrMoreLiterals = do
l <- literal
mplus (try $ oneOrMoreSpace >> liftM (l:) (oneOrMoreLiterals)) (return [l])
literal :: C e s m => m Lit
literal = variablename <|> (char '~' >> liftM negate variablename)
#if MIN_VERSION_megaparsec(5,0,0)
parseOPBString :: String -> String -> Either (ParseError Char Dec) Formula
#else
parseOPBString :: String -> String -> Either ParseError Formula
#endif
parseOPBString = parse (formula <* eof)
#if MIN_VERSION_megaparsec(5,0,0)
parseOPBByteString :: String -> ByteString -> Either (ParseError Char Dec) Formula
#else
parseOPBByteString :: String -> ByteString -> Either ParseError Formula
#endif
parseOPBByteString = parse (formula <* eof)
#if MIN_VERSION_megaparsec(5,0,0)
parseOPBFile :: FilePath -> IO (Either (ParseError Char Dec) Formula)
#else
parseOPBFile :: FilePath -> IO (Either ParseError Formula)
#endif
parseOPBFile filepath = do
s <- BL.readFile filepath
return $! parse (formula <* eof) filepath s
softformula :: C e s m => m SoftFormula
softformula = do
h <- optional hint
sequence_of_comments
top <- softheader
cs <- wbo_sequence_of_comments_or_constraints
return $
SoftFormula
{ wboTopCost = top
, wboConstraints = cs
, wboNumVars = fromMaybe (wboComputeNumVars cs) (fmap fst h)
, wboNumConstraints = fromMaybe (length cs) (fmap snd h)
}
softheader :: C e s m => m (Maybe Integer)
softheader = do
_ <- string "soft:"
zeroOrMoreSpace
top <- optional unsigned_integer
zeroOrMoreSpace
semi
return top
wbo_sequence_of_comments_or_constraints :: C e s m => m [SoftConstraint]
wbo_sequence_of_comments_or_constraints = do
xs <- many wbo_comment_or_constraint
return $ catMaybes xs
wbo_comment_or_constraint :: C e s m => m (Maybe SoftConstraint)
wbo_comment_or_constraint = (comment >> return Nothing) <|> m
where
m = liftM Just $ (constraint >>= \c -> return (Nothing, c)) <|> softconstraint
softconstraint :: C e s m => m SoftConstraint
softconstraint = do
_ <- char '['
zeroOrMoreSpace
cost <- unsigned_integer
zeroOrMoreSpace
_ <- char ']'
zeroOrMoreSpace
c <- constraint
return (Just cost, c)
#if MIN_VERSION_megaparsec(5,0,0)
parseWBOString :: String -> String -> Either (ParseError Char Dec) SoftFormula
#else
parseWBOString :: String -> String -> Either ParseError SoftFormula
#endif
parseWBOString = parse (softformula <* eof)
#if MIN_VERSION_megaparsec(5,0,0)
parseWBOByteString :: String -> ByteString -> Either (ParseError Char Dec) SoftFormula
#else
parseWBOByteString :: String -> ByteString -> Either ParseError SoftFormula
#endif
parseWBOByteString = parse (softformula <* eof)
#if MIN_VERSION_megaparsec(5,0,0)
parseWBOFile :: FilePath -> IO (Either (ParseError Char Dec) SoftFormula)
#else
parseWBOFile :: FilePath -> IO (Either ParseError SoftFormula)
#endif
parseWBOFile filepath = do
s <- BL.readFile filepath
return $! parse (softformula <* eof) filepath s