{-# 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>
--
-----------------------------------------------------------------------------

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

  -- * Parsing WBO files
  , wboParser
  , parseWBOString
  , parseWBOByteString
  , parseWBOFile

  -- * Error type
  , ParseError
  ) where

import Prelude hiding (sum)
import Control.Applicative ((<*))
import Control.Monad
import Data.ByteString.Lazy (ByteString)
import qualified Data.ByteString.Lazy.Char8 as BL
import Data.Maybe
#if MIN_VERSION_megaparsec(6,0,0)
import Data.String
import Data.Word
import Data.Void
#endif
import Text.Megaparsec hiding (ParseError)
import qualified Text.Megaparsec as MP
#if MIN_VERSION_megaparsec(6,0,0)
import Text.Megaparsec.Byte
#else
import Text.Megaparsec.Prim (MonadParsec ())
#endif
import Data.PseudoBoolean.Types
import Data.PseudoBoolean.Internal.TextUtil

#if MIN_VERSION_megaparsec(6,0,0)

type C e s m = (MonadParsec e s m, Token s ~ Word8, IsString (Tokens s))

char8 :: C e s m => Char -> m Word8
char8 :: 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)
type C e s m = (MonadParsec e s m, Token s ~ Char)
#elif MIN_VERSION_megaparsec(4,4,0)
type C e s m = (MonadParsec s m Char)
#else
type C e s m = (MonadParsec s m Char, MonadPlus m)
#endif

char8 :: C e s m => Char -> m Char
char8 = char

#endif

#if MIN_VERSION_megaparsec(7,0,0)
anyChar :: C e s m => m Word8
anyChar :: 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 :: (MonadParsec e s m, Token s ~ Word8, IsString (Tokens s)) => m Formula
#elif MIN_VERSION_megaparsec(5,0,0)
opbParser :: (MonadParsec e s m, Token s ~ Char) => m Formula
#elif MIN_VERSION_megaparsec(4,4,0)
opbParser :: (MonadParsec s m Char) => m Formula
#else
opbParser :: (MonadParsec s m Char, MonadPlus m) => m Formula
#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 :: (MonadParsec e s m, Token s ~ Word8, IsString (Tokens s)) => m SoftFormula
#elif MIN_VERSION_megaparsec(5,0,0)
wboParser :: (MonadParsec e s m, Token s ~ Char) => m SoftFormula
#elif MIN_VERSION_megaparsec(4,4,0)
wboParser :: (MonadParsec s m Char) => m SoftFormula
#else
wboParser :: (MonadParsec s m Char, MonadPlus m) => m SoftFormula
#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 = do
  Maybe (Int, Int)
h <- m (Int, Int) -> m (Maybe (Int, Int))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional m (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)
optional m 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
fst Maybe (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
snd Maybe (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
$ do
  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
  Tokens s
_ <- Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens 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)
string Tokens 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]
manyTill m 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
fromIntegral Integer
nv, Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
nc)

-- <sequence_of_comments>::= <comment> [<sequence_of_comments>]
sequence_of_comments :: C e s m => m ()
sequence_of_comments :: forall e s (m :: * -> *). C e s m => m ()
sequence_of_comments = m () -> m ()
forall (m :: * -> *) a. MonadPlus m => m a -> m ()
skipMany m ()
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 ()
comment :: forall e s (m :: * -> *). C e s m => m ()
comment = do
  Word8
_ <- 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]
manyTill m 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
  m ()
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]
sequence_of_comments_or_constraints :: forall e s (m :: * -> *). C e s m => m [Constraint]
sequence_of_comments_or_constraints = do
  [Maybe Constraint]
