{-# LANGUAGE BangPatterns, OverloadedStrings #-}
{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.PseudoBoolean.Attoparsec
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Portability :  non-portable (BangPatterns, OverloadedStrings)
--
-- A parser library for 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>
--
-----------------------------------------------------------------------------

module Data.PseudoBoolean.Attoparsec
  (
  -- * Parsing OPB files
    opbParser
  , parseOPBByteString
  , parseOPBFile

  -- * Parsing WBO files
  , wboParser
  , parseWBOByteString
  , parseWBOFile
  ) where

import Prelude hiding (sum)
import Control.Applicative ((<|>), (<*))
import Control.Monad
import Data.Attoparsec.ByteString.Char8 hiding (isDigit)
import qualified Data.Attoparsec.ByteString.Lazy as L
import qualified Data.ByteString.Char8 as BS
import qualified Data.ByteString.Lazy as BSLazy
import Data.Char
import Data.Maybe
import Data.PseudoBoolean.Types
import Data.PseudoBoolean.Internal.TextUtil

-- | Parser for OPB files
opbParser :: Parser Formula
opbParser :: Parser Formula
opbParser = Parser Formula
formula

-- | Parser for WBO files
wboParser :: Parser SoftFormula
wboParser :: Parser SoftFormula
wboParser = Parser SoftFormula
softformula

-- <formula>::= <sequence_of_comments> [<objective>] <sequence_of_comments_or_constraints>
formula :: Parser Formula
formula :: Parser Formula
formula = do
  Maybe (Var, Var)
h <- Parser (Var, Var) -> Parser (Maybe (Var, Var))
forall a. Parser a -> Parser (Maybe a)
optionMaybe Parser (Var, Var)
hint
  Parser ()
sequence_of_comments
  Maybe Sum
obj <- Parser Sum -> Parser (Maybe Sum)
forall a. Parser a -> Parser (Maybe a)
optionMaybe Parser Sum
objective
  [Constraint]
cs <- Parser [Constraint]
sequence_of_comments_or_constraints
  Formula -> Parser Formula
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> Parser Formula) -> Formula -> Parser Formula
forall a b. (a -> b) -> a -> b
$
    Formula
    { pbObjectiveFunction :: Maybe Sum
pbObjectiveFunction = Maybe Sum
obj
    , pbConstraints :: [Constraint]
pbConstraints = [Constraint]
cs
    , pbNumVars :: Var
pbNumVars = Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
fromMaybe (Maybe Sum -> [Constraint] -> Var
pbComputeNumVars Maybe Sum
obj [Constraint]
cs) (((Var, Var) -> Var) -> Maybe (Var, Var) -> Maybe Var
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var, Var) -> Var
forall a b. (a, b) -> a
fst Maybe (Var, Var)
h)
    , pbNumConstraints :: Var
pbNumConstraints = Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
fromMaybe ([Constraint] -> Var
forall a. [a] -> Var
forall (t :: * -> *) a. Foldable t => t a -> Var
length [Constraint]
cs) (((Var, Var) -> Var) -> Maybe (Var, Var) -> Maybe Var
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var, Var) -> Var
forall a b. (a, b) -> b
snd Maybe (Var, Var)
h)
    }

hint :: Parser (Int,Int)
hint :: Parser (Var, Var)
hint = Parser (Var, Var) -> Parser (Var, Var)
forall i a. Parser i a -> Parser i a
try (Parser (Var, Var) -> Parser (Var, Var))
-> Parser (Var, Var) -> Parser (Var, Var)
forall a b. (a -> b) -> a -> b
$ do
  Char
_ <- Char -> Parser Char
char Char
'*'
  Parser ()
zeroOrMoreSpace
  ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"#variable="
  Parser ()
zeroOrMoreSpace
  Integer
nv <- Parser Integer
unsigned_integer
  Parser ()
oneOrMoreSpace  
  ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"#constraint="
  Parser ()
zeroOrMoreSpace
  Integer
nc <- Parser Integer
unsigned_integer
  [Char]
_ <- Parser Char -> Parser () -> Parser ByteString [Char]
forall (f :: * -> *) a b. Alternative f => f a -> f b -> f [a]
manyTill Parser Char
anyChar Parser ()
eol
  (Var, Var) -> Parser (Var, Var)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Var
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
nv, Integer -> Var
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
nc)

-- <sequence_of_comments>::= <comment> [<sequence_of_comments>]
sequence_of_comments :: Parser ()
sequence_of_comments :: Parser ()
sequence_of_comments = Parser () -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f ()
skipMany Parser ()
comment -- XXX: we allow empty sequence

