From 023dd111a619cb2b20cf23a416ddfdd862bc821d Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Mon, 4 Oct 2021 09:11:10 +0900 Subject: [PATCH 1/2] add --pb-parser-megaparsec option to toysat, toysolver, and toyconvert --- app/toyconvert.hs | 19 +++++++++++++++++-- app/toysat/toysat.hs | 31 +++++++++++++++++++++++++++---- app/toysolver.hs | 19 +++++++++++++++++-- src/ToySolver/FileFormat.hs | 28 +++++++++++++++++++++++++++- 4 files changed, 88 insertions(+), 9 deletions(-) diff --git a/app/toyconvert.hs b/app/toyconvert.hs index 137c0a52..4684bc64 100644 --- a/app/toyconvert.hs +++ b/app/toyconvert.hs @@ -64,6 +64,7 @@ data Options = Options , optFileEncoding :: Maybe String , optRemoveUserCuts :: Bool , optNewWCNF :: Bool + , optPBParserMegaparsec :: Bool } deriving (Eq, Show) optionsParser :: Parser Options @@ -84,6 +85,7 @@ optionsParser = Options <*> encodingOption <*> removeUserCutsOption <*> newWCNFOption + <*> pbParserMegaparsecOption 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" + pbParserMegaparsecOption :: Parser Bool + pbParserMegaparsecOption = switch + $ long "pb-parser-megaparsec" + <> help "use megaparsec-based parser instead of attoparsec-based one for better error message" + 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 optPBParserMegaparsec o then + liftM FF.unWithMegaparsecParser $ FF.readFile fname + else + FF.readFile fname + ".wbo" -> liftM ProbWBO $ + if optPBParserMegaparsec o then + liftM FF.unWithMegaparsecParser $ 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 index d2a6e955..088b2ce4 100644 --- a/app/toysat/toysat.hs +++ b/app/toysat/toysat.hs @@ -104,6 +104,7 @@ data Options , optTempDir :: Maybe FilePath , optFileEncoding :: Maybe String , optMaxSATCompactVLine :: Bool + , optPBParserMegaparsec :: Bool } instance Default Options where @@ -127,6 +128,7 @@ instance Default Options where , optTempDir = Nothing , optFileEncoding = Nothing , optMaxSATCompactVLine = False + , optPBParserMegaparsec = False } optionsParser :: Parser Options @@ -149,6 +151,7 @@ optionsParser = Options <*> tempDirOption <*> fileEncodingOption <*> maxsatCompactVLineOption + <*> pbParserMegaparsecOption 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" + pbParserMegaparsecOption = switch + $ long "pb-parser-megaparsec" + <> help "use megaparsec-based parser instead of attoparsec-based one for better error message" + 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 optPBParserMegaparsec opt then + liftM (fmap FF.unWithMegaparsecParser . FF.parse) BS.getContents + else + liftM FF.parse BS.getContents + fname -> + if optPBParserMegaparsec opt then + liftM (fmap FF.unWithMegaparsecParser) $ 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 optPBParserMegaparsec opt then + liftM (fmap FF.unWithMegaparsecParser . FF.parse) BS.getContents + else + liftM FF.parse BS.getContents + fname -> + if optPBParserMegaparsec opt then + liftM (fmap FF.unWithMegaparsecParser) $ 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 index c7ed9679..ee715cb9 100644 --- a/app/toysolver.hs +++ b/app/toysolver.hs @@ -78,6 +78,7 @@ data Options = Options , optOmegaReal :: String , optFileEncoding :: Maybe String , optMaxSATCompactVLine :: Bool + , optPBParserMegaparsec :: Bool } deriving (Eq, Show) optionsParser :: Parser Options @@ -94,6 +95,7 @@ optionsParser = Options <*> omegaRealOption <*> fileEncodingOption <*> maxsatCompactVLineOption + <*> pbParserMegaparsecOption 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" + pbParserMegaparsecOption :: Parser Bool + pbParserMegaparsecOption = switch + $ long "pb-parser-megaparsec" + <> help "use megaparsec-based parser instead of attoparsec-based one for better error message" + 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 optPBParserMegaparsec o then + liftM FF.unWithMegaparsecParser $ 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 optPBParserMegaparsec o then + liftM FF.unWithMegaparsecParser $ 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 index cc6b6891..bf6a93e8 100644 --- 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,19 +8,22 @@ -- -- Maintainer : masahiro.sakai@gmail.com -- Stability : provisional --- Portability : portable +-- Portability : non-portable -- ----------------------------------------------------------------------------- module ToySolver.FileFormat ( module ToySolver.FileFormat.Base + , WithMegaparsecParser (..) ) 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 @@ -28,3 +32,25 @@ instance FileFormat PBFile.Formula where instance FileFormat PBFile.SoftFormula where parse = PBFileAttoparsec.parseWBOByteString render = PBFileBB.wboBuilder + + +-- | Wrapper type for parsing opb/wbo files using megaparsec-based parser instead of attoparsec-based one. +newtype WithMegaparsecParser a + = WithMegaparsecParser + { unWithMegaparsecParser :: a + } + +instance FileFormat (WithMegaparsecParser PBFile.Formula) where + parse s = + case PBFileMegaparsec.parseOPBByteString "-" s of + Left err -> Left (errorBundlePretty err) + Right x -> Right (WithMegaparsecParser x) + render (WithMegaparsecParser x) = PBFileBB.opbBuilder x + +instance FileFormat (WithMegaparsecParser PBFile.SoftFormula) where + parse s = + case PBFileMegaparsec.parseWBOByteString "-" s of + Left err -> Left (errorBundlePretty err) + Right x -> Right (WithMegaparsecParser x) + render (WithMegaparsecParser x) = PBFileBB.wboBuilder x + From 44f11b5096f9e11093e5cd29ed19bdefa8d35dd2 Mon Sep 17 00:00:00 2001 From: Masahiro Sakai Date: Mon, 11 Oct 2021 19:02:22 +0900 Subject: [PATCH 2/2] use megaparsec as a default PB parser and use attoparsec if --pb-fast-parser is provided --- app/toyconvert.hs | 22 ++++++++++---------- app/toysat/toysat.hs | 28 +++++++++++++------------- app/toysolver.hs | 20 +++++++++---------- src/ToySolver/FileFormat.hs | 40 ++++++++++++++++++------------------- 4 files changed, 54 insertions(+), 56 deletions(-) diff --git a/app/toyconvert.hs b/app/toyconvert.hs index 4684bc64..15938a76 100644 --- a/app/toyconvert.hs +++ b/app/toyconvert.hs @@ -64,7 +64,7 @@ data Options = Options , optFileEncoding :: Maybe String , optRemoveUserCuts :: Bool , optNewWCNF :: Bool - , optPBParserMegaparsec :: Bool + , optPBFastParser :: Bool } deriving (Eq, Show) optionsParser :: Parser Options @@ -85,7 +85,7 @@ optionsParser = Options <*> encodingOption <*> removeUserCutsOption <*> newWCNFOption - <*> pbParserMegaparsecOption + <*> pbFastParserOption where fileInput :: Parser FilePath fileInput = argument str (metavar "FILE") @@ -186,10 +186,10 @@ optionsParser = Options $ long "wcnf-new" <> help "use new format for writing WCNF files" - pbParserMegaparsecOption :: Parser Bool - pbParserMegaparsecOption = switch - $ long "pb-parser-megaparsec" - <> help "use megaparsec-based parser instead of attoparsec-based one for better error message" + 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) @@ -230,13 +230,13 @@ readProblem o fname = do ".wcnf" -> liftM (ProbWBO . fst . maxsat2wbo) $ FF.readFile fname ".opb" -> liftM ProbOPB $ do - if optPBParserMegaparsec o then - liftM FF.unWithMegaparsecParser $ FF.readFile fname + if optPBFastParser o then + liftM FF.unWithFastParser $ FF.readFile fname else FF.readFile fname - ".wbo" -> liftM ProbWBO $ - if optPBParserMegaparsec o then - liftM FF.unWithMegaparsecParser $ FF.readFile fname + ".wbo" -> liftM ProbWBO $ do + if optPBFastParser o then + liftM FF.unWithFastParser $ FF.readFile fname else FF.readFile fname ".gcnf" -> diff --git a/app/toysat/toysat.hs b/app/toysat/toysat.hs index 088b2ce4..cd343c83 100644 --- a/app/toysat/toysat.hs +++ b/app/toysat/toysat.hs @@ -104,7 +104,7 @@ data Options , optTempDir :: Maybe FilePath , optFileEncoding :: Maybe String , optMaxSATCompactVLine :: Bool - , optPBParserMegaparsec :: Bool + , optPBFastParser :: Bool } instance Default Options where @@ -128,7 +128,7 @@ instance Default Options where , optTempDir = Nothing , optFileEncoding = Nothing , optMaxSATCompactVLine = False - , optPBParserMegaparsec = False + , optPBFastParser = False } optionsParser :: Parser Options @@ -151,7 +151,7 @@ optionsParser = Options <*> tempDirOption <*> fileEncodingOption <*> maxsatCompactVLineOption - <*> pbParserMegaparsecOption + <*> pbFastParserOption where fileInput :: Parser String fileInput = strArgument $ metavar "(FILE|-)" @@ -254,9 +254,9 @@ optionsParser = Options $ long "maxsat-compact-v-line" <> help "print Max-SAT solution in the new compact v-line format" - pbParserMegaparsecOption = switch - $ long "pb-parser-megaparsec" - <> help "use megaparsec-based parser instead of attoparsec-based one for better error message" + pbFastParserOption = switch + $ long "pb-fast-parser" + <> help "use attoparsec-based parser instead of megaparsec-based one for speed" satConfigParser :: Parser SAT.Config @@ -791,13 +791,13 @@ mainPB :: Options -> SAT.Solver -> IO () mainPB opt solver = do ret <- case optInput opt of "-" -> - if optPBParserMegaparsec opt then - liftM (fmap FF.unWithMegaparsecParser . FF.parse) BS.getContents + if optPBFastParser opt then + liftM (fmap FF.unWithFastParser . FF.parse) BS.getContents else liftM FF.parse BS.getContents fname -> - if optPBParserMegaparsec opt then - liftM (fmap FF.unWithMegaparsecParser) $ FF.parseFile fname + if optPBFastParser opt then + liftM (fmap FF.unWithFastParser) $ FF.parseFile fname else FF.parseFile fname case ret of @@ -917,13 +917,13 @@ mainWBO :: Options -> SAT.Solver -> IO () mainWBO opt solver = do ret <- case optInput opt of "-" -> - if optPBParserMegaparsec opt then - liftM (fmap FF.unWithMegaparsecParser . FF.parse) BS.getContents + if optPBFastParser opt then + liftM (fmap FF.unWithFastParser . FF.parse) BS.getContents else liftM FF.parse BS.getContents fname -> - if optPBParserMegaparsec opt then - liftM (fmap FF.unWithMegaparsecParser) $ FF.parseFile fname + if optPBFastParser opt then + liftM (fmap FF.unWithFastParser) $ FF.parseFile fname else FF.parseFile fname case ret of diff --git a/app/toysolver.hs b/app/toysolver.hs index ee715cb9..28b37317 100644 --- a/app/toysolver.hs +++ b/app/toysolver.hs @@ -78,7 +78,7 @@ data Options = Options , optOmegaReal :: String , optFileEncoding :: Maybe String , optMaxSATCompactVLine :: Bool - , optPBParserMegaparsec :: Bool + , optPBFastParser :: Bool } deriving (Eq, Show) optionsParser :: Parser Options @@ -95,7 +95,7 @@ optionsParser = Options <*> omegaRealOption <*> fileEncodingOption <*> maxsatCompactVLineOption - <*> pbParserMegaparsecOption + <*> pbFastParserOption where fileInput :: Parser FilePath fileInput = argument str (metavar "FILE") @@ -172,10 +172,10 @@ optionsParser = Options $ long "maxsat-compact-v-line" <> help "print Max-SAT solution in the new compact v-line format" - pbParserMegaparsecOption :: Parser Bool - pbParserMegaparsecOption = switch - $ long "pb-parser-megaparsec" - <> help "use megaparsec-based parser instead of attoparsec-based one for better error message" + 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) @@ -479,8 +479,8 @@ main = do writeSOLFileSAT o m2 ModePB -> do pb <- - if optPBParserMegaparsec o then - liftM FF.unWithMegaparsecParser $ FF.readFile (optInput o) + if optPBFastParser o then + liftM FF.unWithFastParser $ FF.readFile (optInput o) else FF.readFile (optInput o) let (mip,info2) = pb2ip pb @@ -490,8 +490,8 @@ main = do writeSOLFileSAT o m2 ModeWBO -> do wbo <- - if optPBParserMegaparsec o then - liftM FF.unWithMegaparsecParser $ FF.readFile (optInput o) + if optPBFastParser o then + liftM FF.unWithFastParser $ FF.readFile (optInput o) else FF.readFile (optInput o) let (mip,info2) = wbo2ip False wbo diff --git a/src/ToySolver/FileFormat.hs b/src/ToySolver/FileFormat.hs index bf6a93e8..7b6288f2 100644 --- a/src/ToySolver/FileFormat.hs +++ b/src/ToySolver/FileFormat.hs @@ -13,7 +13,7 @@ ----------------------------------------------------------------------------- module ToySolver.FileFormat ( module ToySolver.FileFormat.Base - , WithMegaparsecParser (..) + , WithFastParser (..) ) where import qualified Data.PseudoBoolean as PBFile @@ -26,31 +26,29 @@ import ToySolver.QUBO () -- importing instances import Text.Megaparsec.Error (errorBundlePretty) instance FileFormat PBFile.Formula where - parse = PBFileAttoparsec.parseOPBByteString - render = PBFileBB.opbBuilder - -instance FileFormat PBFile.SoftFormula where - parse = PBFileAttoparsec.parseWBOByteString - render = PBFileBB.wboBuilder - - --- | Wrapper type for parsing opb/wbo files using megaparsec-based parser instead of attoparsec-based one. -newtype WithMegaparsecParser a - = WithMegaparsecParser - { unWithMegaparsecParser :: a - } - -instance FileFormat (WithMegaparsecParser PBFile.Formula) where parse s = case PBFileMegaparsec.parseOPBByteString "-" s of Left err -> Left (errorBundlePretty err) - Right x -> Right (WithMegaparsecParser x) - render (WithMegaparsecParser x) = PBFileBB.opbBuilder x + Right x -> Right x + render x = PBFileBB.opbBuilder x -instance FileFormat (WithMegaparsecParser PBFile.SoftFormula) where +instance FileFormat PBFile.SoftFormula where parse s = case PBFileMegaparsec.parseWBOByteString "-" s of Left err -> Left (errorBundlePretty err) - Right x -> Right (WithMegaparsecParser x) - render (WithMegaparsecParser x) = PBFileBB.wboBuilder x + 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