Merge pull request #71 from msakai/feature/pb-parser-megaparsec

Use megaparsec as default PB parser and add --pb-fast-parser option to use attoparsec
msakai · Oct 11, 2021 · 5511fa3 · 5511fa3
2 parents a8554b6 + 44f11b5
commit 5511fa3
Show file tree

Hide file tree

Showing 4 changed files with 90 additions and 13 deletions.
diff --git a/app/toyconvert.hs b/app/toyconvert.hs
@@ -64,6 +64,7 @@ data Options = Options
   , optFileEncoding :: Maybe String
   , optRemoveUserCuts :: Bool
   , optNewWCNF :: Bool
+  , optPBFastParser :: Bool
   } deriving (Eq, Show)
 
 optionsParser :: Parser Options
@@ -84,6 +85,7 @@ optionsParser = Options
   <*> encodingOption
   <*> removeUserCutsOption
   <*> newWCNFOption
+  <*> pbFastParserOption
   where
     fileInput :: Parser FilePath
     fileInput = argument str (metavar "FILE")
@@ -184,6 +186,11 @@ optionsParser = Options
       $  long "wcnf-new"
       <> help "use new format for writing WCNF files"
 
+    pbFastParserOption :: Parser Bool
+    pbFastParserOption = switch
+      $  long "pb-fast-parser"
+      <> help "use attoparsec-based parser instead of megaparsec-based one for speed"
+
 parserInfo :: ParserInfo Options
 parserInfo = info (helper <*> versionOption <*> optionsParser)
   $  fullDesc
@@ -222,8 +229,16 @@ readProblem o fname = do
           liftM (ProbOPB . fst . sat2pb) $ FF.readFile fname
     ".wcnf" ->
       liftM (ProbWBO . fst . maxsat2wbo) $ FF.readFile fname
-    ".opb"  -> liftM ProbOPB $ FF.readFile fname
-    ".wbo"  -> liftM ProbWBO $ FF.readFile fname
+    ".opb"  -> liftM ProbOPB $ do
+      if optPBFastParser o then
+        liftM FF.unWithFastParser $ FF.readFile fname
+      else
+        FF.readFile fname
+    ".wbo"  -> liftM ProbWBO $ do
+      if optPBFastParser o then
+        liftM FF.unWithFastParser $ FF.readFile fname
+      else
+        FF.readFile fname
     ".gcnf" ->
       liftM (ProbWBO . fst . maxsat2wbo . fst . gcnf2maxsat) $ FF.readFile fname
     ".lp"   -> ProbMIP <$> MIP.readLPFile def{ MIP.optFileEncoding = enc } fname

diff --git a/app/toysat/toysat.hs b/app/toysat/toysat.hs
@@ -104,6 +104,7 @@ data Options
   , optTempDir :: Maybe FilePath
   , optFileEncoding :: Maybe String
   , optMaxSATCompactVLine :: Bool
+  , optPBFastParser :: Bool
   }
 
 instance Default Options where
@@ -127,6 +128,7 @@ instance Default Options where
     , optTempDir = Nothing
     , optFileEncoding = Nothing
     , optMaxSATCompactVLine = False
+    , optPBFastParser = False
     }
 
 optionsParser :: Parser Options
@@ -149,6 +151,7 @@ optionsParser = Options
   <*> tempDirOption
   <*> fileEncodingOption
   <*> maxsatCompactVLineOption
+  <*> pbFastParserOption
   where
     fileInput :: Parser String
     fileInput = strArgument $ metavar "(FILE|-)"
@@ -251,6 +254,10 @@ optionsParser = Options
       $  long "maxsat-compact-v-line"
       <> help "print Max-SAT solution in the new compact v-line format"
 
+    pbFastParserOption = switch
+      $  long "pb-fast-parser"
+      <> help "use attoparsec-based parser instead of megaparsec-based one for speed"
+
 
 satConfigParser :: Parser SAT.Config
 satConfigParser = SAT.Config
@@ -783,8 +790,16 @@ solveMUS opt solver gcnf = do
 mainPB :: Options -> SAT.Solver -> IO ()
 mainPB opt solver = do
   ret <- case optInput opt of
-           "-"   -> liftM FF.parse BS.getContents
-           fname -> FF.parseFile fname
+           "-"   ->
+             if optPBFastParser opt then
+               liftM (fmap FF.unWithFastParser . FF.parse) BS.getContents
+             else
+               liftM FF.parse BS.getContents
+           fname ->
+             if optPBFastParser opt then
+               liftM (fmap FF.unWithFastParser) $ FF.parseFile fname
+             else
+               FF.parseFile fname
   case ret of
     Left err -> hPutStrLn stderr err >> exitFailure
     Right formula -> solvePB opt solver formula
@@ -901,8 +916,16 @@ setupOptimizer pbo opt = do
 mainWBO :: Options -> SAT.Solver -> IO ()
 mainWBO opt solver = do
   ret <- case optInput opt of