-- <comment>::= "*" <any_sequence_of_characters_other_than_EOL> <EOL>
comment :: Parser ()
comment :: Parser ()
comment = do
  Char
_ <- Char -> Parser Char
char Char
'*' 
  [Char]
_ <- Parser Char -> Parser () -> Parser ByteString [Char]
forall (f :: * -> *) a b. Alternative f => f a -> f b -> f [a]
manyTill Parser Char
anyChar Parser ()
eol
  Parser Char -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f ()
skipMany Parser Char
space -- We relax the grammer and allow spaces in the beggining of next component.
  () -> Parser ()
forall a. a -> Parser ByteString 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 :: Parser [Constraint]
sequence_of_comments_or_constraints :: Parser [Constraint]
sequence_of_comments_or_constraints = do
  [Maybe Constraint]
xs <- Parser ByteString (Maybe Constraint)
-> Parser ByteString [Maybe Constraint]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many' Parser ByteString (Maybe Constraint)
comment_or_constraint -- XXX: we relax the grammer to allow empty sequence
  [Constraint] -> Parser [Constraint]
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> Parser [Constraint])
-> [Constraint] -> Parser [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 :: Parser (Maybe Constraint)
comment_or_constraint :: Parser ByteString (Maybe Constraint)
comment_or_constraint =
  (Parser ()
comment Parser ()
-> Parser ByteString (Maybe Constraint)
-> Parser ByteString (Maybe Constraint)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Constraint -> Parser ByteString (Maybe Constraint)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Constraint
forall a. Maybe a
Nothing) Parser ByteString (Maybe Constraint)
-> Parser ByteString (Maybe Constraint)
-> Parser ByteString (Maybe Constraint)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Constraint -> Maybe Constraint)
-> Parser ByteString Constraint
-> Parser ByteString (Maybe Constraint)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just Parser ByteString Constraint
constraint)

-- <objective>::= "min:" <zeroOrMoreSpace> <sum> ";"
objective :: Parser Sum
objective :: Parser Sum
objective = do
  ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"min:"
  Parser ()
zeroOrMoreSpace
  Sum
obj <- Parser Sum
sum
  Parser ()
semi
  Sum -> Parser Sum
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Sum
obj

-- <constraint>::= <sum> <relational_operator> <zeroOrMoreSpace> <integer> <zeroOrMoreSpace> ";"
constraint :: Parser Constraint
constraint :: Parser ByteString Constraint
constraint = do
  Sum
lhs <- Parser Sum
sum
  Op
op <- Parser Op
relational_operator
  Parser ()
zeroOrMoreSpace
  Integer
rhs <- Parser Integer
integer
  Parser ()
zeroOrMoreSpace
  Parser ()
semi
  Constraint -> Parser ByteString Constraint
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Sum
lhs, Op
op, Integer
rhs)

-- <sum>::= <weightedterm> | <weightedterm> <sum>
sum :: Parser Sum
sum :: Parser Sum
sum = Parser ByteString WeightedTerm -> Parser Sum
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many' Parser ByteString WeightedTerm
weightedterm -- we relax the grammer to allow empty sum

-- <weightedterm>::= <integer> <oneOrMoreSpace> <term> <oneOrMoreSpace>
weightedterm :: Parser WeightedTerm
weightedterm :: Parser ByteString WeightedTerm
weightedterm = do
  Integer
w <- Parser Integer
integer
  Parser ()
oneOrMoreSpace
  Term
t <- Parser Term
term
  Parser ()
zeroOrMoreSpace -- we relax the grammar to allow omitting spaces at the end of <sum>.
  WeightedTerm -> Parser ByteString WeightedTerm
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer
w,Term
t)

-- <integer>::= <unsigned_integer> | "+" <unsigned_integer> | "-" <unsigned_integer>
integer :: Parser Integer
integer :: Parser Integer
integer = [Parser Integer] -> Parser Integer
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
  [ Parser Integer
unsigned_integer
  , Char -> Parser Char
char Char
'+' Parser Char -> Parser Integer -> Parser Integer
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Integer
unsigned_integer
  , Char -> Parser Char
char Char
'-' Parser Char -> Parser Integer -> Parser Integer
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Integer -> Integer) -> Parser Integer -> Parser Integer
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Integer -> Integer
forall a. Num a => a -> a
negate Parser Integer
unsigned_integer
  ]

