{-# LANGUAGE BangPatterns, FlexibleContexts #-}
{-# OPTIONS_GHC -Wall #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.PseudoBoolean.Parsec
-- Copyright   :  (c) Masahiro Sakai 2011-2015
-- License     :  BSD-style
-- 
-- Maintainer  :  masahiro.sakai@gmail.com
-- Portability :  non-portable (BangPatterns, FlexibleContexts)
--
-- 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.Parsec
  (
  -- * Parsing OPB files
    opbParser
  , parseOPBString
  , parseOPBByteString
  , parseOPBFile

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

import Prelude hiding (sum)
import Control.Applicative ((<*))
import Control.Monad
import Data.ByteString.Lazy (ByteString)
import Data.Maybe
import Text.Parsec
import qualified Text.Parsec.ByteString.Lazy as ParsecBS
import Data.PseudoBoolean.Types
import Data.PseudoBoolean.Internal.TextUtil

-- | Parser for OPB files
opbParser :: Stream s m Char => ParsecT s u m Formula
opbParser :: ParsecT s u m Formula
opbParser = ParsecT s u m Formula
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Formula
formula

-- | Parser for WBO files
wboParser :: Stream s m Char => ParsecT s u m SoftFormula
wboParser :: ParsecT s u m SoftFormula
wboParser = ParsecT s u m SoftFormula
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m SoftFormula
softformula

-- <formula>::= <sequence_of_comments> [<objective>] <sequence_of_comments_or_constraints>
formula :: Stream s m Char => ParsecT s u m Formula
formula :: ParsecT s u m Formula
formula = do
  Maybe (Int, Int)
h <- ParsecT s u m (Int, Int) -> ParsecT s u m (Maybe (Int, Int))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT s u m (Int, Int)
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m (Int, Int)
hint
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
sequence_of_comments
  Maybe Sum
obj <- ParsecT s u m Sum -> ParsecT s u m (Maybe Sum)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT s u m Sum
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Sum
objective
  [Constraint]
cs <- ParsecT s u m [Constraint]
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m [Constraint]
sequence_of_comments_or_constraints
  Formula -> ParsecT s u m Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> ParsecT s u m Formula)
-> Formula -> ParsecT s u m Formula
forall a b. (a -> b) -> a -> b
$
    Formula :: Maybe Sum -> [Constraint] -> Int -> Int -> Formula
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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length [Constraint]
cs) (((Int, Int) -> Int) -> Maybe (Int, Int) -> Maybe Int
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 :: Stream s m Char => ParsecT s u m (Int,Int)
hint :: ParsecT s u m (Int, Int)
hint = ParsecT s u m (Int, Int) -> ParsecT s u m (Int, Int)
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s u m (Int, Int) -> ParsecT s u m (Int, Int))
-> ParsecT s u m (Int, Int) -> ParsecT s u m (Int, Int)
forall a b. (a -> b) -> a -> b
$ do
  Char
_ <- Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'*'
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace
  String
_ <- String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"#variable="
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace
  Integer
nv <- ParsecT s u m Integer
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Integer
unsigned_integer
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
oneOrMoreSpace  
  String
_ <- String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"#constraint="
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace
  Integer
nc <- ParsecT s u m Integer
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Integer
unsigned_integer
  String
_ <- ParsecT s u m Char -> ParsecT s u m () -> ParsecT s u m String
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT s u m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
eol
  (Int, Int) -> ParsecT s u m (Int, Int)
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 :: Stream s m Char => ParsecT s u m ()
sequence_of_comments :: ParsecT s u m ()
sequence_of_comments = ParsecT s u m () -> ParsecT s u m ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
comment -- XXX: we allow empty sequence

-- <comment>::= "*" <any_sequence_of_characters_other_than_EOL> <EOL>
comment :: Stream s m Char => ParsecT s u m ()
comment :: ParsecT s u m ()
comment = do
  Char
_ <- Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'*' 
  String
_ <- ParsecT s u m Char -> ParsecT s u m () -> ParsecT s u m String
forall s (m :: * -> *) t u a end.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m end -> ParsecT s u m [a]
manyTill ParsecT s u m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
eol
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces -- We relax the grammer and allow spaces in the beggining of next component.
  () -> ParsecT s u m ()
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 :: Stream s m Char => ParsecT s u m [Constraint]
sequence_of_comments_or_constraints :: ParsecT s u m [Constraint]
sequence_of_comments_or_constraints = do
  [Maybe Constraint]
xs <- ParsecT s u m (Maybe Constraint)
-> ParsecT s u m [Maybe Constraint]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT s u m (Maybe Constraint)
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m (Maybe Constraint)
comment_or_constraint -- We relax the grammer and allow spaces in the beginning of next component.
  [Constraint] -> ParsecT s u m [Constraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Constraint] -> ParsecT s u m [Constraint])