-           "-"   -> liftM FF.parse BS.getContents
-           fname -> FF.parseFile fname
+           "-"   ->
+             if optPBFastParser opt then
+               liftM (fmap FF.unWithFastParser . FF.parse) BS.getContents
+             else
+               liftM FF.parse BS.getContents
+           fname ->
+             if optPBFastParser opt then
+               liftM (fmap FF.unWithFastParser) $ FF.parseFile fname
+             else
+               FF.parseFile fname
   case ret of
     Left err -> hPutStrLn stderr err >> exitFailure
     Right formula -> solveWBO opt solver False formula

diff --git a/app/toysolver.hs b/app/toysolver.hs
@@ -78,6 +78,7 @@ data Options = Options
   , optOmegaReal :: String
   , optFileEncoding :: Maybe String
   , optMaxSATCompactVLine :: Bool
+  , optPBFastParser :: Bool
   } deriving (Eq, Show)
 
 optionsParser :: Parser Options
@@ -94,6 +95,7 @@ optionsParser = Options
   <*> omegaRealOption
   <*> fileEncodingOption
   <*> maxsatCompactVLineOption
+  <*> pbFastParserOption
   where
     fileInput :: Parser FilePath
     fileInput = argument str (metavar "FILE")
@@ -170,6 +172,11 @@ optionsParser = Options
       $  long "maxsat-compact-v-line"
       <> help "print Max-SAT solution in the new compact v-line format"
 
+    pbFastParserOption :: Parser Bool
+    pbFastParserOption = switch
+      $  long "pb-fast-parser"
+      <> help "use attoparsec-based parser instead of megaparsec-based one for speed"
+
 parserInfo :: ParserInfo Options
 parserInfo = info (helper <*> versionOption <*> optionsParser)
   $  fullDesc
@@ -471,14 +478,22 @@ main = do
         satPrintModel stdout m2 0
         writeSOLFileSAT o m2
     ModePB -> do
-      pb <- FF.readFile (optInput o)
+      pb <-
+        if optPBFastParser o then
+          liftM FF.unWithFastParser $ FF.readFile (optInput o)
+        else
+          FF.readFile (optInput o)
       let (mip,info2) = pb2ip pb
       run (optSolver o) o (fmap fromInteger mip) $ \m -> do
         let m2 = transformBackward info2 m
         pbPrintModel stdout m2 0
         writeSOLFileSAT o m2
     ModeWBO -> do
-      wbo <- FF.readFile (optInput o)
+      wbo <-
+        if optPBFastParser o then
+          liftM FF.unWithFastParser $ FF.readFile (optInput o)
+        else
+          FF.readFile (optInput o)
       let (mip,info2) = wbo2ip False wbo
       run (optSolver o) o (fmap fromInteger mip) $ \m -> do
         let m2 = transformBackward info2 m

diff --git a/src/ToySolver/FileFormat.hs b/src/ToySolver/FileFormat.hs
@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -Wall -fno-warn-orphans #-}
+{-# LANGUAGE FlexibleInstances #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  ToySolver.FileFormat
@@ -7,24 +8,47 @@
 --
 -- Maintainer  :  masahiro.sakai@gmail.com
 -- Stability   :  provisional
--- Portability :  portable
+-- Portability :  non-portable
 --
 -----------------------------------------------------------------------------
 module ToySolver.FileFormat
   ( module ToySolver.FileFormat.Base
+  , WithFastParser (..)
   ) where
 
 import qualified Data.PseudoBoolean as PBFile
 import qualified Data.PseudoBoolean.Attoparsec as PBFileAttoparsec
+import qualified Data.PseudoBoolean.Megaparsec as PBFileMegaparsec
 import qualified Data.PseudoBoolean.ByteStringBuilder as PBFileBB
 import ToySolver.FileFormat.Base
 import ToySolver.FileFormat.CNF () -- importing instances
 import ToySolver.QUBO () -- importing instances
+import Text.Megaparsec.Error (errorBundlePretty)
 
 instance FileFormat PBFile.Formula where
-  parse = PBFileAttoparsec.parseOPBByteString
-  render = PBFileBB.opbBuilder
+  parse s =
+    case PBFileMegaparsec.parseOPBByteString "-" s of
+      Left err -> Left (errorBundlePretty err)
+      Right x -> Right x
+  render x = PBFileBB.opbBuilder x
 
 instance FileFormat PBFile.SoftFormula where
-  parse = PBFileAttoparsec.parseWBOByteString
-  render = PBFileBB.wboBuilder
+  parse s =
+    case PBFileMegaparsec.parseWBOByteString "-" s of
+      Left err -> Left (errorBundlePretty err)
+      Right x -> Right x
+  render x = PBFileBB.wboBuilder x
+
+-- | Wrapper type for parsing opb/wbo files using attoparsec-based parser instead of megaparsec-based one.
+newtype WithFastParser a
+  = WithFastParser
+  { unWithFastParser :: a
+  }
+
+instance FileFormat (WithFastParser PBFile.Formula) where
+  parse = fmap WithFastParser . PBFileAttoparsec.parseOPBByteString
+  render (WithFastParser x) = PBFileBB.opbBuilder x
+
+instance FileFormat (WithFastParser PBFile.SoftFormula) where
+  parse = fmap WithFastParser . PBFileAttoparsec.parseWBOByteString
+  render (WithFastParser x) = PBFileBB.wboBuilder x