diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -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)
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/pseudo-boolean.cabal b/pseudo-boolean.cabal
new file mode 100644
--- /dev/null
+++ b/pseudo-boolean.cabal
@@ -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
diff --git a/src/Data/PseudoBoolean.hs b/src/Data/PseudoBoolean.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PseudoBoolean.hs
@@ -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.
diff --git a/src/Data/PseudoBoolean/Attoparsec.hs b/src/Data/PseudoBoolean/Attoparsec.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PseudoBoolean/Attoparsec.hs
@@ -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)
diff --git a/src/Data/PseudoBoolean/Builder.hs b/src/Data/PseudoBoolean/Builder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PseudoBoolean/Builder.hs
@@ -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) ""
diff --git a/src/Data/PseudoBoolean/ByteStringBuilder.hs b/src/Data/PseudoBoolean/ByteStringBuilder.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PseudoBoolean/ByteStringBuilder.hs
@@ -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)
diff --git a/src/Data/PseudoBoolean/Internal/TextUtil.hs b/src/Data/PseudoBoolean/Internal/TextUtil.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PseudoBoolean/Internal/TextUtil.hs
@@ -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
diff --git a/src/Data/PseudoBoolean/Parsec.hs b/src/Data/PseudoBoolean/Parsec.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PseudoBoolean/Parsec.hs
@@ -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
diff --git a/src/Data/PseudoBoolean/Types.hs b/src/Data/PseudoBoolean/Types.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/PseudoBoolean/Types.hs
@@ -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
diff --git a/test/TestPBFile.hs b/test/TestPBFile.hs
new file mode 100644
--- /dev/null
+++ b/test/TestPBFile.hs
@@ -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)
diff --git a/test/samples/example-lin-nohint.opb b/test/samples/example-lin-nohint.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/example-lin-nohint.opb
@@ -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;
diff --git a/test/samples/example-lin-pbs.opb b/test/samples/example-lin-pbs.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/example-lin-pbs.opb
@@ -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;
diff --git a/test/samples/example-lin.opb b/test/samples/example-lin.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/example-lin.opb
@@ -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;
diff --git a/test/samples/example-nlc-1.opb b/test/samples/example-nlc-1.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/example-nlc-1.opb
@@ -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 ;
diff --git a/test/samples/example-nlc-2.opb b/test/samples/example-nlc-2.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/example-nlc-2.opb
@@ -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;
diff --git a/test/samples/example1-nohint.wbo b/test/samples/example1-nohint.wbo
new file mode 100644
--- /dev/null
+++ b/test/samples/example1-nohint.wbo
@@ -0,0 +1,3 @@
+soft: 6 ;
+[2] +1 x1 >= 1 ;
+[3] -1 x1 >= 0 ;
diff --git a/test/samples/example1-notop.wbo b/test/samples/example1-notop.wbo
new file mode 100644
--- /dev/null
+++ b/test/samples/example1-notop.wbo
@@ -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 ;
diff --git a/test/samples/example1.wbo b/test/samples/example1.wbo
new file mode 100644
--- /dev/null
+++ b/test/samples/example1.wbo
@@ -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 ;
diff --git a/test/samples/example2.wbo b/test/samples/example2.wbo
new file mode 100644
--- /dev/null
+++ b/test/samples/example2.wbo
@@ -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 ;
diff --git a/test/samples/example3.wbo b/test/samples/example3.wbo
new file mode 100644
--- /dev/null
+++ b/test/samples/example3.wbo
@@ -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 ;
diff --git a/test/samples/normalized-mds_50_10_4.opb b/test/samples/normalized-mds_50_10_4.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/normalized-mds_50_10_4.opb
@@ -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 ;
diff --git a/test/samples/normalized-opt-market-split_4_30_2.opb b/test/samples/normalized-opt-market-split_4_30_2.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/normalized-opt-market-split_4_30_2.opb
@@ -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 ;
diff --git a/test/samples/pigeonhole_5_4.opb b/test/samples/pigeonhole_5_4.opb
new file mode 100644
--- /dev/null
+++ b/test/samples/pigeonhole_5_4.opb
@@ -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;