-> [Constraint] -> ParsecT s u 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 :: Stream s m Char => ParsecT s u m (Maybe Constraint)
comment_or_constraint :: ParsecT s u m (Maybe Constraint)
comment_or_constraint =
  (ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
comment ParsecT s u m ()
-> ParsecT s u m (Maybe Constraint)
-> ParsecT s u m (Maybe Constraint)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Constraint -> ParsecT s u m (Maybe Constraint)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Constraint
forall a. Maybe a
Nothing) ParsecT s u m (Maybe Constraint)
-> ParsecT s u m (Maybe Constraint)
-> ParsecT s u m (Maybe Constraint)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ((Constraint -> Maybe Constraint)
-> ParsecT s u m Constraint -> ParsecT s u 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 ParsecT s u m Constraint
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m Constraint
constraint)

-- <objective>::= "min:" <zeroOrMoreSpace> <sum> ";"
objective :: Stream s m Char => ParsecT s u m Sum
objective :: ParsecT s u m Sum
objective = do
  String
_ <- String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"min:"
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace
  Sum
obj <- ParsecT s u m Sum
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Sum
sum
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
semi
  Sum -> ParsecT s u m Sum
forall (m :: * -> *) a. Monad m => a -> m a
return Sum
obj

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

-- <sum>::= <weightedterm> | <weightedterm> <sum>
sum :: Stream s m Char => ParsecT s u m Sum
sum :: ParsecT s u m Sum
sum = ParsecT s u m WeightedTerm -> ParsecT s u m Sum
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT s u m WeightedTerm
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m WeightedTerm
weightedterm -- we relax the grammer to allow empty sum

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

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

-- <unsigned_integer>::= <digit> | <digit><unsigned_integer>
unsigned_integer :: Stream s m Char => ParsecT s u m Integer
unsigned_integer :: ParsecT s u m Integer
unsigned_integer = do
  String
ds <- ParsecT s u m Char -> ParsecT s u m String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT s u m Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
  Integer -> ParsecT s u m Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> ParsecT s u m Integer)
-> Integer -> ParsecT s u m Integer
forall a b. (a -> b) -> a -> b
$! String -> Integer
readUnsignedInteger String
ds

-- <relational_operator>::= ">=" | "="
relational_operator :: Stream s m Char => ParsecT s u m Op
relational_operator :: ParsecT s u m Op
relational_operator = (String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
">=" ParsecT s u m String -> ParsecT s u m Op -> ParsecT s u m Op
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Op -> ParsecT s u m Op
forall (m :: * -> *) a. Monad m => a -> m a
return Op
Ge) ParsecT s u m Op -> ParsecT s u m Op -> ParsecT s u m Op
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"=" ParsecT s u m String -> ParsecT s u m Op -> ParsecT s u m Op
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Op -> ParsecT s u m Op
forall (m :: * -> *) a. Monad m => a -> m a
return Op
Eq)

