{-# LANGUAGE Safe #-}
module SAT.Mios.OptionParser
(
MiosConfiguration (..)
, defaultConfiguration
, MiosProgramOption (..)
, miosDefaultOption
, miosOptions
, miosUsage
, miosParseOptions
, miosParseOptionsFromArgs
, toMiosConf
)
where
import System.Console.GetOpt (ArgDescr(..), ArgOrder(..), getOpt, OptDescr(..), usageInfo)
import System.Environment (getArgs)
import SAT.Mios.Types (MiosConfiguration (..), defaultConfiguration)
data MiosProgramOption = MiosProgramOption
{
_targetFile :: Either String String
, _targets :: [String]
, _outputFile :: Maybe String
, _confVariableDecayRate :: Double
, _confClauseDecayRate :: Double
, _confRestartE :: Double
, _confRestartS :: Double
, _confCheckAnswer :: Bool
, _confVerbose :: Bool
, _confBenchmark :: Integer
, _confBenchSeq :: Int
, _confNoAnswer :: Bool
, _confDumpStat :: Int
, _validateAssignment :: Bool
, _displayHelp :: Bool
, _displayVersion :: Bool
}
miosDefaultOption :: MiosProgramOption
miosDefaultOption = MiosProgramOption
{
_targetFile = Left ""
, _targets = []
, _outputFile = Nothing
, _confVariableDecayRate = variableDecayRate defaultConfiguration
, _confClauseDecayRate = clauseDecayRate defaultConfiguration
, _confRestartE = restartExpansion defaultConfiguration
, _confRestartS = restartStep defaultConfiguration
, _confCheckAnswer = False
, _confVerbose = False
, _confBenchmark = -1
, _confBenchSeq = 0
, _confNoAnswer = False
, _confDumpStat = dumpSolverStatMode defaultConfiguration
, _validateAssignment = False
, _displayHelp = False
, _displayVersion = False
}
miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)]
miosOptions =
[
Option ['d'] ["variable-decay-rate"]
(ReqArg (\v c -> c { _confVariableDecayRate = read v }) (show (_confVariableDecayRate miosDefaultOption)))
"[solver] variable activity decay rate (0.0 - 1.0)"
, Option ['c'] ["clause-decay-rate"]
(ReqArg (\v c -> c { _confClauseDecayRate = read v }) (show (_confClauseDecayRate miosDefaultOption)))
"[solver] clause activity decay rate (0.0 - 1.0)"
, Option [] ["Re"]
(ReqArg (\v c -> c { _confRestartE = read v }) (show (_confRestartE miosDefaultOption)))
"[solver] expansion rate for blocking/forcing restart (>= 1.0)"
, Option [] ["Rs"]
(ReqArg (\v c -> c { _confRestartS = read v }) (show (_confRestartS miosDefaultOption)))
"[solver] a fixed number of conflicts between restarts"
, Option [':'] ["validate-assignment"]
(NoArg (\c -> c { _validateAssignment = True }))
"[solver] read an assignment from STDIN and validate it"
, Option [] ["validate"]
(NoArg (\c -> c { _confCheckAnswer = True }))
"[solver] self-check (satisfiable) assignment"
, Option ['o'] ["output"]
(ReqArg (\v c -> c { _outputFile = Just v }) "file")
"[option] filename to store result, '--' for stdout"
, Option ['v'] ["verbose"]
(NoArg (\c -> c { _confVerbose = True }))
"[option] display misc information"
, Option ['X'] ["hide-solution"]
(NoArg (\c -> c { _confNoAnswer = True }))
"[option] hide solution"
, Option [] ["benchmark"]
(ReqArg (\v c -> c { _confBenchmark = read v }) "-1/0/N")
"[devel] No/Exhaustive/N-second timeout benchmark"
, Option [] ["sequence"]
(ReqArg (\v c -> c { _confBenchSeq = read v }) "NUM")
"[devel] set 2nd field of a CSV generated by benchmark"
, Option [] ["dump"]
(ReqArg (\v c -> c { _confDumpStat = read v }) (show (dumpSolverStatMode defaultConfiguration)))
"[devel] dump level; 1:solved, 2:reduction, 3:restart"
, Option ['h'] ["help"]
(NoArg (\c -> c { _displayHelp = True }))
"[misc] display this message"
, Option [] ["version"]
(NoArg (\c -> c { _displayVersion = True }))
"[misc] display program ID"
]
miosUsage :: String -> String
miosUsage mes = usageInfo mes miosOptions
miosParseOptions :: String -> [String] -> IO MiosProgramOption
miosParseOptions mes argv =
case getOpt Permute miosOptions argv of
(o, [], []) -> return $ foldl (flip id) miosDefaultOption o
(o, l, []) -> do
let conf = foldl (flip id) miosDefaultOption o
return $ conf { _targetFile = Left (head l), _targets = l }
(_, _, errs) -> ioError (userError (concat errs ++ miosUsage mes))
miosParseOptionsFromArgs :: String -> IO MiosProgramOption
miosParseOptionsFromArgs mes = miosParseOptions mes =<< getArgs
toMiosConf :: MiosProgramOption -> MiosConfiguration
toMiosConf opts = MiosConfiguration
{
variableDecayRate = _confVariableDecayRate opts
, clauseDecayRate = _confClauseDecayRate opts
, dumpSolverStatMode = _confDumpStat opts
, emaCoeffs = emaCoeffs defaultConfiguration
, restartExpansion = _confRestartE opts
, restartStep = _confRestartS opts
}