diff --git a/app/toyconvert.hs b/app/toyconvert.hs index 5d496b5c..7558f9cf 100644 --- 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 index d2a6e955..cd343c83 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 + , 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 index c7ed9679..28b37317 100644 --- 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 index cc6b6891..7b6288f2 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,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