-- <variablename>::= "x" <unsigned_integer>
variablename :: Stream s m Char => ParsecT s u m Var
variablename :: ParsecT s u m Int
variablename = do
  Char
_ <- Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'x'
  Integer
i <- ParsecT s u m Integer
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Integer
unsigned_integer
  Int -> ParsecT s u m Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ParsecT s u m Int) -> Int -> ParsecT s u 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 :: Stream s m Char => ParsecT s u m ()
oneOrMoreSpace :: ParsecT s u m ()
oneOrMoreSpace  = ParsecT s u m Char -> ParsecT s u m ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 (Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
' ')

-- <zeroOrMoreSpace>::= [" " <zeroOrMoreSpace>]
zeroOrMoreSpace :: Stream s m Char => ParsecT s u m ()
-- zeroOrMoreSpace = skipMany (char ' ')
zeroOrMoreSpace :: ParsecT s u m ()
zeroOrMoreSpace = ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
-- We relax the grammer and allow more type of spacing

eol :: Stream s m Char => ParsecT s u m ()
eol :: ParsecT s u m ()
eol = Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'\n' ParsecT s u m Char -> ParsecT s u m () -> ParsecT s u m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> ParsecT s u m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

semi :: Stream s m Char => ParsecT s u m ()
semi :: ParsecT s u m ()
semi = Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
';' ParsecT s u m Char -> ParsecT s u m () -> ParsecT s u m ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
-- 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 :: Stream s m Char => ParsecT s u m Term
term :: ParsecT s u m Term
term = ParsecT s u m Term
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Term
oneOrMoreLiterals

-- <oneOrMoreLiterals>::= <literal> | <literal> <oneOrMoreSpace> <oneOrMoreLiterals>
oneOrMoreLiterals :: Stream s m Char => ParsecT s u m [Lit]
oneOrMoreLiterals :: ParsecT s u m Term
oneOrMoreLiterals = do
  Int
l <- ParsecT s u m Int
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Int
literal
  ParsecT s u m Term -> ParsecT s u m Term -> ParsecT s u m Term
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (ParsecT s u m Term -> ParsecT s u m Term
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
try (ParsecT s u m Term -> ParsecT s u m Term)
-> ParsecT s u m Term -> ParsecT s u m Term
forall a b. (a -> b) -> a -> b
$ ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
oneOrMoreSpace ParsecT s u m () -> ParsecT s u m Term -> ParsecT s u m Term
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term) -> ParsecT s u m Term -> ParsecT s u m Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int
lInt -> Term -> Term
forall a. a -> [a] -> [a]
:) (ParsecT s u m Term
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Term
oneOrMoreLiterals)) (Term -> ParsecT s u m Term
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 :: Stream s m Char => ParsecT s u m Lit
literal :: ParsecT s u m Int
literal = ParsecT s u m Int
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Int
variablename ParsecT s u m Int -> ParsecT s u m Int -> ParsecT s u m Int
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'~' ParsecT s u m Char -> ParsecT s u m Int -> ParsecT s u m Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Int -> Int) -> ParsecT s u m Int -> ParsecT s u m Int
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Int
forall a. Num a => a -> a
negate ParsecT s u m Int
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Int
variablename)

-- | Parse a OPB format string containing pseudo boolean problem.
parseOPBString :: SourceName -> String -> Either ParseError Formula
parseOPBString :: String -> String -> Either ParseError Formula
parseOPBString = Parsec String () Formula
-> String -> String -> Either ParseError Formula
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse (Parsec String () Formula
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Formula
formula Parsec String () Formula
-> ParsecT String () Identity () -> Parsec String () Formula
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)

-- | Parse a OPB format lazy bytestring containing pseudo boolean problem.
parseOPBByteString :: SourceName -> ByteString -> Either ParseError Formula
parseOPBByteString :: String -> ByteString -> Either ParseError Formula
parseOPBByteString = Parsec ByteString () Formula
-> String -> ByteString -> Either ParseError Formula
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse (Parsec ByteString () Formula
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Formula
formula Parsec ByteString () Formula
-> ParsecT ByteString () Identity ()
-> Parsec ByteString () Formula
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT ByteString () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)