-- <unsigned_integer>::= <digit> | <digit><unsigned_integer>
unsigned_integer :: Parser Integer
unsigned_integer :: Parser Integer
unsigned_integer = do
  ByteString
ds <- (Char -> Bool) -> Parser ByteString
takeWhile1 Char -> Bool
isDigit
  Integer -> Parser Integer
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Parser Integer) -> Integer -> Parser Integer
forall a b. (a -> b) -> a -> b
$! [Char] -> Integer
readUnsignedInteger ([Char] -> Integer) -> [Char] -> Integer
forall a b. (a -> b) -> a -> b
$ ByteString -> [Char]
BS.unpack ByteString
ds

-- <relational_operator>::= ">=" | "="
relational_operator :: Parser Op
relational_operator :: Parser Op
relational_operator = (ByteString -> Parser ByteString
string ByteString
">=" Parser ByteString -> Parser Op -> Parser Op
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Op -> Parser Op
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Op
Ge) Parser Op -> Parser Op -> Parser Op
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ByteString -> Parser ByteString
string ByteString
"=" Parser ByteString -> Parser Op -> Parser Op
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Op -> Parser Op
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Op
Eq)

-- <variablename>::= "x" <unsigned_integer>
variablename :: Parser Var
variablename :: Parser Var
variablename = do
  Char
_ <- Char -> Parser Char
char Char
'x'
  Integer
i <- Parser Integer
unsigned_integer
  Var -> Parser Var
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Parser Var) -> Var -> Parser Var
forall a b. (a -> b) -> a -> b
$! Integer -> Var
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i

-- <oneOrMoreSpace>::= " " [<oneOrMoreSpace>]
oneOrMoreSpace :: Parser ()
oneOrMoreSpace :: Parser ()
oneOrMoreSpace  = Parser Char -> Parser ()
forall (f :: * -> *) a. Alternative f => f a -> f ()
skipMany1 (Char -> Parser Char
char Char
' ')

-- <zeroOrMoreSpace>::= [" " <zeroOrMoreSpace>]
zeroOrMoreSpace :: Parser ()
-- zeroOrMoreSpace = skipMany (char ' ')
zeroOrMoreSpace :: Parser ()
zeroOrMoreSpace = Parser ()
skipSpace
-- We relax the grammer and allow more type of spacing

eol :: Parser ()
eol :: Parser ()
eol = Char -> Parser Char
char Char
'\n' Parser Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> Parser ()
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

semi :: Parser ()
semi :: Parser ()
semi = Char -> Parser Char
char Char
';' Parser Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
-- 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 :: Parser Term
term :: Parser Term
term = Parser Term
oneOrMoreLiterals

-- <oneOrMoreLiterals>::= <literal> | <literal> <oneOrMoreSpace> <oneOrMoreLiterals>
oneOrMoreLiterals :: Parser [Lit]
oneOrMoreLiterals :: Parser Term
oneOrMoreLiterals = do
  Var
l <- Parser Var
literal
  Parser Term -> Parser Term -> Parser Term
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (Parser Term -> Parser Term
forall i a. Parser i a -> Parser i a
try (Parser Term -> Parser Term) -> Parser Term -> Parser Term
forall a b. (a -> b) -> a -> b
$ Parser ()
oneOrMoreSpace Parser () -> Parser Term -> Parser Term
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term) -> Parser Term -> Parser Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Var
lVar -> Term -> Term
forall a. a -> [a] -> [a]
:) Parser Term
oneOrMoreLiterals) (Term -> Parser Term
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return [Var
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 :: Parser Lit
literal :: Parser Var
literal = Parser Var
variablename Parser Var -> Parser Var -> Parser Var
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Char -> Parser Char
char Char
'~' Parser Char -> Parser Var -> Parser Var
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Var -> Var) -> Parser Var -> Parser Var
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Var -> Var
forall a. Num a => a -> a
negate Parser Var
variablename)

-- | Parse a OPB format string containing pseudo boolean problem.
parseOPBByteString :: BSLazy.ByteString -> Either String Formula
parseOPBByteString :: ByteString -> Either [Char] Formula
parseOPBByteString ByteString
s = Result Formula -> Either [Char] Formula
forall r. Result r -> Either [Char] r
L.eitherResult (Result Formula -> Either [Char] Formula)
-> Result Formula -> Either [Char] Formula
forall a b. (a -> b) -> a -> b
$ Parser Formula -> ByteString -> Result Formula
forall a. Parser a -> ByteString -> Result a
L.parse (Parser Formula
formula Parser Formula -> Parser () -> Parser Formula
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall t. Chunk t => Parser t ()
endOfInput) ByteString
s