xs <- m (Maybe Constraint) -> m [Maybe Constraint]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many m (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 (Maybe Constraint)
comment_or_constraint :: forall e s (m :: * -> *). C e s m => m (Maybe Constraint)
comment_or_constraint =
  (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
return Maybe 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
liftM Constraint -> Maybe Constraint
forall a. a -> Maybe a
Just m 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 = do
  Tokens s
_ <- Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens 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
return Sum
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 = do
  Sum
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]
many m 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 = do
  Integer
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 Integer
integer :: 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
liftM Integer -> Integer
forall a. Num a => a -> a
negate m 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 Integer
unsigned_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]
some m 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 $! readUnsignedInteger ds
#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)
string Tokens 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
return Op
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)
string Tokens 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
return Op
Eq)

-- <variablename>::= "x" <unsigned_integer>
variablename :: C e s m => m Var
variablename :: forall e s (m :: * -> *). C e s m => m Int
variablename = do
  Word8
_ <- 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
fromIntegral Integer
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 spacing

semi :: 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 = do
  Int
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
lInt -> 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
liftM Int -> Int
forall a. Num a => a -> a
negate m Int
forall e s (m :: * -> *). C e s m => m Int
variablename)

#if MIN_VERSION_megaparsec(7,0,0)
type ParseError = MP.ParseErrorBundle BL.ByteString Void
#elif MIN_VERSION_megaparsec(6,0,0)
type ParseError = MP.ParseError Word8 Void
#elif MIN_VERSION_megaparsec(5,0,0)
type ParseError = MP.ParseError Char Dec
#else
type ParseError = MP.ParseError
#endif

-- | Parse a OPB format string containing pseudo boolean problem.
parseOPBString :: String -> String -> Either ParseError 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.pack String
s)
#else
parseOPBString = parse (formula <* eof)
#endif

-- | Parse a OPB format lazy bytestring containing pseudo boolean problem.
parseOPBByteString :: String -> ByteString -> Either ParseError 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 (Either ParseError Formula)
parseOPBFile :: String -> IO (Either ParseError Formula)
parseOPBFile String
filepath = do
  ByteString
s <- String -> IO ByteString
BL.readFile String
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 = do
  Maybe (Int, Int)
h <- m (Int, Int) -> m (Maybe (Int, Int))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional m (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
fst Maybe (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
snd Maybe (Int, Int)
h)
    }

-- <softheader>::= "soft:" [<unsigned_integer>] ";"
softheader :: C e s m => m (Maybe Integer)
softheader :: forall e s (m :: * -> *). C e s m => m (Maybe Integer)
softheader = do
  Tokens s
_ <- Tokens s -> m (Tokens s)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens s
"soft:"
  m ()
forall e s (m :: * -> *). C e s m => m ()
zeroOrMoreSpace -- XXX
  Maybe Integer
top <- m Integer -> m (Maybe Integer)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional 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 -- XXX
  m ()
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
return Maybe 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]
wbo_sequence_of_comments_or_constraints :: forall e s (m :: * -> *). C e s m => m [SoftConstraint]
wbo_sequence_of_comments_or_constraints = do
  [Maybe SoftConstraint]
xs <- m (Maybe SoftConstraint) -> m [Maybe SoftConstraint]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many m (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 (Maybe SoftConstraint)
wbo_comment_or_constraint :: forall e s (m :: * -> *). C e s m => m (Maybe SoftConstraint)
wbo_comment_or_constraint = (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
return Maybe 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
  where
    m :: m (Maybe SoftConstraint)
m = (SoftConstraint -> Maybe SoftConstraint)
-> m SoftConstraint -> m (Maybe SoftConstraint)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM SoftConstraint -> 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 = do
  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
  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 -- XXX
  Constraint
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
Just Integer
cost, Constraint
c)

-- | Parse a WBO format string containing weighted boolean optimization problem.
parseWBOString :: String -> String -> Either ParseError 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.pack String
s)
#else
parseWBOString = parse (softformula <* eof)
#endif

-- | Parse a WBO format lazy bytestring containing pseudo boolean problem.
parseWBOByteString :: String -> ByteString -> Either ParseError 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 (Either ParseError SoftFormula)
parseWBOFile :: String -> IO (Either ParseError SoftFormula)
parseWBOFile String
filepath = do
  ByteString
s <- String -> IO ByteString
BL.readFile String
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