-- | Parse a OPB file containing pseudo boolean problem.
parseOPBFile :: FilePath -> IO (Either ParseError Formula)
parseOPBFile :: String -> IO (Either ParseError Formula)
parseOPBFile = Parsec ByteString () Formula
-> String -> IO (Either ParseError Formula)
forall a. Parser a -> String -> IO (Either ParseError a)
ParsecBS.parseFromFile (Parsec ByteString () Formula
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Formula
formula Parsec ByteString () Formula
-> ParsecT ByteString () Identity ()
-> Parsec ByteString () Formula
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT ByteString () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)


-- <softformula>::= <sequence_of_comments> <softheader> <sequence_of_comments_or_constraints>
softformula :: Stream s m Char => ParsecT s u m SoftFormula
softformula :: ParsecT s u m SoftFormula
softformula = do
  Maybe (Int, Int)
h <- ParsecT s u m (Int, Int) -> ParsecT s u m (Maybe (Int, Int))
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT s u m (Int, Int)
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m (Int, Int)
hint
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
sequence_of_comments
  Maybe Integer
top <- ParsecT s u m (Maybe Integer)
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m (Maybe Integer)
softheader
  [SoftConstraint]
cs <- ParsecT s u m [SoftConstraint]
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m [SoftConstraint]
wbo_sequence_of_comments_or_constraints
  SoftFormula -> ParsecT s u m SoftFormula
forall (m :: * -> *) a. Monad m => a -> m a
return (SoftFormula -> ParsecT s u m SoftFormula)
-> SoftFormula -> ParsecT s u m SoftFormula
forall a b. (a -> b) -> a -> b
$
    SoftFormula :: Maybe Integer -> [SoftConstraint] -> Int -> Int -> SoftFormula
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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length [SoftConstraint]
cs) (((Int, Int) -> Int) -> Maybe (Int, Int) -> Maybe Int
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 :: Stream s m Char => ParsecT s u m (Maybe Integer)
softheader :: ParsecT s u m (Maybe Integer)
softheader = do
  String
_ <- String -> ParsecT s u m String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
"soft:"
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace -- XXX
  Maybe Integer
top <- ParsecT s u m Integer -> ParsecT s u m (Maybe Integer)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe ParsecT s u m Integer
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Integer
unsigned_integer
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace -- XXX
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
semi
  Maybe Integer -> ParsecT s u m (Maybe Integer)
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 :: Stream s m Char => ParsecT s u m [SoftConstraint]
wbo_sequence_of_comments_or_constraints :: ParsecT s u m [SoftConstraint]
wbo_sequence_of_comments_or_constraints = do
  [Maybe SoftConstraint]
xs <- ParsecT s u m (Maybe SoftConstraint)
-> ParsecT s u m [Maybe SoftConstraint]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT s u m (Maybe SoftConstraint)
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m (Maybe SoftConstraint)
wbo_comment_or_constraint -- XXX: we relax the grammer to allow empty sequence
  [SoftConstraint] -> ParsecT s u m [SoftConstraint]
forall (m :: * -> *) a. Monad m => a -> m a
return ([SoftConstraint] -> ParsecT s u m [SoftConstraint])
-> [SoftConstraint] -> ParsecT s u 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 :: Stream s m Char => ParsecT s u m (Maybe SoftConstraint)
wbo_comment_or_constraint :: ParsecT s u m (Maybe SoftConstraint)
wbo_comment_or_constraint = (ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
comment ParsecT s u m ()
-> ParsecT s u m (Maybe SoftConstraint)
-> ParsecT s u m (Maybe SoftConstraint)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe SoftConstraint -> ParsecT s u m (Maybe SoftConstraint)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SoftConstraint
forall a. Maybe a
Nothing) ParsecT s u m (Maybe SoftConstraint)
-> ParsecT s u m (Maybe SoftConstraint)
-> ParsecT s u m (Maybe SoftConstraint)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m (Maybe SoftConstraint)
forall u. ParsecT s u m (Maybe SoftConstraint)
m
  where
    m :: ParsecT s u m (Maybe SoftConstraint)
m = (SoftConstraint -> Maybe SoftConstraint)
-> ParsecT s u m SoftConstraint
-> ParsecT s u 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 (ParsecT s u m SoftConstraint
 -> ParsecT s u m (Maybe SoftConstraint))
-> ParsecT s u m SoftConstraint
-> ParsecT s u m (Maybe SoftConstraint)
forall a b. (a -> b) -> a -> b
$ (ParsecT s u m Constraint
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m Constraint
constraint ParsecT s u m Constraint
-> (Constraint -> ParsecT s u m SoftConstraint)
-> ParsecT s u m SoftConstraint
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Constraint
c -> SoftConstraint -> ParsecT s u m SoftConstraint
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Integer
forall a. Maybe a
Nothing, Constraint
c)) ParsecT s u m SoftConstraint
-> ParsecT s u m SoftConstraint -> ParsecT s u m SoftConstraint
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT s u m SoftConstraint
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m SoftConstraint
softconstraint

