{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
module Crux.Config.Common (
OutputOptions(..),
CruxOptions(..),
PathStrategy(..),
cruxOptions,
defaultOutputOptions,
postprocessOptions,
) where
import Control.Lens (set)
import Data.Functor.Alt
import Data.Generics.Product.Fields (field)
import Data.Time(DiffTime, NominalDiffTime)
import Data.Maybe(fromMaybe)
import Data.Char(toLower)
import Data.Word (Word64)
import Data.Text (pack)
import GHC.Generics (Generic)
import System.Directory ( createDirectoryIfMissing )
import Crux.Config
import Crux.Config.Load (ColorOptions(..))
import Crux.Log as Log
import Config.Schema
import What4.ProblemFeatures
data PathStrategy
= AlwaysMergePaths
| SplitAndExploreDepthFirst
pathStrategySpec :: ValueSpec PathStrategy
pathStrategySpec :: ValueSpec PathStrategy
pathStrategySpec =
(PathStrategy
AlwaysMergePaths PathStrategy -> ValueSpec () -> ValueSpec PathStrategy
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"always-merge") ValueSpec PathStrategy
-> ValueSpec PathStrategy -> ValueSpec PathStrategy
forall a. ValueSpec a -> ValueSpec a -> ValueSpec a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!>
(PathStrategy
SplitAndExploreDepthFirst PathStrategy -> ValueSpec () -> ValueSpec PathStrategy
forall a b. a -> ValueSpec b -> ValueSpec a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ValueSpec ()
atomSpec Text
"split-dfs")
postprocessOptions ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
CruxOptions -> IO CruxOptions
postprocessOptions :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
postprocessOptions =
CruxOptions -> IO CruxOptions
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathStrategyInteractions (CruxOptions -> IO CruxOptions)
-> (CruxOptions -> IO CruxOptions) -> CruxOptions -> IO CruxOptions
forall a b.
(CruxOptions -> a) -> (CruxOptions -> b) -> CruxOptions -> b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
CruxOptions -> IO CruxOptions
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathSatInteractions (CruxOptions -> IO CruxOptions)
-> (CruxOptions -> IO CruxOptions) -> CruxOptions -> IO CruxOptions
forall a b.
(CruxOptions -> a) -> (CruxOptions -> b) -> CruxOptions -> b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
CruxOptions -> IO CruxOptions
checkBldDir
checkPathStrategyInteractions ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
CruxOptions -> IO CruxOptions
checkPathStrategyInteractions :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathStrategyInteractions CruxOptions
crux =
case CruxOptions -> PathStrategy
pathStrategy CruxOptions
crux of
PathStrategy
AlwaysMergePaths -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux
PathStrategy
SplitAndExploreDepthFirst
| CruxOptions -> Bool
profileCrucibleFunctions CruxOptions
crux Bool -> Bool -> Bool
|| CruxOptions -> Bool
branchCoverage CruxOptions
crux ->
do CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.DisablingProfilingIncompatibleWithPathSplitting
return CruxOptions
crux { profileCrucibleFunctions = False, branchCoverage = False }
| Bool
otherwise -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux
checkPathSatInteractions ::
Logs msgs =>
SupportsCruxLogMessage msgs =>
CruxOptions -> IO CruxOptions
checkPathSatInteractions :: forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxOptions -> IO CruxOptions
checkPathSatInteractions CruxOptions
crux =
case CruxOptions -> Bool
checkPathSat CruxOptions
crux of
Bool
True -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux
Bool
False
| CruxOptions -> Bool
branchCoverage CruxOptions
crux ->
do CruxLogMessage -> IO ()
forall msgs.
(Logs msgs, SupportsCruxLogMessage msgs) =>
CruxLogMessage -> IO ()
sayCrux CruxLogMessage
Log.DisablingBranchCoverageRequiresPathSatisfiability
return CruxOptions
crux { branchCoverage = False }
| Bool
otherwise -> CruxOptions -> IO CruxOptions
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return CruxOptions
crux
checkBldDir :: CruxOptions -> IO CruxOptions
checkBldDir :: CruxOptions -> IO CruxOptions
checkBldDir CruxOptions
crux = do
Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ CruxOptions -> FilePath
bldDir CruxOptions
crux
return CruxOptions
crux
data OutputOptions = OutputOptions
{ OutputOptions -> ColorOptions
colorOptions :: ColorOptions
, OutputOptions -> Bool
printFailures :: Bool
, OutputOptions -> Bool
printSymbolicVars :: Bool
, OutputOptions -> Int
simVerbose :: Int
, OutputOptions -> Bool
quietMode :: Bool
}
deriving ((forall x. OutputOptions -> Rep OutputOptions x)
-> (forall x. Rep OutputOptions x -> OutputOptions)
-> Generic OutputOptions
forall x. Rep OutputOptions x -> OutputOptions
forall x. OutputOptions -> Rep OutputOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. OutputOptions -> Rep OutputOptions x
from :: forall x. OutputOptions -> Rep OutputOptions x
$cto :: forall x. Rep OutputOptions x -> OutputOptions
to :: forall x. Rep OutputOptions x -> OutputOptions
Generic)
defaultOutputOptions :: ColorOptions -> OutputOptions
defaultOutputOptions :: ColorOptions -> OutputOptions
defaultOutputOptions ColorOptions
copts = OutputOptions
{ colorOptions :: ColorOptions
colorOptions = ColorOptions
copts
, printFailures :: Bool
printFailures = Bool
False
, printSymbolicVars :: Bool
printSymbolicVars = Bool
False
, quietMode :: Bool
quietMode = Bool
False
, simVerbose :: Int
simVerbose = Int
0
}
data CruxOptions = CruxOptions
{ CruxOptions -> [FilePath]
inputFiles :: [FilePath]
, CruxOptions -> FilePath
outDir :: FilePath
, CruxOptions -> FilePath
bldDir :: FilePath
, CruxOptions -> Bool
checkPathSat :: Bool
, CruxOptions -> Bool
profileCrucibleFunctions :: Bool
, CruxOptions -> Bool
profileSolver :: Bool
, CruxOptions -> Bool
branchCoverage :: Bool
, CruxOptions -> PathStrategy
pathStrategy :: PathStrategy
, CruxOptions -> Maybe NominalDiffTime
globalTimeout :: Maybe NominalDiffTime
, CruxOptions -> Maybe DiffTime
goalTimeout :: Maybe DiffTime
, CruxOptions -> NominalDiffTime
profileOutputInterval :: NominalDiffTime
, CruxOptions -> Maybe Word64
loopBound :: Maybe Word64
, CruxOptions -> Maybe Word64
recursionBound :: Maybe Word64
, CruxOptions -> Bool
makeCexes :: Bool
, CruxOptions -> Bool
unsatCores :: Bool
, CruxOptions -> Maybe Word64
getNAbducts :: Maybe Word64
, CruxOptions -> FilePath
solver :: String
, CruxOptions -> Maybe FilePath
pathSatSolver :: Maybe String
, CruxOptions -> Bool
forceOfflineGoalSolving :: Bool
, CruxOptions -> Maybe FilePath
pathSatSolverOutput :: Maybe FilePath
, CruxOptions -> Maybe FilePath
onlineSolverOutput :: Maybe FilePath
, CruxOptions -> Maybe FilePath
offlineSolverOutput :: Maybe FilePath
, CruxOptions -> Bool
yicesMCSat :: Bool
, CruxOptions -> FilePath
floatMode :: String
, CruxOptions -> Bool
proofGoalsFailFast :: Bool
, CruxOptions -> Bool
skipReport :: Bool
, CruxOptions -> Bool
skipSuccessReports :: Bool
, CruxOptions -> Bool
skipIncompleteReports :: Bool
, CruxOptions -> Bool
hashConsing :: Bool
, CruxOptions -> ProblemFeatures
onlineProblemFeatures :: ProblemFeatures
, CruxOptions -> OutputOptions
outputOptions :: OutputOptions
}
deriving ((forall x. CruxOptions -> Rep CruxOptions x)
-> (forall x. Rep CruxOptions x -> CruxOptions)
-> Generic CruxOptions
forall x. Rep CruxOptions x -> CruxOptions
forall x. CruxOptions -> Rep CruxOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. CruxOptions -> Rep CruxOptions x
from :: forall x. CruxOptions -> Rep CruxOptions x
$cto :: forall x. Rep CruxOptions x -> CruxOptions
to :: forall x. Rep CruxOptions x -> CruxOptions
Generic)
cruxOptions :: Config CruxOptions
cruxOptions :: Config CruxOptions
cruxOptions = Config
{ cfgFile :: SectionsSpec CruxOptions
cfgFile =
do [FilePath]
inputFiles <-
Text
-> ValueSpec [FilePath]
-> [FilePath]
-> Text
-> SectionsSpec [FilePath]
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"files" (ValueSpec FilePath -> ValueSpec [FilePath]
forall a. ValueSpec a -> ValueSpec [a]
oneOrList ValueSpec FilePath
fileSpec) []
Text
"Input files to process."
FilePath
outDir <-
Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"output-directory" ValueSpec FilePath
dirSpec FilePath
""
Text
"Save results in this directory."
FilePath
bldDir <-
Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"build-dir" ValueSpec FilePath
dirSpec FilePath
"crux-build"
Text
"Directory in which to create files generated from the inputFiles."
Bool
checkPathSat <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"path-sat" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Enable path satisfiability checking (default: no)."
Bool
profileCrucibleFunctions <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"profile-crucible" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Profile crucible function entry/exit. (default: no)"
Bool
profileSolver <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"profile-solver" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Profile solver events. (default: no)"
Bool
branchCoverage <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"branch-coverage" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Record branch coverage information. (default: no)"
NominalDiffTime
profileOutputInterval <-
Text
-> ValueSpec NominalDiffTime
-> NominalDiffTime
-> Text
-> SectionsSpec NominalDiffTime
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"profiling-period" ValueSpec NominalDiffTime
forall a. Fractional a => ValueSpec a
fractionalSpec NominalDiffTime
5
Text
"Time between intermediate profile data reports (default: 5 seconds)"
Maybe NominalDiffTime
globalTimeout <-
Text
-> ValueSpec NominalDiffTime
-> Text
-> SectionsSpec (Maybe NominalDiffTime)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"timeout" ValueSpec NominalDiffTime
forall a. Fractional a => ValueSpec a
fractionalSpec
Text
"Stop executing the simulator after this many seconds."
Maybe DiffTime
goalTimeout <-
Text -> ValueSpec DiffTime -> Text -> SectionsSpec (Maybe DiffTime)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"goal-timeout" ValueSpec DiffTime
forall a. Fractional a => ValueSpec a
fractionalSpec
Text
"Stop trying to prove a goal after this many seconds."
Maybe Word64
loopBound <-
Text -> ValueSpec Word64 -> Text -> SectionsSpec (Maybe Word64)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"iteration-bound" ValueSpec Word64
forall a. Num a => ValueSpec a
numSpec
Text
"Bound all loops to at most this many iterations."
Maybe Word64
recursionBound <-
Text -> ValueSpec Word64 -> Text -> SectionsSpec (Maybe Word64)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"recursion-bound" ValueSpec Word64
forall a. Num a => ValueSpec a
numSpec
Text
"Bound the number of recursive calls to at most this many calls."
PathStrategy
pathStrategy <-
Text
-> ValueSpec PathStrategy
-> PathStrategy
-> Text
-> SectionsSpec PathStrategy
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"path-strategy" ValueSpec PathStrategy
pathStrategySpec PathStrategy
AlwaysMergePaths
Text
"Simulator strategy for path exploration."
Bool
makeCexes <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"make-executables" ValueSpec Bool
yesOrNoSpec Bool
True
Text
"Should we generate counter-example executables. (default: yes)"
Bool
unsatCores <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"unsat-cores" ValueSpec Bool
yesOrNoSpec Bool
True
Text
"Should we attempt to compute unsatisfiable cores for successfult proofs (default: yes)"
Maybe Word64
getNAbducts <-
Text -> ValueSpec Word64 -> Text -> SectionsSpec (Maybe Word64)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"get-abducts" ValueSpec Word64
forall a. Num a => ValueSpec a
numSpec
Text
"How many abducts should we get from the solver for sat results? Only works with cvc5, 0 otherwise."
FilePath
solver <-
Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"solver" ValueSpec FilePath
stringSpec FilePath
"yices"
(FilePath -> Text
pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ FilePath
"Select the solver to use to discharge proof obligations. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"May be a single solver, a comma-separated list of solvers, or the string \"all\". " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"Specifying multiple solvers requires the --force-offline-goal-solving option. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"(default: \"yices\")")
Maybe FilePath
pathSatSolver <-
Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"path-sat-solver" ValueSpec FilePath
stringSpec
Text
"Select the solver to use for path satisfiability checking (if different from `solver` and required by the `path-sat` option). (default: use `solver`)"
Bool
forceOfflineGoalSolving <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"force-offline-goal-solving" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Force goals to be solved using an offline solver, even if the selected solver could have been used in online mode (default: no)"
Maybe FilePath
pathSatSolverOutput <-
Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"path-sat-solver-output" ValueSpec FilePath
stringSpec
Text
"The file to store the interaction with the path satisfiability solver (if enabled and different from the main solver) (default: none)"
Maybe FilePath
onlineSolverOutput <-
Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"online-solver-output" ValueSpec FilePath
stringSpec
Text
"The file to store the interaction with the online goal solver (if any) (default: none)"
Maybe FilePath
offlineSolverOutput <-
Text -> ValueSpec FilePath -> Text -> SectionsSpec (Maybe FilePath)
forall a. Text -> ValueSpec a -> Text -> SectionsSpec (Maybe a)
sectionMaybe Text
"offine-solver-output" ValueSpec FilePath
stringSpec
(FilePath -> Text
pack FilePath
offlineSolverOutputHelp)
Int
simVerbose <-
Text -> ValueSpec Int -> Int -> Text -> SectionsSpec Int
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"sim-verbose" ValueSpec Int
forall a. Num a => ValueSpec a
numSpec Int
1
Text
"Verbosity of simulators. (default: 1)"
Bool
yicesMCSat <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"mcsat" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Enable the MC-SAT solver in Yices (disables unsat cores) (default: no)"
FilePath
floatMode <-
Text
-> ValueSpec FilePath -> FilePath -> Text -> SectionsSpec FilePath
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"floating-point" ValueSpec FilePath
stringSpec FilePath
"default"
(FilePath -> Text
pack (FilePath -> Text) -> FilePath -> Text
forall a b. (a -> b) -> a -> b
$ FilePath
"Select floating point representation,"
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" i.e. one of [real|ieee|uninterpreted|default]. "
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
Bool
hashConsing <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"hash-consing" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Enable hash-consing in the symbolic expression backend"
Bool
printFailures <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"print-failures" ValueSpec Bool
yesOrNoSpec Bool
True
Text
"Print error messages regarding failed verification goals"
Bool
printSymbolicVars <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"print-symbolic-vars" ValueSpec Bool
yesOrNoSpec Bool
False
(Text
"Print values assigned to symbolic variables " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>
Text
"when printing failed verification goals")
Bool
skipReport <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"skip-report" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Skip producing the HTML report after verification"
Bool
skipSuccessReports <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"skip-success-reports" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Skip reporting on successful proof obligations"
Bool
skipIncompleteReports <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"skip-incomplete-reports" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Skip reporting on proof obligations that arise from timeouts and resource exhaustion"
Bool
noColors <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"no-colors" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Suppress color codes in both the output and the errors"
Bool
noColorsErr <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"no-colors-err" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Suppress color codes in the errors"
Bool
noColorsOut <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"no-colors-out" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"Suppress color codes in the output"
Bool
quietMode <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"quiet-mode" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"If true, produce minimal output"
Bool
proofGoalsFailFast <-
Text -> ValueSpec Bool -> Bool -> Text -> SectionsSpec Bool
forall a. Text -> ValueSpec a -> a -> Text -> SectionsSpec a
section Text
"proof-goals-fail-fast" ValueSpec Bool
yesOrNoSpec Bool
False
Text
"If true, stop attempting to prove goals as soon as one of them is disproved"
ProblemFeatures
onlineProblemFeatures <- ProblemFeatures -> SectionsSpec ProblemFeatures
forall a. a -> SectionsSpec a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProblemFeatures
noFeatures
pure CruxOptions
{ outputOptions :: OutputOptions
outputOptions = OutputOptions
{ colorOptions :: ColorOptions
colorOptions = ColorOptions
{ noColorsErr :: Bool
noColorsErr = Bool
noColorsErr Bool -> Bool -> Bool
|| Bool
noColors
, noColorsOut :: Bool
noColorsOut = Bool
noColorsOut Bool -> Bool -> Bool
|| Bool
noColors
},
Bool
Int
printFailures :: Bool
printSymbolicVars :: Bool
simVerbose :: Int
quietMode :: Bool
simVerbose :: Int
printFailures :: Bool
printSymbolicVars :: Bool
quietMode :: Bool
..
},
Bool
FilePath
[FilePath]
Maybe FilePath
Maybe Word64
Maybe DiffTime
Maybe NominalDiffTime
NominalDiffTime
ProblemFeatures
PathStrategy
pathStrategy :: PathStrategy
profileCrucibleFunctions :: Bool
branchCoverage :: Bool
checkPathSat :: Bool
bldDir :: FilePath
inputFiles :: [FilePath]
outDir :: FilePath
profileSolver :: Bool
globalTimeout :: Maybe NominalDiffTime
goalTimeout :: Maybe DiffTime
profileOutputInterval :: NominalDiffTime
loopBound :: Maybe Word64
recursionBound :: Maybe Word64
makeCexes :: Bool
unsatCores :: Bool
getNAbducts :: Maybe Word64
solver :: FilePath
pathSatSolver :: Maybe FilePath
forceOfflineGoalSolving :: Bool
pathSatSolverOutput :: Maybe FilePath
onlineSolverOutput :: Maybe FilePath
offlineSolverOutput :: Maybe FilePath
yicesMCSat :: Bool
floatMode :: FilePath
proofGoalsFailFast :: Bool
skipReport :: Bool
skipSuccessReports :: Bool
skipIncompleteReports :: Bool
hashConsing :: Bool
onlineProblemFeatures :: ProblemFeatures
inputFiles :: [FilePath]
outDir :: FilePath
bldDir :: FilePath
checkPathSat :: Bool
profileCrucibleFunctions :: Bool
profileSolver :: Bool
branchCoverage :: Bool
profileOutputInterval :: NominalDiffTime
globalTimeout :: Maybe NominalDiffTime
goalTimeout :: Maybe DiffTime
loopBound :: Maybe Word64
recursionBound :: Maybe Word64
pathStrategy :: PathStrategy
makeCexes :: Bool
unsatCores :: Bool
getNAbducts :: Maybe Word64
solver :: FilePath
pathSatSolver :: Maybe FilePath
forceOfflineGoalSolving :: Bool
pathSatSolverOutput :: Maybe FilePath
onlineSolverOutput :: Maybe FilePath
offlineSolverOutput :: Maybe FilePath
yicesMCSat :: Bool
floatMode :: FilePath
hashConsing :: Bool
skipReport :: Bool
skipSuccessReports :: Bool
skipIncompleteReports :: Bool
proofGoalsFailFast :: Bool
onlineProblemFeatures :: ProblemFeatures
..
}
, cfgEnv :: [EnvDescr CruxOptions]
cfgEnv =
[
FilePath
-> FilePath
-> (FilePath -> OptSetter CruxOptions)
-> EnvDescr CruxOptions
forall opts.
FilePath
-> FilePath -> (FilePath -> OptSetter opts) -> EnvDescr opts
EnvVar FilePath
"BLDDIR" FilePath
"Directory for writing build files generated from the input files."
((FilePath -> OptSetter CruxOptions) -> EnvDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> EnvDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { bldDir = v }
]
, cfgCmdLineFlag :: [OptDescr CruxOptions]
cfgCmdLineFlag =
[ FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"d" [FilePath
"sim-verbose"]
FilePath
"Set simulator verbosity level."
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"NUM" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Int -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"NUM" ((Int -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (Int -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Int
v -> ASetter CruxOptions CruxOptions Int Int
-> Int -> CruxOptions -> CruxOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"outputOptions" ((OutputOptions -> Identity OutputOptions)
-> CruxOptions -> Identity CruxOptions)
-> ((Int -> Identity Int)
-> OutputOptions -> Identity OutputOptions)
-> ASetter CruxOptions CruxOptions Int Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"simVerbose") Int
v
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"path-sat"]
FilePath
"Enable path satisfiability checking"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { checkPathSat = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"output-directory"]
FilePath
"Location for reports. If unset, no reports will be generated."
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"DIR" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { outDir = v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"profile-crucible"]
FilePath
"Enable profiling of crucible function entry/exit"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { profileCrucibleFunctions = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"profile-solver"]
FilePath
"Enable profiling of solver events"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { profileSolver = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"branch-coverage"]
FilePath
"Record branch coverage information"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { branchCoverage = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"t" [FilePath
"timeout"]
FilePath
"Stop executing the simulator after this many seconds (default: 60)"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SECS"
((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
"60"
((FilePath -> OptSetter CruxOptions)
-> Maybe FilePath -> OptSetter CruxOptions)
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (NominalDiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseNominalDiffTime FilePath
"seconds"
((NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \NominalDiffTime
v CruxOptions
opts -> CruxOptions
opts { globalTimeout = Just v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"goal-timeout"]
FilePath
"Stop trying to prove each goal after this many seconds (default: 10)."
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SECS"
((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
"10"
((FilePath -> OptSetter CruxOptions)
-> Maybe FilePath -> OptSetter CruxOptions)
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (DiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (DiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseDiffTime FilePath
"seconds"
((DiffTime -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (DiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \DiffTime
v CruxOptions
opts -> CruxOptions
opts { goalTimeout = Just v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"" [FilePath
"path-strategy"]
FilePath
"Strategy to use for exploring paths ('always-merge' or 'split-dfs')"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"strategy"
((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ (PathStrategy -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions
forall opts.
(PathStrategy -> opts -> opts) -> FilePath -> OptSetter opts
parsePathStrategy
((PathStrategy -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (PathStrategy -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \PathStrategy
strat CruxOptions
opts -> CruxOptions
opts{ pathStrategy = strat }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"p" [FilePath
"profiling-period"]
FilePath
"Time between intermediate profile data reports (default: 5 seconds)"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SECS"
((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
"5"
((FilePath -> OptSetter CruxOptions)
-> Maybe FilePath -> OptSetter CruxOptions)
-> (FilePath -> OptSetter CruxOptions)
-> Maybe FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall opts.
FilePath
-> (NominalDiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseNominalDiffTime FilePath
"seconds"
((NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (NominalDiffTime -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \NominalDiffTime
v CruxOptions
opts -> CruxOptions
opts { profileOutputInterval = v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"i" [FilePath
"iteration-bound"]
FilePath
"Bound all loops to at most this many iterations"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"ITER"
((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"iterations"
((Word64 -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Word64
v CruxOptions
opts -> CruxOptions
opts { loopBound = Just v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"r" [FilePath
"recursion-bound"]
FilePath
"Bound all recursive calls to at most this many calls"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"CALLS"
((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"calls"
((Word64 -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Word64
v CruxOptions
opts -> CruxOptions
opts { recursionBound = Just v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"x" [FilePath
"no-execs"]
FilePath
"Disable generating counter-example executables"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { makeCexes = False }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"no-unsat-cores"]
FilePath
"Disable computing unsat cores for successful proofs"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { unsatCores = False }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"n" [FilePath
"get-abducts"]
FilePath
"Get these many abducts. Only works with cvc5, 0 otherwise."
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"ABDUCTS"
((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
"abducts"
((Word64 -> CruxOptions -> CruxOptions)
-> FilePath -> OptSetter CruxOptions)
-> (Word64 -> CruxOptions -> CruxOptions)
-> FilePath
-> OptSetter CruxOptions
forall a b. (a -> b) -> a -> b
$ \Word64
v CruxOptions
opts -> CruxOptions
opts { getNAbducts = Just v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"s" [FilePath
"solver"]
(FilePath
"Select the solver to use to discharge proof obligations. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"May be a single solver, a comma-separated list of solvers, or the string \"all\". " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"Specifying multiple solvers requires the --force-offline-goal-solving option. " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
FilePath
"(default: \"yices\")")
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"SOLVER" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { solver = map toLower v }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"path-sat-solver"]
FilePath
"Select the solver to use for path satisfiability checking (if different from `solver` and required by the `path-sat` option). (default: use `solver`)"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a. FilePath -> (Maybe FilePath -> OptSetter a) -> ArgDescr a
OptArg FilePath
"SOLVER" ((Maybe FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (Maybe FilePath -> OptSetter CruxOptions)
-> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \Maybe FilePath
ms CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { pathSatSolver = ms }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"force-offline-goal-solving"]
FilePath
"Force goals to be solved using an offline solver, even if the selected solver could have been used in online mode (default: no)"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { forceOfflineGoalSolving = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"path-sat-solver-output"]
FilePath
"The file to store the interaction with the path satisfiability solver (if enabled and different from the main solver) (default: none)"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
f CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { pathSatSolverOutput = Just f }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"online-solver-output"]
FilePath
"The file to store the interaction with the online goal solver (if any) (default: none)"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
f CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { onlineSolverOutput = Just f }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"offline-solver-output"]
FilePath
offlineSolverOutputHelp
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FILE" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
f CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { offlineSolverOutput = Just f }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"mcsat"]
FilePath
"Enable the MC-SAT solver in Yices (disables unsat cores)"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { yicesMCSat = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-report"]
FilePath
"Skip producing the HTML report following verificaion"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { skipReport = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-success-reports"]
FilePath
"Skip reporting on successful proof obligations"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { skipSuccessReports = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-incomplete-reports"]
FilePath
"Skip reporting on proof obligations that arise from timeouts and resource exhaustion"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { skipIncompleteReports = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"hash-consing"]
FilePath
"Enable hash-consing in the symbolic expression backend"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts{ hashConsing = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"skip-print-failures"]
FilePath
"Skip printing messages related to failed verification goals"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions
forall a b. b -> Either a b
Right OptSetter CruxOptions
-> (CruxOptions -> CruxOptions) -> OptSetter CruxOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter CruxOptions CruxOptions Bool Bool
-> Bool -> CruxOptions -> CruxOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"outputOptions" ((OutputOptions -> Identity OutputOptions)
-> CruxOptions -> Identity CruxOptions)
-> ((Bool -> Identity Bool)
-> OutputOptions -> Identity OutputOptions)
-> ASetter CruxOptions CruxOptions Bool Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"printFailures") Bool
False
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option [] [FilePath
"fail-fast"]
FilePath
"Stop attempting to prove goals as soon as one of them is disproved"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { proofGoalsFailFast = True }
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"q" [FilePath
"quiet"]
FilePath
"Quiet mode; produce minimal output"
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions -> ArgDescr CruxOptions
forall a. OptSetter a -> ArgDescr a
NoArg (OptSetter CruxOptions -> ArgDescr CruxOptions)
-> OptSetter CruxOptions -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ OptSetter CruxOptions
forall a b. b -> Either a b
Right OptSetter CruxOptions
-> (CruxOptions -> CruxOptions) -> OptSetter CruxOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASetter CruxOptions CruxOptions Bool Bool
-> Bool -> CruxOptions -> CruxOptions
forall s t a b. ASetter s t a b -> b -> s -> t
set (forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"outputOptions" ((OutputOptions -> Identity OutputOptions)
-> CruxOptions -> Identity CruxOptions)
-> ((Bool -> Identity Bool)
-> OutputOptions -> Identity OutputOptions)
-> ASetter CruxOptions CruxOptions Bool Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (field :: Symbol) s t a b.
HasField field s t a b =>
Lens s t a b
field @"quietMode") Bool
True
, FilePath
-> [FilePath]
-> FilePath
-> ArgDescr CruxOptions
-> OptDescr CruxOptions
forall a.
FilePath -> [FilePath] -> FilePath -> ArgDescr a -> OptDescr a
Option FilePath
"f" [FilePath
"floating-point"]
(FilePath
"Select floating point representation,"
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" i.e. one of [real|ieee|uninterpreted|default]. "
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
(ArgDescr CruxOptions -> OptDescr CruxOptions)
-> ArgDescr CruxOptions -> OptDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ FilePath
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a. FilePath -> (FilePath -> OptSetter a) -> ArgDescr a
ReqArg FilePath
"FPREP" ((FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions)
-> (FilePath -> OptSetter CruxOptions) -> ArgDescr CruxOptions
forall a b. (a -> b) -> a -> b
$ \FilePath
v CruxOptions
opts -> OptSetter CruxOptions
forall a b. b -> Either a b
Right CruxOptions
opts { floatMode = map toLower v }
]
}
offlineSolverOutputHelp :: String
offlineSolverOutputHelp :: FilePath
offlineSolverOutputHelp = [FilePath] -> FilePath
unlines
[ FilePath
"A template to use for files to store interactions with offline goal solvers"
, FilePath
"(if any) (default: none). For example, if the template is `offline-output.smt2`,"
, FilePath
"then each file will be named `offline-output-<goal number>-<solver name>.smt2,"
, FilePath
"where <goal number> is the number of the goal that was proven (starting at 0)"
, FilePath
"and <solver name> is the name of the solver used to dispatch that goal."
]
dflt :: String -> (String -> OptSetter opts) -> (Maybe String -> OptSetter opts)
dflt :: forall opts.
FilePath
-> (FilePath -> OptSetter opts) -> Maybe FilePath -> OptSetter opts
dflt FilePath
x FilePath -> OptSetter opts
p Maybe FilePath
mb = FilePath -> OptSetter opts
p (FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
x Maybe FilePath
mb)
parseDiffTime ::
String -> (DiffTime -> opts -> opts) -> String -> OptSetter opts
parseDiffTime :: forall opts.
FilePath
-> (DiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseDiffTime FilePath
thing DiffTime -> opts -> opts
mk =
FilePath -> (Double -> opts -> opts) -> FilePath -> OptSetter opts
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
thing (\Double
a opts
opts -> DiffTime -> opts -> opts
mk (Double -> DiffTime
cvt Double
a) opts
opts)
where cvt :: Double -> DiffTime
cvt :: Double -> DiffTime
cvt = Rational -> DiffTime
forall a. Fractional a => Rational -> a
fromRational (Rational -> DiffTime)
-> (Double -> Rational) -> Double -> DiffTime
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Rational
forall a. Real a => a -> Rational
toRational
parseNominalDiffTime ::
String -> (NominalDiffTime -> opts -> opts) -> String -> OptSetter opts
parseNominalDiffTime :: forall opts.
FilePath
-> (NominalDiffTime -> opts -> opts) -> FilePath -> OptSetter opts
parseNominalDiffTime FilePath
thing NominalDiffTime -> opts -> opts
mk =
FilePath -> (Double -> opts -> opts) -> FilePath -> OptSetter opts
forall a opts.
(Read a, Num a, Ord a) =>
FilePath -> (a -> opts -> opts) -> FilePath -> OptSetter opts
parsePosNum FilePath
thing (\Double
a opts
opts -> NominalDiffTime -> opts -> opts
mk (Double -> NominalDiffTime
cvt Double
a) opts
opts)
where cvt :: Double -> NominalDiffTime
cvt :: Double -> NominalDiffTime
cvt = Rational -> NominalDiffTime
forall a. Fractional a => Rational -> a
fromRational (Rational -> NominalDiffTime)
-> (Double -> Rational) -> Double -> NominalDiffTime
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Rational
forall a. Real a => a -> Rational
toRational
parsePathStrategy ::
(PathStrategy -> opts -> opts) -> String -> OptSetter opts
parsePathStrategy :: forall opts.
(PathStrategy -> opts -> opts) -> FilePath -> OptSetter opts
parsePathStrategy PathStrategy -> opts -> opts
mk FilePath
"always-merge" opts
opts = opts -> Either FilePath opts
forall a b. b -> Either a b
Right (opts -> Either FilePath opts) -> opts -> Either FilePath opts
forall a b. (a -> b) -> a -> b
$ PathStrategy -> opts -> opts
mk PathStrategy
AlwaysMergePaths opts
opts
parsePathStrategy PathStrategy -> opts -> opts
mk FilePath
"split-dfs" opts
opts = opts -> Either FilePath opts
forall a b. b -> Either a b
Right (opts -> Either FilePath opts) -> opts -> Either FilePath opts
forall a b. (a -> b) -> a -> b
$ PathStrategy -> opts -> opts
mk PathStrategy
SplitAndExploreDepthFirst opts
opts
parsePathStrategy PathStrategy -> opts -> opts
_mk FilePath
nm opts
_opts = FilePath -> Either FilePath opts
forall a b. a -> Either a b
Left (FilePath
"Unknown path strategy: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
nm)