packages feed

pseudo-boolean (empty) → 0.1.0.0

raw patch · 25 files changed

+1505/−0 lines, 25 filesdep +HUnitdep +QuickCheckdep +attoparsecsetup-changed

Dependencies added: HUnit, QuickCheck, attoparsec, base, bytestring, bytestring-builder, containers, deepseq, dlist, hashable, parsec, pseudo-boolean, tasty, tasty-hunit, tasty-quickcheck, tasty-th, temporary

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Masahiro Sakai++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Masahiro Sakai nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,4 @@+# pseudo-boolean+Haskell library for parsing/generating OPB/WBO files used in pseudo boolean competition.++[![Build Status](https://secure.travis-ci.org/msakai/pseudo-boolean.png?branch=master)](http://travis-ci.org/msakai/pseudo-boolean) [![Coverage Status](https://coveralls.io/repos/msakai/pseudo-boolean/badge.svg)](https://coveralls.io/r/msakai/pseudo-boolean) [![Hackage](https://budueba.com/hackage/pseudo-boolean)](https://hackage.haskell.org/package/pseudo-boolean)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ pseudo-boolean.cabal view
@@ -0,0 +1,72 @@+-- Initial pseudo-boolean.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++name:                pseudo-boolean+version:             0.1.0.0+synopsis:            Reading\/Writing OPB\/WBO files used in pseudo boolean competition+description:         Reading\/Writing OPB\/WBO files used in pseudo boolean competition+homepage:            https://github.com/msakai/pseudo-boolean+license:             BSD3+license-file:        LICENSE+author:              Masahiro Sakai+maintainer:          masahiro.sakai@gmail.com+-- copyright:           +category:            Data, Optimisation, Optimization, Constraints, Logic+build-type:          Simple+extra-source-files:+    README.md+    test/samples/*.opb+    test/samples/*.wbo+cabal-version:       >=1.10++source-repository head+  type:     git+  location: git://github.com/msakai/pseudo-boolean.git++library+  exposed-modules:+     Data.PseudoBoolean+     Data.PseudoBoolean.Builder+     Data.PseudoBoolean.ByteStringBuilder+     Data.PseudoBoolean.Parsec+     Data.PseudoBoolean.Attoparsec+     Data.PseudoBoolean.Internal.TextUtil+  other-modules:+     Data.PseudoBoolean.Types+  other-extensions:+     BangPatterns+     CPP+     DeriveDataTypeable+     DeriveGeneric+     FlexibleContexts+     OverloadedStrings+  build-depends:+     base >=4.6.0.1 && <4.9,+     containers >=0.4.2.1,+     parsec >=3.1.2 && <4,+     bytestring >=0.9.2.1 && <0.11,+     bytestring-builder,+     dlist >=0.7.0 && <0.8.0,+     attoparsec >=0.10.4.0,+     deepseq >=1.3.0.0,+     hashable >=1.1.2.5 && <1.3.0.0+  hs-source-dirs:      src+  default-language:    Haskell2010++Test-suite TestPBFile+  Type:              exitcode-stdio-1.0+  HS-Source-Dirs:    test+  Main-is:           TestPBFile.hs+  Build-depends:+    pseudo-boolean,+    base,+    bytestring,+    tasty >=0.10.1,+    tasty-hunit ==0.9.*,+    tasty-quickcheck ==0.8.*,+    tasty-th,+    HUnit,+    QuickCheck >=2.5 && <3,+    temporary >=1.2+  Default-Language: Haskell2010+  Other-Extensions: TemplateHaskell
+ src/Data/PseudoBoolean.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE BangPatterns #-}+{-# OPTIONS_GHC -Wall #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.PseudoBoolean+-- Copyright   :  (c) Masahiro Sakai 2011-2015+-- License     :  BSD-style+-- +-- Maintainer  :  masahiro.sakai@gmail.com+-- Portability :  non-portable (BangPatterns)+--+-- A library for parsing\/generating 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+  (+  -- * Abstract Syntax+    Formula (..)+  , Constraint+  , Op (..)+  , SoftFormula (..)+  , SoftConstraint+  , Sum+  , WeightedTerm+  , Term+  , Lit+  , Var++  -- * Parsing OPB files+  -- $ParsingOPB+  , parseOPBString+  , parseOPBByteString+  , parseOPBFile++  -- * Parsing WBO files+  -- $ParsingWBO+  , parseWBOString+  , parseWBOByteString+  , parseWBOFile++  -- * Generating OPB files+  , toOPBString+  , toOPBByteString+  , writeOPBFile+  , hPutOPB++  -- * Generating WBO files+  , toWBOString+  , toWBOByteString+  , writeWBOFile+  , hPutWBO+  ) where++import Data.PseudoBoolean.Parsec+import Data.PseudoBoolean.Types+import Data.PseudoBoolean.Builder+import Data.PseudoBoolean.ByteStringBuilder as ByteStringBuilder++-- $ParsingOPB+-- These functions are based on Parsec.+-- If you want faster parser, you can also use "Data.PseudoBoolean.Attoparsec" module.++-- $ParsingWBO+-- These functions are based on Parsec. +-- If you want faster parser, you can also use "Data.PseudoBoolean.Attoparsec" module.
+ src/Data/PseudoBoolean/Attoparsec.hs view
@@ -0,0 +1,272 @@+{-# 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 = formula++-- | Parser for WBO files+wboParser :: Parser SoftFormula+wboParser = softformula++-- <formula>::= <sequence_of_comments> [<objective>] <sequence_of_comments_or_constraints>+formula :: Parser Formula+formula = do+  h <- optionMaybe hint+  sequence_of_comments+  obj <- optionMaybe 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 :: Parser (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>::= <comment> [<sequence_of_comments>]+sequence_of_comments :: Parser ()+sequence_of_comments = skipMany comment -- XXX: we allow empty sequence++-- <comment>::= "*" <any_sequence_of_characters_other_than_EOL> <EOL>+comment :: Parser ()+comment = do+  _ <- char '*' +  _ <- manyTill anyChar eol+  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 = do+  xs <- many1 comment_or_constraint+  return $ catMaybes xs++-- <comment_or_constraint>::= <comment>|<constraint>+comment_or_constraint :: Parser (Maybe Constraint)+comment_or_constraint =+  (comment >> return Nothing) <|> (liftM Just constraint)++-- <objective>::= "min:" <zeroOrMoreSpace> <sum> ";"+objective :: Parser Sum+objective = do+  _ <- string "min:"+  zeroOrMoreSpace+  obj <- sum+  _ <- char ';'+  eol+  return obj++-- <constraint>::= <sum> <relational_operator> <zeroOrMoreSpace> <integer> <zeroOrMoreSpace> ";"+constraint :: Parser Constraint+constraint = do+  lhs <- sum+  op <- relational_operator+  zeroOrMoreSpace+  rhs <- integer+  zeroOrMoreSpace+  semi+  return (lhs, op, rhs)++-- <sum>::= <weightedterm> | <weightedterm> <sum>+sum :: Parser Sum+sum = many1 weightedterm++-- <weightedterm>::= <integer> <oneOrMoreSpace> <term> <oneOrMoreSpace>+weightedterm :: Parser WeightedTerm+weightedterm = do+  w <- integer+  oneOrMoreSpace+  t <- term+  oneOrMoreSpace+  return (w,t)++-- <integer>::= <unsigned_integer> | "+" <unsigned_integer> | "-" <unsigned_integer>+integer :: Parser Integer+integer = msum+  [ unsigned_integer+  , char '+' >> unsigned_integer+  , char '-' >> liftM negate unsigned_integer+  ]++-- <unsigned_integer>::= <digit> | <digit><unsigned_integer>+unsigned_integer :: Parser Integer+unsigned_integer = do+  ds <- takeWhile1 isDigit+  return $! readUnsignedInteger $ BS.unpack ds++-- <relational_operator>::= ">=" | "="+relational_operator :: Parser Op+relational_operator = (string ">=" >> return Ge) <|> (string "=" >> return Eq)++-- <variablename>::= "x" <unsigned_integer>+variablename :: Parser Var+variablename = do+  _ <- char 'x'+  i <- unsigned_integer+  return $! fromIntegral i++-- <oneOrMoreSpace>::= " " [<oneOrMoreSpace>]+oneOrMoreSpace :: Parser ()+oneOrMoreSpace  = skipMany1 (char ' ')++-- <zeroOrMoreSpace>::= [" " <zeroOrMoreSpace>]+zeroOrMoreSpace :: Parser ()+zeroOrMoreSpace = skipMany (char ' ')++eol :: Parser ()+eol = char '\n' >> return ()++semi :: Parser ()+semi = char ';' >> eol++{-+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 = oneOrMoreLiterals++-- <oneOrMoreLiterals>::= <literal> | <literal> <oneOrMoreSpace> <oneOrMoreLiterals>+oneOrMoreLiterals :: Parser [Lit]+oneOrMoreLiterals = do+  l <- literal+  mplus (try $ oneOrMoreSpace >> liftM (l:) (oneOrMoreLiterals)) (return [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 = variablename <|> (char '~' >> liftM negate variablename)++-- | Parse a OPB format string containing pseudo boolean problem.+parseOPBByteString :: BSLazy.ByteString -> Either String Formula+parseOPBByteString s = L.eitherResult $ L.parse formula s++-- | Parse a OPB file containing pseudo boolean problem.+parseOPBFile :: FilePath -> IO (Either String Formula)+parseOPBFile fname = do+  s <- BSLazy.readFile fname+  return $ parseOPBByteString s++-- <softformula>::= <sequence_of_comments> <softheader> <sequence_of_comments_or_constraints>+softformula :: Parser SoftFormula+softformula = do+  h <- optionMaybe 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>::= "soft:" [<unsigned_integer>] ";"+softheader :: Parser (Maybe Integer)+softheader = do+  _ <- string "soft:"+  zeroOrMoreSpace -- XXX+  top <- optionMaybe unsigned_integer+  zeroOrMoreSpace -- XXX+  semi+  return 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 = do+  xs <- many1 wbo_comment_or_constraint+  return $ catMaybes xs++-- <comment_or_constraint>::= <comment>|<constraint>|<softconstraint>+wbo_comment_or_constraint :: Parser (Maybe SoftConstraint)+wbo_comment_or_constraint = (comment >> return Nothing) <|> m+  where+    m = liftM Just $ (constraint >>= \c -> return (Nothing, c)) <|> softconstraint++-- <softconstraint>::= "[" <zeroOrMoreSpace> <unsigned_integer> <zeroOrMoreSpace> "]" <constraint>+softconstraint :: Parser SoftConstraint+softconstraint = do+  _ <- char '['+  zeroOrMoreSpace+  cost <- unsigned_integer+  zeroOrMoreSpace+  _ <- char ']'+  zeroOrMoreSpace -- XXX+  c <- constraint+  return (Just cost, c)++-- | Parse a WBO format string containing weighted boolean optimization problem.+parseWBOByteString :: BSLazy.ByteString -> Either String SoftFormula+parseWBOByteString s = L.eitherResult $ L.parse softformula s++-- | Parse a WBO file containing weighted boolean optimization problem.+parseWBOFile :: FilePath -> IO (Either String SoftFormula)+parseWBOFile fname = do+  s <- BSLazy.readFile fname+  return $ parseWBOByteString s++optionMaybe :: Parser a -> Parser (Maybe a)+optionMaybe p = option Nothing (liftM Just p)
+ src/Data/PseudoBoolean/Builder.hs view
@@ -0,0 +1,91 @@+{-# OPTIONS_GHC -Wall #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.PseudoBoolean.Builder+-- Copyright   :  (c) Masahiro Sakai 2011-2015+-- License     :  BSD-style+-- +-- Maintainer  :  masahiro.sakai@gmail.com+-- Portability :  portable+--+-----------------------------------------------------------------------------++module Data.PseudoBoolean.Builder+  (+  -- * Builder for String-like Monoid+    opbBuilder+  , wboBuilder++  -- * String generation+  , toOPBString+  , toWBOString+  ) where++import Prelude hiding (sum)+import qualified Data.DList as DList+import Data.Monoid hiding (Sum (..))+import Data.String+import Text.Printf+import Data.PseudoBoolean.Types++-- | A builder which renders a OPB format in any String-like 'Monoid'.+opbBuilder :: (Monoid a, IsString a) => Formula -> a+opbBuilder opb = (size <> part1 <> part2)+  where+    nv = pbNumVars opb+    nc = pbNumConstraints opb+    size = fromString (printf "* #variable= %d #constraint= %d\n" nv nc)+    part1 = +      case pbObjectiveFunction opb of+        Nothing -> mempty+        Just o -> fromString "min: " <> showSum o <> fromString ";\n"+    part2 = mconcat $ map showConstraint (pbConstraints opb)++-- | A builder which renders a WBO format in any String-like 'Monoid'.+wboBuilder :: (Monoid a, IsString a) => SoftFormula -> a+wboBuilder wbo = size <> part1 <> part2+  where+    nv = wboNumVars wbo+    nc = wboNumConstraints wbo+    size = fromString (printf "* #variable= %d #constraint= %d\n" nv nc)+    part1 = +      case wboTopCost wbo of+        Nothing -> fromString "soft: ;\n"+        Just t -> fromString "soft: " <> fromString (show t) <> fromString ";\n"+    part2 = mconcat $ map showSoftConstraint (wboConstraints wbo)++showSum :: (Monoid a, IsString a) => Sum -> a+showSum = mconcat . map showWeightedTerm++showWeightedTerm :: (Monoid a, IsString a) => WeightedTerm -> a+showWeightedTerm (c, lits) = foldr (\f g -> f <> fromString " " <> g) mempty (x:xs)+  where+    x = if c >= 0 then fromString "+" <> fromString (show c) else fromString (show c)+    xs = map showLit lits++showLit :: (Monoid a, IsString a) => Lit -> a+showLit lit = if lit > 0 then v else fromString "~" <> v+  where+    v = fromString "x" <> fromString (show (abs lit))++showConstraint :: (Monoid a, IsString a) => Constraint -> a+showConstraint (lhs, op, rhs) =+  showSum lhs <> f op <>  fromString " " <> fromString (show rhs) <> fromString ";\n"+  where+    f Eq = fromString "="+    f Ge = fromString ">="++showSoftConstraint :: (Monoid a, IsString a) => SoftConstraint -> a+showSoftConstraint (cost, constr) =+  case cost of+    Nothing -> showConstraint constr+    Just c -> fromString "[" <> fromString (show c) <> fromString "] " <> showConstraint constr+++-- | Generate a OPB format string containing pseudo boolean problem.+toOPBString :: Formula -> String+toOPBString opb = DList.apply (opbBuilder opb) ""++-- | Generate a WBO format string containing weighted boolean optimization problem.+toWBOString :: SoftFormula -> String+toWBOString wbo = DList.apply (wboBuilder wbo) ""
+ src/Data/PseudoBoolean/ByteStringBuilder.hs view
@@ -0,0 +1,131 @@+{-# OPTIONS_GHC -Wall #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.PseudoBoolean.ByteStringBuilder+-- Copyright   :  (c) Masahiro Sakai 2011-2015+-- License     :  BSD-style+-- +-- Maintainer  :  masahiro.sakai@gmail.com+-- Portability :  portable+--+-----------------------------------------------------------------------------++module Data.PseudoBoolean.ByteStringBuilder+  (+  -- * Builder for (Lazy) ByteString generation+    opbBuilder+  , wboBuilder++  -- * Lazy ByteString generation+  , toOPBByteString+  , toWBOByteString++  -- * File I/O+  , writeOPBFile+  , writeWBOFile+  , hPutOPB+  , hPutWBO+  ) where++import Prelude hiding (sum)+import Data.Monoid hiding (Sum (..))+import qualified Data.ByteString.Lazy as BS+import Data.ByteString.Builder (Builder, intDec, integerDec, char7, string7, hPutBuilder, toLazyByteString)+import System.IO+import Data.PseudoBoolean.Types++-- | A ByteString Builder which renders a OPB format byte-string containing pseudo boolean problem.+opbBuilder :: Formula -> Builder+opbBuilder opb = (size <> part1 <> part2)+  where+    nv = pbNumVars opb+    nc = pbNumConstraints opb+    size = string7 "* #variable= " <> intDec nv <> string7 " #constraint= " <> intDec nc <> char7 '\n'+    part1 = +      case pbObjectiveFunction opb of+        Nothing -> mempty+        Just o -> string7 "min: " <> showSum o <> string7 ";\n"+    part2 = mconcat $ map showConstraint (pbConstraints opb)++-- | A ByteString Builder which renders a WBO format byte-string containing weighted boolean optimization problem.+wboBuilder :: SoftFormula -> Builder+wboBuilder wbo = size <> part1 <> part2+  where+    nv = wboNumVars wbo+    nc = wboNumConstraints wbo+    size = string7 "* #variable= " <> intDec nv <> string7 " #constraint= " <> intDec nc <> char7 '\n'+    part1 = +      case wboTopCost wbo of+        Nothing -> string7 "soft: ;\n"+        Just t -> string7 "soft: " <> integerDec t <> string7 ";\n"+    part2 = mconcat $ map showSoftConstraint (wboConstraints wbo)++showSum :: Sum -> Builder+showSum = mconcat . map showWeightedTerm++showWeightedTerm :: WeightedTerm -> Builder+showWeightedTerm (c, lits) = foldr (\f g -> f <> char7 ' ' <> g) mempty (x:xs)+  where+    x = if c >= 0 then char7 '+' <> integerDec c else integerDec c+    xs = map showLit lits++showLit :: Lit -> Builder+showLit lit = if lit > 0 then v else char7 '~' <> v+  where+    v = char7 'x' <> intDec (abs lit)++showConstraint :: Constraint -> Builder+showConstraint (lhs, op, rhs) =+  showSum lhs <> f op <>  char7 ' ' <> integerDec rhs <> string7 ";\n"+  where+    f Eq = char7 '='+    f Ge = string7 ">="++showSoftConstraint :: SoftConstraint -> Builder+showSoftConstraint (cost, constr) =+  case cost of+    Nothing -> showConstraint constr+    Just c -> char7 '[' <> integerDec c <> string7 "] " <> showConstraint constr++++-- | Generate a OPB format byte-string containing pseudo boolean problem.+toOPBByteString :: Formula -> BS.ByteString+toOPBByteString opb = toLazyByteString (opbBuilder opb)++-- | Generate a WBO format byte-string containing weighted boolean optimization problem.+toWBOByteString :: SoftFormula -> BS.ByteString+toWBOByteString wbo = toLazyByteString (wboBuilder wbo)++-- | Output a OPB file containing pseudo boolean problem.+writeOPBFile :: FilePath -> Formula -> IO ()+writeOPBFile filepath opb = withBinaryFile filepath WriteMode $ \h -> do+  hSetBuffering h (BlockBuffering Nothing)+  hPutOPB h opb++-- | Output a WBO file containing weighted boolean optimization problem.+writeWBOFile :: FilePath -> SoftFormula -> IO ()+writeWBOFile filepath wbo = withBinaryFile filepath WriteMode $ \h -> do+  hSetBuffering h (BlockBuffering Nothing)+  hPutWBO h wbo++-- | Output a OPB file to a 'Handle' using 'hPutBuilder'.+--+-- It is recommended that the 'Handle' is set to binary and+-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.+--+-- This function is more efficient than 'hPut' . 'toOPBByteString'+-- because in many cases no buffer allocation has to be done.+hPutOPB :: Handle -> Formula -> IO ()+hPutOPB h opb = hPutBuilder h (opbBuilder opb)+++-- | Output a WBO file to a 'Handle' using 'hPutBuilder'.+--+-- It is recommended that the 'Handle' is set to binary and+-- 'BlockBuffering' mode. See 'hSetBinaryMode' and 'hSetBuffering'.+--+-- This function is more efficient than 'hPut' . 'toWBOByteString'+-- because in many cases no buffer allocation has to be done.+hPutWBO :: Handle -> SoftFormula -> IO ()+hPutWBO h wbo = hPutBuilder h (wboBuilder wbo)
+ src/Data/PseudoBoolean/Internal/TextUtil.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE BangPatterns, CPP #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.PseudoBoolean.Internal.TextUtil+-- Copyright   :  (c) Masahiro Sakai 2012-2014+-- License     :  BSD-style+-- +-- Maintainer  :  masahiro.sakai@gmail.com+-- Stability   :  provisional+-- Portability :  non-portable (BangPatterns)+--+-----------------------------------------------------------------------------+module Data.PseudoBoolean.Internal.TextUtil+  ( readUnsignedInteger+  ) where++#include "MachDeps.h"++import Control.Exception+import Data.Word++-- | 'read' allocate too many intermediate 'Integer'.+-- Therefore we use this optimized implementation instead.+-- Many intermediate values in this implementation will be optimized+-- away by worker-wrapper transformation and unboxing.+{-# INLINABLE readUnsignedInteger #-}+readUnsignedInteger :: String -> Integer +readUnsignedInteger str = assert (result == read str) $ result+  where+    result :: Integer+    result = go 0 str++    lim :: Word+#if !MIN_VERSION_base(4,6,1) && WORD_SIZE_IN_BITS == 32+    {- To avoid a bug of maxBound <https://ghc.haskell.org/trac/ghc/ticket/8072> -}+    lim = 0xFFFFFFFF `div` 10+#else+    lim = maxBound `div` 10+#endif+  +    go :: Integer -> [Char] -> Integer +    go !r [] = r+    go !r ds =+      case go2 0 1 ds of+        (r2,b,ds2) -> go (r * fromIntegral b + fromIntegral r2) ds2++    go2 :: Word -> Word -> [Char] -> (Word, Word, [Char])+    go2 !r !b dds | assert (b > r) (b > lim) = (r,b,dds)+    go2 !r !b []     = (r, b, [])+    go2 !r !b (d:ds) = go2 (r*10 + charToWord d) (b*10) ds++    charToWord :: Char -> Word+    charToWord '0' = 0+    charToWord '1' = 1+    charToWord '2' = 2+    charToWord '3' = 3+    charToWord '4' = 4+    charToWord '5' = 5+    charToWord '6' = 6+    charToWord '7' = 7+    charToWord '8' = 8+    charToWord '9' = 9
+ src/Data/PseudoBoolean/Parsec.hs view
@@ -0,0 +1,273 @@+{-# 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.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 = formula++-- | Parser for WBO files+wboParser :: Stream s m Char => ParsecT s u m SoftFormula+wboParser = softformula++-- <formula>::= <sequence_of_comments> [<objective>] <sequence_of_comments_or_constraints>+formula :: Stream s m Char => ParsecT s u m Formula+formula = do+  h <- optionMaybe hint+  sequence_of_comments+  obj <- optionMaybe 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 :: Stream s m Char => ParsecT s u 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>::= <comment> [<sequence_of_comments>]+sequence_of_comments :: Stream s m Char => ParsecT s u m ()+sequence_of_comments = skipMany 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 = do+  _ <- char '*' +  _ <- manyTill anyChar eol+  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 = do+  xs <- many1 comment_or_constraint+  return $ catMaybes xs++-- <comment_or_constraint>::= <comment>|<constraint>+comment_or_constraint :: Stream s m Char => ParsecT s u m (Maybe Constraint)+comment_or_constraint =+  (comment >> return Nothing) <|> (liftM Just constraint)++-- <objective>::= "min:" <zeroOrMoreSpace> <sum> ";"+objective :: Stream s m Char => ParsecT s u m Sum+objective = do+  _ <- string "min:"+  zeroOrMoreSpace+  obj <- sum+  _ <- char ';'+  eol+  return obj++-- <constraint>::= <sum> <relational_operator> <zeroOrMoreSpace> <integer> <zeroOrMoreSpace> ";"+constraint :: Stream s m Char => ParsecT s u m Constraint+constraint = do+  lhs <- sum+  op <- relational_operator+  zeroOrMoreSpace+  rhs <- integer+  zeroOrMoreSpace+  semi+  return (lhs, op, rhs)++-- <sum>::= <weightedterm> | <weightedterm> <sum>+sum :: Stream s m Char => ParsecT s u m Sum+sum = many1 weightedterm++-- <weightedterm>::= <integer> <oneOrMoreSpace> <term> <oneOrMoreSpace>+weightedterm :: Stream s m Char => ParsecT s u m WeightedTerm+weightedterm = do+  w <- integer+  oneOrMoreSpace+  t <- term+  oneOrMoreSpace+  return (w,t)++-- <integer>::= <unsigned_integer> | "+" <unsigned_integer> | "-" <unsigned_integer>+integer :: Stream s m Char => ParsecT s u m Integer+integer = msum+  [ unsigned_integer+  , char '+' >> unsigned_integer+  , char '-' >> liftM negate unsigned_integer+  ]++-- <unsigned_integer>::= <digit> | <digit><unsigned_integer>+unsigned_integer :: Stream s m Char => ParsecT s u m Integer+unsigned_integer = do+  ds <- many1 digit+  return $! readUnsignedInteger ds++-- <relational_operator>::= ">=" | "="+relational_operator :: Stream s m Char => ParsecT s u m Op+relational_operator = (string ">=" >> return Ge) <|> (string "=" >> return Eq)++-- <variablename>::= "x" <unsigned_integer>+variablename :: Stream s m Char => ParsecT s u m Var+variablename = do+  _ <- char 'x'+  i <- unsigned_integer+  return $! fromIntegral i++-- <oneOrMoreSpace>::= " " [<oneOrMoreSpace>]+oneOrMoreSpace :: Stream s m Char => ParsecT s u m ()+oneOrMoreSpace  = skipMany1 (char ' ')++-- <zeroOrMoreSpace>::= [" " <zeroOrMoreSpace>]+zeroOrMoreSpace :: Stream s m Char => ParsecT s u m ()+zeroOrMoreSpace = skipMany (char ' ')++eol :: Stream s m Char => ParsecT s u m ()+eol = char '\n' >> return ()++semi :: Stream s m Char => ParsecT s u m ()+semi = char ';' >> eol++{-+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 = oneOrMoreLiterals++-- <oneOrMoreLiterals>::= <literal> | <literal> <oneOrMoreSpace> <oneOrMoreLiterals>+oneOrMoreLiterals :: Stream s m Char => ParsecT s u m [Lit]+oneOrMoreLiterals = do+  l <- literal+  mplus (try $ oneOrMoreSpace >> liftM (l:) (oneOrMoreLiterals)) (return [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 = variablename <|> (char '~' >> liftM negate variablename)++-- | Parse a OPB format string containing pseudo boolean problem.+parseOPBString :: SourceName -> String -> Either ParseError Formula+parseOPBString = parse formula++-- | Parse a OPB format lazy bytestring containing pseudo boolean problem.+parseOPBByteString :: SourceName -> ByteString -> Either ParseError Formula+parseOPBByteString = parse formula++-- | Parse a OPB file containing pseudo boolean problem.+parseOPBFile :: FilePath -> IO (Either ParseError Formula)+parseOPBFile = ParsecBS.parseFromFile formula+++-- <softformula>::= <sequence_of_comments> <softheader> <sequence_of_comments_or_constraints>+softformula :: Stream s m Char => ParsecT s u m SoftFormula+softformula = do+  h <- optionMaybe 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>::= "soft:" [<unsigned_integer>] ";"+softheader :: Stream s m Char => ParsecT s u m (Maybe Integer)+softheader = do+  _ <- string "soft:"+  zeroOrMoreSpace -- XXX+  top <- optionMaybe unsigned_integer+  zeroOrMoreSpace -- XXX+  semi+  return 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 = do+  xs <- many1 wbo_comment_or_constraint+  return $ catMaybes 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 = (comment >> return Nothing) <|> m+  where+    m = liftM Just $ (constraint >>= \c -> return (Nothing, c)) <|> softconstraint++-- <softconstraint>::= "[" <zeroOrMoreSpace> <unsigned_integer> <zeroOrMoreSpace> "]" <constraint>+softconstraint :: Stream s m Char => ParsecT s u m SoftConstraint+softconstraint = do+  _ <- char '['+  zeroOrMoreSpace+  cost <- unsigned_integer+  zeroOrMoreSpace+  _ <- char ']'+  zeroOrMoreSpace -- XXX+  c <- constraint+  return (Just cost, c)++-- | Parse a WBO format string containing weighted boolean optimization problem.+parseWBOString :: SourceName -> String -> Either ParseError SoftFormula+parseWBOString = parse softformula++-- | Parse a WBO format lazy bytestring containing pseudo boolean problem.+parseWBOByteString :: SourceName -> ByteString -> Either ParseError SoftFormula+parseWBOByteString = parse softformula++-- | Parse a WBO file containing weighted boolean optimization problem.+parseWBOFile :: FilePath -> IO (Either ParseError SoftFormula)+parseWBOFile = ParsecBS.parseFromFile softformula
+ src/Data/PseudoBoolean/Types.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE BangPatterns, DeriveDataTypeable, DeriveGeneric #-}+{-# OPTIONS_GHC -Wall #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Data.PseudoBoolean.Types+-- Copyright   :  (c) Masahiro Sakai 2011-2015+-- License     :  BSD-style+-- +-- Maintainer  :  masahiro.sakai@gmail.com+-- Portability :  non-portable (BangPatterns, DeriveDataTypeable, DeriveGeneric)+-- +-- 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.Types+  (+  -- * Abstract Syntax+    Formula (..)+  , Constraint+  , Op (..)+  , SoftFormula (..)+  , SoftConstraint+  , Sum+  , WeightedTerm+  , Term+  , Lit+  , Var++  -- * Internal utilities+  , pbComputeNumVars+  , wboComputeNumVars+  ) where++import GHC.Generics (Generic)+import Control.DeepSeq+import Data.Data+import Data.Hashable+import Data.Maybe++-- | Pair of /objective function/ and a list of constraints.+data Formula+  = Formula+  { pbObjectiveFunction :: Maybe Sum+  , pbConstraints :: [Constraint]+  , pbNumVars :: !Int+  , pbNumConstraints :: !Int+  }+  deriving (Eq, Ord, Show, Typeable, Data, Generic)++instance NFData Formula+instance Hashable Formula++-- | Lhs, relational operator and rhs.+type Constraint = (Sum, Op, Integer)++-- | Relational operators+data Op+  = Ge -- ^ /greater than or equal/+  | Eq -- ^ /equal/+  deriving (Eq, Ord, Show, Enum, Bounded, Typeable, Data, Generic)++instance NFData Op+instance Hashable Op++-- | A pair of /top cost/ and a list of soft constraints.+data SoftFormula+  = SoftFormula+  { wboTopCost :: Maybe Integer+  , wboConstraints :: [SoftConstraint]+  , wboNumVars :: !Int+  , wboNumConstraints :: !Int+  }+  deriving (Eq, Ord, Show, Typeable, Data, Generic)++instance NFData SoftFormula+instance Hashable SoftFormula++-- | A pair of weight and constraint.+type SoftConstraint = (Maybe Integer, Constraint)++-- | Sum of 'WeightedTerm'+type Sum = [WeightedTerm]++-- | Coefficient and 'Term'+type WeightedTerm = (Integer, Term)++-- | List of variables interpreted as products+type Term = [Lit]++-- | Positive (resp. negative) literals are represented as positive (resp. negative) integers.+type Lit = Int++-- | Variable are repserented as positive integers.+type Var = Int++-- | Utility function for computing number of variables in given objective function and constraints.+pbComputeNumVars :: Maybe Sum -> [Constraint] -> Int+pbComputeNumVars obj cs = maximum (0 : vs)+  where+    vs = do+      s <- maybeToList obj ++ [s | (s,_,_) <- cs]+      (_, tm) <- s+      lit <- tm+      return $ abs lit++-- | Utility function for computing number of variables in given objective function and constraints.+wboComputeNumVars :: [SoftConstraint] -> Int+wboComputeNumVars cs = maximum (0 : vs)+  where+    vs = do+      s <- [s | (_, (s,_,_)) <- cs]+      (_, tm) <- s+      lit <- tm+      return $ abs lit
+ test/TestPBFile.hs view
@@ -0,0 +1,218 @@+{-# LANGUAGE TemplateHaskell #-}+{-# OPTIONS_GHC -Wall #-}+module Main (main) where++import qualified Data.ByteString.Lazy.Char8 as BSChar8+import System.IO+import System.IO.Temp+import Test.Tasty+import Test.Tasty.QuickCheck+import Test.Tasty.HUnit+import Test.Tasty.TH+import Data.PseudoBoolean+import qualified Data.PseudoBoolean.Attoparsec as A+import Data.PseudoBoolean.Internal.TextUtil++case_exampleLIN  = checkOPBString "exampleLIN"  exampleLIN+case_exampleNLC1 = checkOPBString "exampleNLC1" exampleNLC1+case_exampleNLC2 = checkOPBString "exampleNLC2" exampleNLC2+case_exampleWBO1 = checkWBOString "exampleWBO1" exampleWBO1+case_exampleWBO2 = checkWBOString "exampleWBO2" exampleWBO2+case_exampleWBO3 = checkWBOString "exampleWBO3" exampleWBO3++case_exampleLIN_file  = checkOPBFile "test/samples/example-lin.opb"+case_exampleNLC1_file = checkOPBFile "test/samples/example-nlc-1.opb"+case_exampleNLC2_file = checkOPBFile "test/samples/example-nlc-2.opb"+case_exampleWBO1_file = checkWBOFile "test/samples/example1.wbo"+case_exampleWBO2_file = checkWBOFile "test/samples/example2.wbo"+case_exampleWBO3_file = checkWBOFile "test/samples/example3.wbo"++case_exampleLIN_PBS_file = checkOPBFile "test/samples/example-lin-pbs.opb"+case_exampleLIN_nohint_file = checkOPBFile "test/samples/example-lin-nohint.opb"+case_exampleWBO1_nohint_file = checkWBOFile "test/samples/example1-nohint.wbo"+case_exampleWBO1_notop_file = checkWBOFile "test/samples/example1-notop.wbo"++case_normalized_1096_cudf_paranoid  = checkOPBFile "test/samples/normalized-1096.cudf.paranoid.opb"+case_normalized_mds_50_10_4 = checkOPBFile "test/samples/normalized-mds_50_10_4.opb"+case_normalized_opt_market_split_4_30_2 = checkOPBFile "test/samples/normalized-opt-market-split_4_30_2.opb"+case_pigeonhole_5_4 = checkOPBFile "test/samples/pigeonhole_5_4.opb"++case_readUnsignedInteger_maxBound_bug :: IO ()+case_readUnsignedInteger_maxBound_bug =+  readUnsignedInteger "006666666666666667" @?= 6666666666666667++prop_readUnsignedInteger = +  forAll (choose (0, 2^(128::Int))) $ \i -> +    readUnsignedInteger (show i) == i++------------------------------------------------------------------------+-- Sample data++exampleLIN :: String+exampleLIN = unlines+  [ "* #variable= 5 #constraint= 4"+  , "*"+  , "* this is a dummy instance"+  , "*"+  , "min: 1 x2 -1 x3 ;"+  , "1 x1 +4 x2 -2 x5 >= 2;"+  , "-1 x1 +4 x2 -2 x5 >= +3;"+  , "12345678901234567890 x4 +4 x3 >= 10;"+  , "* an equality constraint"+  , "2 x2 +3 x4 +2 x1 +3 x5 = 5;"+  ]++exampleNLC1 :: String+exampleNLC1 = unlines+  [ "* #variable= 5 #constraint= 4 #product= 5 sizeproduct= 13"+  , "*"+  , "* this is a dummy instance"+  , "*"+  , "min: 1 x2 x3 -1 x3 ;"+  , "1 x1 +4 x1 ~x2 -2 x5 >= 2;"+  , "-1 x1 +4 x2 -2 x5 >= 3;"+  , "12345678901234567890 x4 +4 x3 >= 10;"+  , "2 x2 x3 +3 x4 ~x5 +2 ~x1 x2 +3 ~x1 x2 x3 ~x4 ~x5 = 5 ;"+  ]++exampleNLC2 :: String+exampleNLC2 = unlines+  [ "* #variable= 6 #constraint= 3 #product= 9 sizeproduct= 18"+  , "*"+  , "* Factorization problem: find the smallest P such that P*Q=N"+  , "* P is a 3 bits number (x3 x2 x1)"+  , "* Q is a 3 bits number (x6 x5 x4)"+  , "* N=35"+  , "* "+  , "* minimize the value of P"+  , "min: +1 x1 +2 x2 +4 x3 ;"+  , "* P>=2 (to avoid trivial factorization)"+  , "+1 x1 +2 x2 +4 x3 >=2;"+  , "* Q>=2 (to avoid trivial factorization)"+  , "+1 x4 +2 x5 +4 x6 >=2;"+  , "*"+  , "* P*Q=N"+  , "+1 x1 x4 +2 x1 x5 +4 x1 x6 +2 x2 x4 +4 x2 x5 +8 x2 x6 +4 x3 x4 +8 x3 x5 +16 x3 x6 = 35;"+  ]++exampleWBO1 :: String+exampleWBO1 = unlines $+  [ "* #variable= 1 #constraint= 2 #soft= 2 mincost= 2 maxcost= 3 sumcost= 5"+  , "soft: 6 ;"+  , "[2] +1 x1 >= 1 ;"+  , "[3] -1 x1 >= 0 ;"+  ]++exampleWBO2 :: String+exampleWBO2 = unlines $+  [ "* #variable= 2 #constraint= 3 #soft= 2 mincost= 2 maxcost= 3 sumcost= 5"+  , "soft: 6 ;"+  , "[2] +1 x1 >= 1 ;"+  , "[3] +1 x2 >= 1 ;"+  , "-1 x1 -1 x2 >= -1 ;"+  ]++exampleWBO3 :: String+exampleWBO3 = unlines $+  [ "* #variable= 4 #constraint= 6 #soft= 4 mincost= 2 maxcost= 5 sumcost= 14"+  , "soft: 6 ;"+  , "[2] +1 x1 >= 1;"+  , "[3] +1 x2 >= 1;"+  , "[4] +1 x3 >= 1;"+  , "[5] +1 x4 >= 1;"+  , "-1 x1 -1 x2 >= -1 ;"+  , "-1 x3 -1 x4 >= -1 ;"+  ]++------------------------------------------------------------------------+-- Utilities++checkOPBFile :: FilePath -> IO ()+checkOPBFile fname = do+  r <- parseOPBFile fname+  case r of+    Left err -> assertFailure $ show err+    Right opb -> do+      r2 <- A.parseOPBFile fname+      case r2 of+        Left err2 -> assertFailure $ show err2+        Right opb2 -> opb2 @?= opb+      withSystemTempFile "TestPBFile.opb" $ \tmppath h -> do+        hClose h+        writeOPBFile tmppath opb+        r3 <- parseOPBFile tmppath+        case r3 of+          Left err3 -> assertFailure $ show err3+          Right opb3 -> opb3 @?= opb++checkOPBString :: String -> String -> IO ()+checkOPBString name str = do+  case parseOPBString name str of+    Left err -> assertFailure $ show err+    Right opb -> do+      let s = toOPBString opb+          bs = toOPBByteString opb+      BSChar8.unpack bs @?= s+      case parseOPBString name s of+        Left err -> assertFailure $ show err+        Right opb2 -> opb2 @?= opb+      case parseOPBByteString name bs of+        Left err -> assertFailure $ show err+        Right opb2 -> opb2 @?= opb+      case A.parseOPBByteString bs of+        Left err -> assertFailure err+        Right opb2 -> opb2 @?= opb++checkWBOFile :: FilePath -> IO ()+checkWBOFile fname = do+  r <- parseWBOFile fname+  case r of+    Left err -> assertFailure $ show err+    Right wbo -> do+      r2 <- A.parseWBOFile fname+      case r2 of+        Left err2 -> assertFailure $ show err2+        Right wbo2 -> wbo2 @?= wbo+      withSystemTempFile "TestPBFile.wbo" $ \tmppath h -> do+        hClose h+        writeWBOFile tmppath wbo+        r3 <- parseWBOFile tmppath+        case r3 of+          Left err3 -> assertFailure $ show err3+          Right wbo3 -> wbo3 @?= wbo++checkWBOString :: String -> String -> IO ()+checkWBOString name str = do+  case parseWBOString name str of+    Left err -> assertFailure $ show err+    Right wbo -> do+      let s = toWBOString wbo+          bs = toWBOByteString wbo+      BSChar8.unpack bs @?= s+      case parseWBOString name s of+        Left err -> assertFailure $ show err+        Right wbo2 -> wbo2 @?= wbo+      case parseWBOByteString name bs of+        Left err -> assertFailure $ show err+        Right wbo2 -> wbo2 @?= wbo+      case A.parseWBOByteString bs of+        Left err -> assertFailure err+        Right wbo2 -> wbo2 @?= wbo++testOPB :: String -> Bool+testOPB s = sf == sf2+  where+    Right sf  = parseOPBString "-" s+    Right sf2 = parseOPBString "-" (toOPBString sf)++testWBO :: String -> Bool+testWBO s = sf == sf2+  where+    Right sf  = parseWBOString "-" s+    Right sf2 = parseWBOString "-" (toWBOString sf)++------------------------------------------------------------------------+-- Test harness++main :: IO ()+main = $(defaultMainGenerator)
+ test/samples/example-lin-nohint.opb view
@@ -0,0 +1,9 @@+*+* this is a dummy instance+*+min: 1 x2 -1 x3 ;+1 x1 +4 x2 -2 x5 >= 2;+-1 x1 +4 x2 -2 x5 >= +3;+12345678901234567890 x4 +4 x3 >= 10;+* an equality constraint+2 x2 +3 x4 +2 x1 +3 x5 = 5;
+ test/samples/example-lin-pbs.opb view
@@ -0,0 +1,9 @@+* #variable= 5 #constraint= 4+*+* this is a dummy instance+*+1 x1 +4 x2 -2 x5 >= 2;+-1 x1 +4 x2 -2 x5 >= +3;+12345678901234567890 x4 +4 x3 >= 10;+* an equality constraint+2 x2 +3 x4 +2 x1 +3 x5 = 5;
+ test/samples/example-lin.opb view
@@ -0,0 +1,10 @@+* #variable= 5 #constraint= 4+*+* this is a dummy instance+*+min: 1 x2 -1 x3 ;+1 x1 +4 x2 -2 x5 >= 2;+-1 x1 +4 x2 -2 x5 >= +3;+12345678901234567890 x4 +4 x3 >= 10;+* an equality constraint+2 x2 +3 x4 +2 x1 +3 x5 = 5;
+ test/samples/example-nlc-1.opb view
@@ -0,0 +1,9 @@+* #variable= 5 #constraint= 4 #product= 5 sizeproduct= 13+*+* this is a dummy instance+*+min: 1 x2 x3 -1 x3 ;+1 x1 +4 x1 ~x2 -2 x5 >= 2;+-1 x1 +4 x2 -2 x5 >= 3;+12345678901234567890 x4 +4 x3 >= 10;+2 x2 x3 +3 x4 ~x5 +2 ~x1 x2 +3 ~x1 x2 x3 ~x4 ~x5 = 5 ;
+ test/samples/example-nlc-2.opb view
@@ -0,0 +1,16 @@+* #variable= 6 #constraint= 3 #product= 9 sizeproduct= 18+*+* Factorization problem: find the smallest P such that P*Q=N+* P is a 3 bits number (x3 x2 x1)+* Q is a 3 bits number (x6 x5 x4)+* N=35+* +* minimize the value of P+min: +1 x1 +2 x2 +4 x3 ;+* P>=2 (to avoid trivial factorization)++1 x1 +2 x2 +4 x3 >=2;+* Q>=2 (to avoid trivial factorization)++1 x4 +2 x5 +4 x6 >=2;+*+* P*Q=N++1 x1 x4 +2 x1 x5 +4 x1 x6 +2 x2 x4 +4 x2 x5 +8 x2 x6 +4 x3 x4 +8 x3 x5 +16 x3 x6 = 35;
+ test/samples/example1-nohint.wbo view
@@ -0,0 +1,3 @@+soft: 6 ;+[2] +1 x1 >= 1 ;+[3] -1 x1 >= 0 ;
+ test/samples/example1-notop.wbo view
@@ -0,0 +1,4 @@+* #variable= 1 #constraint= 2 #soft= 2 mincost= 2 maxcost= 3 sumcost= 5+soft: ;+[2] +1 x1 >= 1 ;+[3] -1 x1 >= 0 ;
+ test/samples/example1.wbo view
@@ -0,0 +1,4 @@+* #variable= 1 #constraint= 2 #soft= 2 mincost= 2 maxcost= 3 sumcost= 5+soft: 6 ;+[2] +1 x1 >= 1 ;+[3] -1 x1 >= 0 ;
+ test/samples/example2.wbo view
@@ -0,0 +1,5 @@+* #variable= 2 #constraint= 3 #soft= 2 mincost= 2 maxcost= 3 sumcost= 5+soft: 6 ;+[2] +1 x1 >= 1 ;+[3] +1 x2 >= 1 ;+-1 x1 -1 x2 >= -1 ;
+ test/samples/example3.wbo view
@@ -0,0 +1,8 @@+* #variable= 4 #constraint= 6 #soft= 4 mincost= 2 maxcost= 5 sumcost= 14+soft: 6 ;+[2] +1 x1 >= 1;+[3] +1 x2 >= 1;+[4] +1 x3 >= 1;+[5] +1 x4 >= 1;+-1 x1 -1 x2 >= -1 ;+-1 x3 -1 x4 >= -1 ;
+ test/samples/normalized-mds_50_10_4.opb view
@@ -0,0 +1,57 @@+* #variable= 50 #constraint= 50 #product= 614 sizeproduct= 1228+****************************************+* begin normalizer comments+* category= OPT-SMALLINT-NLC+* end normalizer comments+****************************************+min: +1 x1 +1 x2 +1 x3 +1 x4 +1 x5 +1 x6 +1 x7 +1 x8 +1 x9 +1 x10 +1 x11 +1 x12 +1 x13 +1 x14 +1 x15 +1 x16 +1 x17 +1 x18 +1 x19 +1 x20 +1 x21 +1 x22 +1 x23 +1 x24 +1 x25 +1 x26 +1 x27 +1 x28 +1 x29 +1 x30 +1 x31 +1 x32 +1 x33 +1 x34 +1 x35 +1 x36 +1 x37 +1 x38 +1 x39 +1 x40 +1 x41 +1 x42 +1 x43 +1 x44 +1 x45 +1 x46 +1 x47 +1 x48 +1 x49 +1 x50 ;++1 ~x1 x2 +1 ~x1 x34 +1 ~x1 x25 +1 ~x1 x27 +1 ~x1 x14 +1 ~x1 x38 +1 ~x1 x26 +1 ~x1 x29 +1 ~x1 x36 +1 ~x1 x45 +1 ~x1 x8 +1 ~x1 x9 +1 ~x1 x17 +1 ~x1 x46 +1 x1 >= 1 ;++1 x1 ~x2 +1 ~x2 x5 +1 ~x2 x15 +1 ~x2 x4 +1 ~x2 x3 +1 ~x2 x42 +1 ~x2 x50 +1 ~x2 x18 +1 ~x2 x19 +1 ~x2 x30 +1 ~x2 x12 +1 ~x2 x16 +1 ~x2 x20 +1 ~x2 x24 +1 ~x2 x40 +1 ~x2 x48 +1 x2 >= 1 ;++1 x2 ~x3 +1 ~x3 x24 +1 ~x3 x19 +1 ~x3 x23 +1 ~x3 x33 +1 ~x3 x21 +1 ~x3 x31 +1 ~x3 x5 +1 ~x3 x7 +1 ~x3 x50 +1 ~x3 x8 +1 ~x3 x11 +1 ~x3 x14 +1 ~x3 x26 +1 ~x3 x41 +1 ~x3 x43 +1 x3 >= 1 ;++1 x2 ~x4 +1 ~x4 x20 +1 ~x4 x45 +1 ~x4 x25 +1 ~x4 x34 +1 ~x4 x23 +1 ~x4 x12 +1 ~x4 x30 +1 ~x4 x27 +1 ~x4 x26 +1 ~x4 x38 +1 ~x4 x43 +1 ~x4 x44 +1 ~x4 x49 +1 x4 >= 1 ;++1 x2 ~x5 +1 x3 ~x5 +1 ~x5 x45 +1 ~x5 x32 +1 ~x5 x43 +1 ~x5 x49 +1 ~x5 x23 +1 ~x5 x44 +1 ~x5 x48 +1 ~x5 x40 +1 ~x5 x6 +1 ~x5 x14 +1 ~x5 x17 +1 ~x5 x27 +1 ~x5 x29 +1 x5 >= 1 ;++1 x5 ~x6 +1 ~x6 x48 +1 ~x6 x18 +1 ~x6 x22 +1 ~x6 x23 +1 ~x6 x37 +1 ~x6 x46 +1 ~x6 x7 +1 ~x6 x17 +1 ~x6 x38 +1 ~x6 x9 +1 ~x6 x14 +1 ~x6 x19 +1 ~x6 x25 +1 ~x6 x49 +1 ~x6 x50 +1 x6 >= 1 ;++1 x3 ~x7 +1 x6 ~x7 +1 ~x7 x32 +1 ~x7 x23 +1 ~x7 x44 +1 ~x7 x42 +1 ~x7 x40 +1 ~x7 x8 +1 ~x7 x27 +1 ~x7 x12 +1 ~x7 x9 +1 ~x7 x10 +1 ~x7 x16 +1 ~x7 x25 +1 ~x7 x36 +1 ~x7 x45 +1 x7 >= 1 ;++1 x1 ~x8 +1 x3 ~x8 +1 x7 ~x8 +1 ~x8 x20 +1 ~x8 x41 +1 ~x8 x47 +1 ~x8 x24 +1 ~x8 x39 +1 ~x8 x34 +1 ~x8 x50 +1 ~x8 x22 +1 x8 >= 1 ;++1 x1 ~x9 +1 x6 ~x9 +1 x7 ~x9 +1 ~x9 x38 +1 ~x9 x33 +1 ~x9 x18 +1 ~x9 x11 +1 ~x9 x12 +1 ~x9 x14 +1 ~x9 x25 +1 ~x9 x24 +1 ~x9 x28 +1 ~x9 x29 +1 ~x9 x32 +1 ~x9 x34 +1 ~x9 x45 +1 x9 >= 1 ;++1 x7 ~x10 +1 ~x10 x45 +1 ~x10 x49 +1 ~x10 x47 +1 ~x10 x28 +1 ~x10 x40 +1 ~x10 x36 +1 ~x10 x17 +1 ~x10 x50 +1 ~x10 x25 +1 ~x10 x15 +1 ~x10 x16 +1 ~x10 x18 +1 x10 >= 1 ;++1 x3 ~x11 +1 x9 ~x11 +1 ~x11 x42 +1 ~x11 x27 +1 ~x11 x15 +1 ~x11 x44 +1 ~x11 x29 +1 ~x11 x13 +1 ~x11 x28 +1 ~x11 x12 +1 ~x11 x22 +1 ~x11 x24 +1 ~x11 x36 +1 ~x11 x50 +1 x11 >= 1 ;++1 x2 ~x12 +1 x4 ~x12 +1 x7 ~x12 +1 x9 ~x12 +1 x11 ~x12 +1 ~x12 x47 +1 ~x12 x15 +1 ~x12 x17 +1 ~x12 x21 +1 ~x12 x30 +1 ~x12 x13 +1 ~x12 x48 +1 x12 >= 1 ;++1 x11 ~x13 +1 x12 ~x13 +1 ~x13 x15 +1 ~x13 x47 +1 ~x13 x31 +1 ~x13 x45 +1 ~x13 x27 +1 ~x13 x39 +1 ~x13 x35 +1 ~x13 x14 +1 ~x13 x20 +1 ~x13 x22 +1 ~x13 x42 +1 x13 >= 1 ;++1 x1 ~x14 +1 x3 ~x14 +1 x5 ~x14 +1 x6 ~x14 +1 x9 ~x14 +1 x13 ~x14 +1 ~x14 x26 +1 ~x14 x34 +1 ~x14 x27 +1 ~x14 x39 +1 ~x14 x21 +1 ~x14 x25 +1 x14 >= 1 ;++1 x2 ~x15 +1 x10 ~x15 +1 x11 ~x15 +1 x12 ~x15 +1 x13 ~x15 +1 ~x15 x21 +1 ~x15 x32 +1 ~x15 x33 +1 ~x15 x35 +1 ~x15 x37 +1 ~x15 x17 +1 ~x15 x23 +1 ~x15 x38 +1 ~x15 x46 +1 x15 >= 1 ;++1 x2 ~x16 +1 x7 ~x16 +1 x10 ~x16 +1 ~x16 x21 +1 ~x16 x37 +1 ~x16 x24 +1 ~x16 x19 +1 ~x16 x27 +1 ~x16 x49 +1 ~x16 x38 +1 ~x16 x20 +1 ~x16 x26 +1 ~x16 x30 +1 ~x16 x35 +1 ~x16 x36 +1 ~x16 x45 +1 x16 >= 1 ;++1 x1 ~x17 +1 x5 ~x17 +1 x6 ~x17 +1 x10 ~x17 +1 x12 ~x17 +1 x15 ~x17 +1 ~x17 x27 +1 ~x17 x28 +1 ~x17 x40 +1 ~x17 x39 +1 ~x17 x18 +1 x17 >= 1 ;++1 x2 ~x18 +1 x6 ~x18 +1 x9 ~x18 +1 x10 ~x18 +1 x17 ~x18 +1 ~x18 x33 +1 ~x18 x27 +1 ~x18 x37 +1 ~x18 x32 +1 ~x18 x19 +1 ~x18 x24 +1 ~x18 x31 +1 ~x18 x42 +1 ~x18 x44 +1 x18 >= 1 ;++1 x2 ~x19 +1 x3 ~x19 +1 x6 ~x19 +1 x16 ~x19 +1 x18 ~x19 +1 ~x19 x20 +1 ~x19 x29 +1 ~x19 x40 +1 ~x19 x37 +1 ~x19 x46 +1 ~x19 x21 +1 ~x19 x24 +1 ~x19 x33 +1 ~x19 x43 +1 x19 >= 1 ;++1 x2 ~x20 +1 x4 ~x20 +1 x8 ~x20 +1 x13 ~x20 +1 x16 ~x20 +1 x19 ~x20 +1 ~x20 x30 +1 ~x20 x47 +1 ~x20 x24 +1 ~x20 x23 +1 ~x20 x21 +1 ~x20 x29 +1 ~x20 x36 +1 ~x20 x44 +1 x20 >= 1 ;++1 x3 ~x21 +1 x12 ~x21 +1 x14 ~x21 +1 x15 ~x21 +1 x16 ~x21 +1 x19 ~x21 +1 x20 ~x21 +1 ~x21 x41 +1 ~x21 x48 +1 ~x21 x25 +1 ~x21 x28 +1 ~x21 x29 +1 x21 >= 1 ;++1 x6 ~x22 +1 x8 ~x22 +1 x11 ~x22 +1 x13 ~x22 +1 ~x22 x36 +1 ~x22 x30 +1 ~x22 x44 +1 ~x22 x29 +1 ~x22 x43 +1 ~x22 x32 +1 ~x22 x31 +1 x22 >= 1 ;++1 x3 ~x23 +1 x4 ~x23 +1 x5 ~x23 +1 x6 ~x23 +1 x7 ~x23 +1 x15 ~x23 +1 x20 ~x23 +1 ~x23 x35 +1 ~x23 x31 +1 ~x23 x39 +1 x23 >= 1 ;++1 x2 ~x24 +1 x3 ~x24 +1 x8 ~x24 +1 x9 ~x24 +1 x11 ~x24 +1 x16 ~x24 +1 x18 ~x24 +1 x19 ~x24 +1 x20 ~x24 +1 ~x24 x28 +1 ~x24 x38 +1 ~x24 x39 +1 x24 >= 1 ;++1 x1 ~x25 +1 x4 ~x25 +1 x6 ~x25 +1 x7 ~x25 +1 x9 ~x25 +1 x10 ~x25 +1 x14 ~x25 +1 x21 ~x25 +1 ~x25 x37 +1 ~x25 x33 +1 ~x25 x34 +1 ~x25 x35 +1 ~x25 x40 +1 ~x25 x42 +1 x25 >= 1 ;++1 x1 ~x26 +1 x3 ~x26 +1 x4 ~x26 +1 x14 ~x26 +1 x16 ~x26 +1 ~x26 x46 +1 ~x26 x31 +1 ~x26 x41 +1 ~x26 x38 +1 ~x26 x47 +1 ~x26 x28 +1 ~x26 x50 +1 x26 >= 1 ;++1 x1 ~x27 +1 x4 ~x27 +1 x5 ~x27 +1 x7 ~x27 +1 x11 ~x27 +1 x13 ~x27 +1 x14 ~x27 +1 x16 ~x27 +1 x17 ~x27 +1 x18 ~x27 +1 ~x27 x43 +1 x27 >= 1 ;++1 x9 ~x28 +1 x10 ~x28 +1 x11 ~x28 +1 x17 ~x28 +1 x21 ~x28 +1 x24 ~x28 +1 x26 ~x28 +1 ~x28 x32 +1 ~x28 x46 +1 ~x28 x38 +1 ~x28 x31 +1 ~x28 x34 +1 x28 >= 1 ;++1 x1 ~x29 +1 x5 ~x29 +1 x9 ~x29 +1 x11 ~x29 +1 x19 ~x29 +1 x20 ~x29 +1 x21 ~x29 +1 x22 ~x29 +1 ~x29 x40 +1 ~x29 x49 +1 ~x29 x30 +1 ~x29 x33 +1 x29 >= 1 ;++1 x2 ~x30 +1 x4 ~x30 +1 x12 ~x30 +1 x16 ~x30 +1 x20 ~x30 +1 x22 ~x30 +1 x29 ~x30 +1 ~x30 x31 +1 ~x30 x47 +1 ~x30 x39 +1 x30 >= 1 ;++1 x3 ~x31 +1 x13 ~x31 +1 x18 ~x31 +1 x22 ~x31 +1 x23 ~x31 +1 x26 ~x31 +1 x28 ~x31 +1 x30 ~x31 +1 ~x31 x35 +1 ~x31 x41 +1 ~x31 x32 +1 ~x31 x45 +1 ~x31 x50 +1 x31 >= 1 ;++1 x5 ~x32 +1 x7 ~x32 +1 x9 ~x32 +1 x15 ~x32 +1 x18 ~x32 +1 x22 ~x32 +1 x28 ~x32 +1 x31 ~x32 +1 ~x32 x35 +1 ~x32 x42 +1 ~x32 x36 +1 ~x32 x47 +1 x32 >= 1 ;++1 x3 ~x33 +1 x9 ~x33 +1 x15 ~x33 +1 x18 ~x33 +1 x19 ~x33 +1 x25 ~x33 +1 x29 ~x33 +1 ~x33 x42 +1 ~x33 x49 +1 ~x33 x39 +1 x33 >= 1 ;++1 x1 ~x34 +1 x4 ~x34 +1 x8 ~x34 +1 x9 ~x34 +1 x14 ~x34 +1 x25 ~x34 +1 x28 ~x34 +1 ~x34 x49 +1 ~x34 x43 +1 ~x34 x48 +1 ~x34 x35 +1 x34 >= 1 ;++1 x13 ~x35 +1 x15 ~x35 +1 x16 ~x35 +1 x23 ~x35 +1 x25 ~x35 +1 x31 ~x35 +1 x32 ~x35 +1 x34 ~x35 +1 ~x35 x37 +1 ~x35 x49 +1 x35 >= 1 ;++1 x1 ~x36 +1 x7 ~x36 +1 x10 ~x36 +1 x11 ~x36 +1 x16 ~x36 +1 x20 ~x36 +1 x22 ~x36 +1 x32 ~x36 +1 ~x36 x37 +1 ~x36 x39 +1 ~x36 x38 +1 ~x36 x48 +1 x36 >= 1 ;++1 x6 ~x37 +1 x15 ~x37 +1 x16 ~x37 +1 x18 ~x37 +1 x19 ~x37 +1 x25 ~x37 +1 x35 ~x37 +1 x36 ~x37 +1 ~x37 x41 +1 ~x37 x42 +1 ~x37 x44 +1 ~x37 x48 +1 x37 >= 1 ;++1 x1 ~x38 +1 x4 ~x38 +1 x6 ~x38 +1 x9 ~x38 +1 x15 ~x38 +1 x16 ~x38 +1 x24 ~x38 +1 x26 ~x38 +1 x28 ~x38 +1 x36 ~x38 +1 x38 >= 1 ;++1 x8 ~x39 +1 x13 ~x39 +1 x14 ~x39 +1 x17 ~x39 +1 x23 ~x39 +1 x24 ~x39 +1 x30 ~x39 +1 x33 ~x39 +1 x36 ~x39 +1 ~x39 x43 +1 ~x39 x46 +1 x39 >= 1 ;++1 x2 ~x40 +1 x5 ~x40 +1 x7 ~x40 +1 x10 ~x40 +1 x17 ~x40 +1 x19 ~x40 +1 x25 ~x40 +1 x29 ~x40 +1 ~x40 x43 +1 ~x40 x49 +1 ~x40 x41 +1 ~x40 x46 +1 ~x40 x47 +1 x40 >= 1 ;++1 x3 ~x41 +1 x8 ~x41 +1 x21 ~x41 +1 x26 ~x41 +1 x31 ~x41 +1 x37 ~x41 +1 x40 ~x41 +1 ~x41 x50 +1 ~x41 x44 +1 ~x41 x47 +1 ~x41 x45 +1 x41 >= 1 ;++1 x2 ~x42 +1 x7 ~x42 +1 x11 ~x42 +1 x13 ~x42 +1 x18 ~x42 +1 x25 ~x42 +1 x32 ~x42 +1 x33 ~x42 +1 x37 ~x42 +1 ~x42 x48 +1 ~x42 x46 +1 x42 >= 1 ;++1 x3 ~x43 +1 x4 ~x43 +1 x5 ~x43 +1 x19 ~x43 +1 x22 ~x43 +1 x27 ~x43 +1 x34 ~x43 +1 x39 ~x43 +1 x40 ~x43 +1 ~x43 x44 +1 x43 >= 1 ;++1 x4 ~x44 +1 x5 ~x44 +1 x7 ~x44 +1 x11 ~x44 +1 x18 ~x44 +1 x20 ~x44 +1 x22 ~x44 +1 x37 ~x44 +1 x41 ~x44 +1 x43 ~x44 +1 x44 >= 1 ;++1 x1 ~x45 +1 x4 ~x45 +1 x5 ~x45 +1 x7 ~x45 +1 x9 ~x45 +1 x10 ~x45 +1 x13 ~x45 +1 x16 ~x45 +1 x31 ~x45 +1 x41 ~x45 +1 ~x45 x46 +1 x45 >= 1 ;++1 x1 ~x46 +1 x6 ~x46 +1 x15 ~x46 +1 x19 ~x46 +1 x26 ~x46 +1 x28 ~x46 +1 x39 ~x46 +1 x40 ~x46 +1 x42 ~x46 +1 x45 ~x46 +1 x46 >= 1 ;++1 x8 ~x47 +1 x10 ~x47 +1 x12 ~x47 +1 x13 ~x47 +1 x20 ~x47 +1 x26 ~x47 +1 x30 ~x47 +1 x32 ~x47 +1 x40 ~x47 +1 x41 ~x47 +1 x47 >= 1 ;++1 x2 ~x48 +1 x5 ~x48 +1 x6 ~x48 +1 x12 ~x48 +1 x21 ~x48 +1 x34 ~x48 +1 x36 ~x48 +1 x37 ~x48 +1 x42 ~x48 +1 ~x48 x50 +1 x48 >= 1 ;++1 x4 ~x49 +1 x5 ~x49 +1 x6 ~x49 +1 x10 ~x49 +1 x16 ~x49 +1 x29 ~x49 +1 x33 ~x49 +1 x34 ~x49 +1 x35 ~x49 +1 x40 ~x49 +1 x49 >= 1 ;++1 x2 ~x50 +1 x3 ~x50 +1 x6 ~x50 +1 x8 ~x50 +1 x10 ~x50 +1 x11 ~x50 +1 x26 ~x50 +1 x31 ~x50 +1 x41 ~x50 +1 x48 ~x50 +1 x50 >= 1 ;
+ test/samples/normalized-opt-market-split_4_30_2.opb view
@@ -0,0 +1,15 @@+* #variable= 94 #constraint= 8+****************************************+* begin normalizer comments+* category= OPT-SMALLINT+* end normalizer comments+****************************************+min: +1 x1 +2 x2 +4 x3 +8 x4 +16 x5 +32 x6 +64 x7 +128 x8 +1 x9 +2 x10 +4 x11 +8 x12 +16 x13 +32 x14 +64 x15 +128 x16 +1 x17 +2 x18 +4 x19 +8 x20 +16 x21 +32 x22 +64 x23 +128 x24 +1 x25 +2 x26 +4 x27 +8 x28 +16 x29 +32 x30 +64 x31 +128 x32 +1 x33 +2 x34 +4 x35 +8 x36 +16 x37 +32 x38 +64 x39 +128 x40 +1 x41 +2 x42 +4 x43 +8 x44 +16 x45 +32 x46 +64 x47 +128 x48 +1 x49 +2 x50 +4 x51 +8 x52 +16 x53 +32 x54 +64 x55 +128 x56 +1 x57 +2 x58 +4 x59 +8 x60 +16 x61 +32 x62 +64 x63 +128 x64 ;+-1 x49 -2 x50 -4 x51 -8 x52 -16 x53 -32 x54 -64 x55 -128 x56 +1 x57 +2 x58 +4 x59 +8 x60 +16 x61 +32 x62 +64 x63 +128 x64 -48 x65 -71 x66 -5 x67 -77 x68 -43 x70 -23 x71 -3 x72 -6 x73 -47 x74 -17 x75 -56 x76 -17 x77 -67 x78 -70 x79 -67 x80 -93 x81 -99 x82 -5 x83 -9 x84 -86 x85 -46 x86 -96 x87 -61 x88 -86 x89 -75 x90 -55 x91 -41 x92 -3 x93 -1 x94 >= -686 ;++1 x49 +2 x50 +4 x51 +8 x52 +16 x53 +32 x54 +64 x55 +128 x56 -1 x57 -2 x58 -4 x59 -8 x60 -16 x61 -32 x62 -64 x63 -128 x64 +48 x65 +71 x66 +5 x67 +77 x68 +43 x70 +23 x71 +3 x72 +6 x73 +47 x74 +17 x75 +56 x76 +17 x77 +67 x78 +70 x79 +67 x80 +93 x81 +99 x82 +5 x83 +9 x84 +86 x85 +46 x86 +96 x87 +61 x88 +86 x89 +75 x90 +55 x91 +41 x92 +3 x93 +1 x94 >= 686 ;+-1 x33 -2 x34 -4 x35 -8 x36 -16 x37 -32 x38 -64 x39 -128 x40 +1 x41 +2 x42 +4 x43 +8 x44 +16 x45 +32 x46 +64 x47 +128 x48 -77 x65 -16 x66 -29 x67 -77 x68 -86 x69 -46 x70 -3 x71 -11 x72 -72 x73 -62 x74 -49 x75 -70 x76 -50 x77 -14 x78 -97 x79 -73 x80 -29 x81 -38 x82 -16 x83 -34 x84 -89 x85 -86 x86 -23 x87 -87 x88 -27 x89 -41 x90 -55 x91 -76 x92 -94 x93 -89 x94 >= -808 ;++1 x33 +2 x34 +4 x35 +8 x36 +16 x37 +32 x38 +64 x39 +128 x40 -1 x41 -2 x42 -4 x43 -8 x44 -16 x45 -32 x46 -64 x47 -128 x48 +77 x65 +16 x66 +29 x67 +77 x68 +86 x69 +46 x70 +3 x71 +11 x72 +72 x73 +62 x74 +49 x75 +70 x76 +50 x77 +14 x78 +97 x79 +73 x80 +29 x81 +38 x82 +16 x83 +34 x84 +89 x85 +86 x86 +23 x87 +87 x88 +27 x89 +41 x90 +55 x91 +76 x92 +94 x93 +89 x94 >= 808 ;+-1 x17 -2 x18 -4 x19 -8 x20 -16 x21 -32 x22 -64 x23 -128 x24 +1 x25 +2 x26 +4 x27 +8 x28 +16 x29 +32 x30 +64 x31 +128 x32 -30 x65 -57 x66 -70 x68 -17 x69 -74 x70 -73 x71 -74 x72 -58 x73 -86 x74 -46 x75 -36 x76 -13 x77 -27 x78 -23 x79 -14 x80 -89 x81 -91 x82 -5 x83 -50 x84 -18 x85 -37 x86 -98 x87 -40 x88 -66 x89 -15 x90 -49 x91 -34 x93 -20 x94 >= -655 ;++1 x17 +2 x18 +4 x19 +8 x20 +16 x21 +32 x22 +64 x23 +128 x24 -1 x25 -2 x26 -4 x27 -8 x28 -16 x29 -32 x30 -64 x31 -128 x32 +30 x65 +57 x66 +70 x68 +17 x69 +74 x70 +73 x71 +74 x72 +58 x73 +86 x74 +46 x75 +36 x76 +13 x77 +27 x78 +23 x79 +14 x80 +89 x81 +91 x82 +5 x83 +50 x84 +18 x85 +37 x86 +98 x87 +40 x88 +66 x89 +15 x90 +49 x91 +34 x93 +20 x94 >= 655 ;+-1 x1 -2 x2 -4 x3 -8 x4 -16 x5 -32 x6 -64 x7 -128 x8 +1 x9 +2 x10 +4 x11 +8 x12 +16 x13 +32 x14 +64 x15 +128 x16 -86 x65 -23 x66 -88 x67 -8 x68 -22 x69 -51 x70 -57 x71 -84 x72 -60 x73 -20 x74 -25 x75 -27 x76 -80 x77 -87 x78 -49 x79 -62 x80 -15 x81 -91 x82 -9 x83 -27 x84 -31 x85 -96 x86 -70 x87 -77 x88 -65 x89 -56 x90 -82 x91 -18 x92 -71 x93 -24 x94 >= -780 ;++1 x1 +2 x2 +4 x3 +8 x4 +16 x5 +32 x6 +64 x7 +128 x8 -1 x9 -2 x10 -4 x11 -8 x12 -16 x13 -32 x14 -64 x15 -128 x16 +86 x65 +23 x66 +88 x67 +8 x68 +22 x69 +51 x70 +57 x71 +84 x72 +60 x73 +20 x74 +25 x75 +27 x76 +80 x77 +87 x78 +49 x79 +62 x80 +15 x81 +91 x82 +9 x83 +27 x84 +31 x85 +96 x86 +70 x87 +77 x88 +65 x89 +56 x90 +82 x91 +18 x92 +71 x93 +24 x94 >= 780 ;
+ test/samples/pigeonhole_5_4.opb view
@@ -0,0 +1,10 @@+* #variable= 20 #constraint= 9++1 x1 +1 x2 +1 x3 +1 x4 >= 1;++1 x5 +1 x6 +1 x7 +1 x8 >= 1;++1 x9 +1 x10 +1 x11 +1 x12 >= 1;++1 x13 +1 x14 +1 x15 +1 x16 >= 1;++1 x17 +1 x18 +1 x19 +1 x20 >= 1;+-1 x1 -1 x5 -1 x9 -1 x13 -1 x17 >= -1;+-1 x2 -1 x6 -1 x10 -1 x14 -1 x18 >= -1;+-1 x3 -1 x7 -1 x11 -1 x15 -1 x19 >= -1;+-1 x4 -1 x8 -1 x12 -1 x16 -1 x20 >= -1;