-- | Parse a OPB file containing pseudo boolean problem.
parseOPBFile :: FilePath -> IO (Either String Formula)
parseOPBFile :: [Char] -> IO (Either [Char] Formula)
parseOPBFile [Char]
fname = do
  ByteString
s <- [Char] -> IO ByteString
BSLazy.readFile [Char]
fname
  Either [Char] Formula -> IO (Either [Char] Formula)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [Char] Formula -> IO (Either [Char] Formula))
-> Either [Char] Formula -> IO (Either [Char] Formula)
forall a b. (a -> b) -> a -> b
$ ByteString -> Either [Char] Formula
parseOPBByteString ByteString
s

-- <softformula>::= <sequence_of_comments> <softheader> <sequence_of_comments_or_constraints>
softformula :: Parser SoftFormula
softformula :: Parser SoftFormula
softformula = do
  Maybe (Var, Var)
h <- Parser (Var, Var) -> Parser (Maybe (Var, Var))
forall a. Parser a -> Parser (Maybe a)
optionMaybe Parser (Var, Var)
hint
  Parser ()
sequence_of_comments
  Maybe Integer
top <- Parser (Maybe Integer)
softheader
  [SoftConstraint]
cs <- Parser [SoftConstraint]
wbo_sequence_of_comments_or_constraints
  SoftFormula -> Parser SoftFormula
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (SoftFormula -> Parser SoftFormula)
-> SoftFormula -> Parser SoftFormula
forall a b. (a -> b) -> a -> b
$
    SoftFormula
    { wboTopCost :: Maybe Integer
wboTopCost = Maybe Integer
top
    , wboConstraints :: [SoftConstraint]
wboConstraints = [SoftConstraint]
cs
    , wboNumVars :: Var
wboNumVars = Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
fromMaybe ([SoftConstraint] -> Var
wboComputeNumVars [SoftConstraint]
cs) (((Var, Var) -> Var) -> Maybe (Var, Var) -> Maybe Var
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var, Var) -> Var
forall a b. (a, b) -> a
fst Maybe (Var, Var)
h)
    , wboNumConstraints :: Var
wboNumConstraints = Var -> Maybe Var -> Var
forall a. a -> Maybe a -> a
fromMaybe ([SoftConstraint] -> Var
forall a. [a] -> Var
forall (t :: * -> *) a. Foldable t => t a -> Var
length [SoftConstraint]
cs) (((Var, Var) -> Var) -> Maybe (Var, Var) -> Maybe Var
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Var, Var) -> Var
forall a b. (a, b) -> b
snd Maybe (Var, Var)
h)
    }

-- <softheader>::= "soft:" [<unsigned_integer>] ";"
softheader :: Parser (Maybe Integer)
softheader :: Parser (Maybe Integer)
softheader = do
  ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"soft:"
  Parser ()
zeroOrMoreSpace -- XXX
  Maybe Integer
top <- Parser Integer -> Parser (Maybe Integer)
forall a. Parser a -> Parser (Maybe a)
optionMaybe Parser Integer
unsigned_integer
  Parser ()
zeroOrMoreSpace -- XXX
  Parser ()
semi
  Maybe Integer -> Parser (Maybe Integer)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Integer
top

-- <sequence_of_comments_or_constraints>::= <comment_or_constraint> [<sequence_of_comments_or_constraints>]
wbo_sequence_of_comments_or_constraints :: Parser [SoftConstraint]
wbo_sequence_of_comments_or_constraints :: Parser [SoftConstraint]
wbo_sequence_of_comments_or_constraints = do
  [Maybe SoftConstraint]