-- <softconstraint>::= "[" <zeroOrMoreSpace> <unsigned_integer> <zeroOrMoreSpace> "]" <constraint>
softconstraint :: Stream s m Char => ParsecT s u m SoftConstraint
softconstraint :: ParsecT s u m SoftConstraint
softconstraint = do
  Char
_ <- Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'['
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace
  Integer
cost <- ParsecT s u m Integer
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Integer
unsigned_integer
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace
  Char
_ <- Char -> ParsecT s u m Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
']'
  ParsecT s u m ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
zeroOrMoreSpace -- XXX
  Constraint
c <- ParsecT s u m Constraint
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m Constraint
constraint
  SoftConstraint -> ParsecT s u m SoftConstraint
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 :: SourceName -> String -> Either ParseError SoftFormula
parseWBOString :: String -> String -> Either ParseError SoftFormula
parseWBOString = Parsec String () SoftFormula
-> String -> String -> Either ParseError SoftFormula
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse (Parsec String () SoftFormula
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m SoftFormula
softformula Parsec String () SoftFormula
-> ParsecT String () Identity () -> Parsec String () SoftFormula
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)

-- | Parse a WBO format lazy bytestring containing pseudo boolean problem.
parseWBOByteString :: SourceName -> ByteString -> Either ParseError SoftFormula
parseWBOByteString :: String -> ByteString -> Either ParseError SoftFormula
parseWBOByteString = Parsec ByteString () SoftFormula
-> String -> ByteString -> Either ParseError SoftFormula
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse (Parsec ByteString () SoftFormula
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m SoftFormula
softformula Parsec ByteString () SoftFormula
-> ParsecT ByteString () Identity ()
-> Parsec ByteString () SoftFormula
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT ByteString () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)

-- | Parse a WBO file containing weighted boolean optimization problem.
parseWBOFile :: FilePath -> IO (Either ParseError SoftFormula)
parseWBOFile :: String -> IO (Either ParseError SoftFormula)
parseWBOFile = Parsec ByteString () SoftFormula
-> String -> IO (Either ParseError SoftFormula)
forall a. Parser a -> String -> IO (Either ParseError a)
ParsecBS.parseFromFile (Parsec ByteString () SoftFormula
forall s (m :: * -> *) u.
Stream s m Char =>
ParsecT s u m SoftFormula
softformula Parsec ByteString () SoftFormula
-> ParsecT ByteString () Identity ()
-> Parsec ByteString () SoftFormula
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT ByteString () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof)