toysolver-0.10.0: app/toysolver_check.hs

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Main where

import Control.Monad
import qualified Data.ByteString.Lazy.Char8 as BL
import Data.Default.Class
import Data.Scientific
import qualified Data.Version as V
import qualified Numeric.Optimization.MIP as MIP
import qualified Numeric.Optimization.MIP.Solution.Gurobi as GurobiSol
import Options.Applicative hiding (Const)
import System.Exit
import System.IO

import qualified ToySolver.FileFormat as FF
import ToySolver.Internal.SolutionChecker
import ToySolver.SAT.LogParser (parseSATLog, parseMaxSATLog, parsePBLog)
import ToySolver.Internal.Util (setEncodingChar8)
import ToySolver.Version


data Mode = ModeSAT | ModePB | ModeWBO | ModeMaxSAT | ModeMIP
  deriving (Eq, Ord, Show)

data Options = Options
  { optInputFile :: FilePath
  , optSolutionFile :: FilePath
  , optMode :: Maybe Mode
  , optFileEncoding :: Maybe String
  , optPBFastParser :: Bool
  , optMIPTol :: MIP.Tol Scientific
  }

optionsParser :: Parser Options
optionsParser = Options
  <$> fileInput
  <*> solutionFileInput
  <*> modeOption
  <*> fileEncodingOption
  <*> pbFastParserOption
  <*> mipTolOptions
  where
    fileInput :: Parser FilePath
    fileInput = argument str (metavar "FILE")

    solutionFileInput :: Parser FilePath
    solutionFileInput = argument str (metavar "SOLUTION_FILE")

    modeOption :: Parser (Maybe Mode)
    modeOption = optional $
          flag' ModeSAT    (long "sat"    <> help "load boolean satisfiability problem in .cnf file")
      <|> flag' ModePB     (long "pb"     <> help "load pseudo boolean problem in .opb file")
      <|> flag' ModeWBO    (long "wbo"    <> help "load weighted boolean optimization problem in .wbo file")
      <|> flag' ModeMaxSAT (long "maxsat" <> help "load MaxSAT problem in .cnf or .wcnf file")
      <|> flag' ModeMIP    (long "mip"    <> help "load LP/MIP problem in .lp or .mps file")
      <|> flag' ModeMIP    (long "lp"     <> help "alias for --mip (deprecated)")

    fileEncodingOption :: Parser (Maybe String)
    fileEncodingOption = optional $ strOption
      $  long "encoding"
      <> metavar "ENCODING"
      <> help "file encoding for LP/MPS files"

    pbFastParserOption :: Parser Bool
    pbFastParserOption = switch
      $  long "pb-fast-parser"
      <> help "use attoparsec-based parser instead of megaparsec-based one for speed"

    mipTolOptions :: Parser (MIP.Tol Scientific)
    mipTolOptions = MIP.Tol <$> intTol <*> feasTol <*> optTol
      where
        intTol = option auto
          $  long "tol-integrality"
          <> metavar "REAL"
          <> help "If a value of integer variable is within this amount from its nearest integer, it is considered feasible."
          <> value (MIP.integralityTol def)
          <> showDefault
        feasTol = option auto
          $  long "tol-feasibility"
          <> metavar "REAL"
          <> help "If the amount of violation of constraints is within this amount, it is considered feasible."
          <> value (MIP.feasibilityTol def)
          <> showDefault
        optTol = option auto
          $  long "tol-optimality"
          <> metavar "REAL"
          <> help "Feasibility tolerance of dual constraints."
          <> value (MIP.optimalityTol def)
          <> showDefault

parserInfo :: ParserInfo Options
parserInfo = info (helper <*> versionOption <*> optionsParser)
  $  fullDesc
  <> header "toysolver-check - a solution checker"
  where
    versionOption :: Parser (a -> a)
    versionOption = infoOption (V.showVersion version)
      $  hidden
      <> long "version"
      <> help "Show version"

main :: IO ()
main = do
#ifdef FORCE_CHAR8
  setEncodingChar8
#endif

  opt <- execParser parserInfo
  let mode =
        case optMode opt of
          Just m  -> m
          Nothing ->
            case FF.getBaseExtension (optInputFile opt) of
              ".cnf"  -> ModeSAT
              ".opb"  -> ModePB
              ".wbo"  -> ModeWBO
              ".wcnf" -> ModeMaxSAT
              ".lp"   -> ModeMIP
              ".mps"  -> ModeMIP
              _ -> ModeSAT

  (ok, ls) <- case mode of
    ModeSAT -> do
      cnf  <- FF.readFile (optInputFile opt)
      (status, m) <- liftM parseSATLog (BL.readFile (optSolutionFile opt))
      pure $ checkSATResult cnf (status, m)

    ModePB -> do
      opb <-
        if optPBFastParser opt then
          liftM FF.unWithFastParser $ FF.readFile (optInputFile opt)
        else
          FF.readFile (optInputFile opt)
      (status, o, m) <- liftM parsePBLog (BL.readFile (optSolutionFile opt))
      pure $ checkPBResult opb (status, o, m)

    ModeWBO -> do
      wbo <-
        if optPBFastParser opt then
          liftM FF.unWithFastParser $ FF.readFile (optInputFile opt)
        else
          FF.readFile (optInputFile opt)
      (status, o, m) <- liftM parsePBLog (BL.readFile (optSolutionFile opt))
      pure $ checkWBOResult wbo (status, o, m)

    ModeMaxSAT -> do
      wcnf  <- FF.readFile (optInputFile opt)
      (status, o, m) <- liftM parseMaxSATLog (BL.readFile (optSolutionFile opt))
      pure $ checkMaxSATResult wcnf (status, o, m)

    ModeMIP -> do
      enc <- mapM mkTextEncoding $ optFileEncoding opt
      mip <- MIP.readFile def{ MIP.optFileEncoding = enc } (optInputFile opt)
      sol <- GurobiSol.readFile (optSolutionFile opt)
      let tol = optMIPTol opt
      pure $ checkMIPResult tol mip sol

  mapM_ putStrLn ls

  unless ok $ exitFailure