xs <- Parser ByteString (Maybe SoftConstraint)
-> Parser ByteString [Maybe SoftConstraint]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many' Parser ByteString (Maybe SoftConstraint)
wbo_comment_or_constraint -- We relax the grammer and allow spaces in the beginning of next component.
  [SoftConstraint] -> Parser [SoftConstraint]
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return ([SoftConstraint] -> Parser [SoftConstraint])
-> [SoftConstraint] -> Parser [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 :: Parser (Maybe SoftConstraint)
wbo_comment_or_constraint :: Parser ByteString (Maybe SoftConstraint)
wbo_comment_or_constraint = (Parser ()
comment Parser ()
-> Parser ByteString (Maybe SoftConstraint)
-> Parser ByteString (Maybe SoftConstraint)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe SoftConstraint -> Parser ByteString (Maybe SoftConstraint)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SoftConstraint
forall a. Maybe a
Nothing) Parser ByteString (Maybe SoftConstraint)
-> Parser ByteString (Maybe SoftConstraint)
-> Parser ByteString (Maybe SoftConstraint)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ByteString (Maybe SoftConstraint)
m
  where
    m :: Parser ByteString (Maybe SoftConstraint)
m = (SoftConstraint -> Maybe SoftConstraint)
-> Parser ByteString SoftConstraint
-> Parser ByteString (Maybe SoftConstraint)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SoftConstraint -> Maybe SoftConstraint
forall a. a -> Maybe a
Just (Parser ByteString SoftConstraint
 -> Parser ByteString (Maybe SoftConstraint))
-> Parser ByteString SoftConstraint
-> Parser ByteString (Maybe SoftConstraint)
forall a b. (a -> b) -> a -> b
$ (Parser ByteString Constraint
constraint Parser ByteString Constraint
-> (Constraint -> Parser ByteString SoftConstraint)
-> Parser ByteString SoftConstraint
forall a b.
Parser ByteString a
-> (a -> Parser ByteString b) -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Constraint
c -> SoftConstraint -> Parser ByteString SoftConstraint
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
forall a. Maybe a
Nothing, Constraint
c)) Parser ByteString SoftConstraint
-> Parser ByteString SoftConstraint
-> Parser ByteString SoftConstraint
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ByteString SoftConstraint
softconstraint

-- <softconstraint>::= "[" <zeroOrMoreSpace> <unsigned_integer> <zeroOrMoreSpace> "]" <constraint>
softconstraint :: Parser SoftConstraint
softconstraint :: Parser ByteString SoftConstraint
softconstraint = do
  Char
_ <- Char -> Parser Char
char Char
'['
  Parser ()
zeroOrMoreSpace
  Integer
cost <- Parser Integer
unsigned_integer
  Parser ()
zeroOrMoreSpace
  Char
_ <- Char -> Parser Char
char Char
']'
  Parser ()
zeroOrMoreSpace -- XXX
  Constraint
c <- Parser ByteString Constraint
constraint
  SoftConstraint -> Parser ByteString SoftConstraint
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
cost, Constraint
c)

-- | Parse a WBO format string containing weighted boolean optimization problem.
parseWBOByteString :: BSLazy.ByteString -> Either String SoftFormula
parseWBOByteString :: ByteString -> Either [Char] SoftFormula
parseWBOByteString ByteString
s = Result SoftFormula -> Either [Char] SoftFormula
forall r. Result r -> Either [Char] r
L.eitherResult (Result SoftFormula -> Either [Char] SoftFormula)
-> Result SoftFormula -> Either [Char] SoftFormula
forall a b. (a -> b) -> a -> b
$ Parser SoftFormula -> ByteString -> Result SoftFormula
forall a. Parser a -> ByteString -> Result a
L.parse (Parser SoftFormula
softformula Parser SoftFormula -> Parser () -> Parser SoftFormula
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall t. Chunk t => Parser t ()
endOfInput) ByteString
s

-- | Parse a WBO file containing weighted boolean optimization problem.
parseWBOFile :: FilePath -> IO (Either String SoftFormula)
parseWBOFile :: [Char] -> IO (Either [Char] SoftFormula)
parseWBOFile [Char]
fname = do
  ByteString
s <- [Char] -> IO ByteString
BSLazy.readFile [Char]
fname
  Either [Char] SoftFormula -> IO (Either [Char] SoftFormula)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either [Char] SoftFormula -> IO (Either [Char] SoftFormula))
-> Either [Char] SoftFormula -> IO (Either [Char] SoftFormula)
forall a b. (a -> b) -> a -> b
$ ByteString -> Either [Char] SoftFormula
parseWBOByteString ByteString
s

optionMaybe :: Parser a -> Parser (Maybe a)
optionMaybe :: forall a. Parser a -> Parser (Maybe a)
optionMaybe Parser a
p = Maybe a
-> Parser ByteString (Maybe a) -> Parser ByteString (Maybe a)
forall (f :: * -> *) a. Alternative f => a -> f a -> f a
option Maybe a
forall a. Maybe a
Nothing ((a -> Maybe a) -> Parser a -> Parser ByteString (Maybe a)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM a -> Maybe a
forall a. a -> Maybe a
Just Parser a
p)