liquid-fixpoint 0.9.6.3.6 → 0.9.6.3.7

raw patch · 14 files changed

+393/−126 lines, 14 filesdep −cmdargsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: cmdargs

API changes (from Hackage documentation)

Files

• CHANGES.md +7/−0
• liquid-fixpoint.cabal +2/−2
• src/Language/Fixpoint/Horn/Solve.hs +1/−1
• src/Language/Fixpoint/Horn/Transformations.hs +1/−1
• src/Language/Fixpoint/Misc.hs +1/−1
• src/Language/Fixpoint/Smt/Interface.hs +1/−1
• src/Language/Fixpoint/Solver.hs +1/−1
• src/Language/Fixpoint/Solver/EnvironmentReduction.hs +3/−1
• src/Language/Fixpoint/Solver/Solve.hs +1/−1
• src/Language/Fixpoint/Types/Config.hs +306/−115
• src/Language/Fixpoint/Verbosity.hs +45/−0
• tests/neg/numeric-version.fq +1/−0
• tests/test.hs +22/−1
• unix/Language/Fixpoint/Utils/Progress.hs +1/−1

@@ -2,6 +2,13 @@  ## NEXT +## 0.9.6.3.7 (2026-06-04)++- Migrate from cmdargs to base:System.Console.GetOpt+  [#842](https://github.com/ucsd-progsys/liquid-fixpoint/pull/842)+  [#843](https://github.com/ucsd-progsys/liquid-fixpoint/pull/843)+  [#844](https://github.com/ucsd-progsys/liquid-fixpoint/pull/844)+ ## 0.9.6.3.6 (2026-05-06)  - Drop dependency on lens-family [#841](http://github.com/ucsd-progsys/liquid-fixpoint/pull/841)

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquid-fixpoint-version:            0.9.6.3.6+version:            0.9.6.3.7 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description:   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint@@ -121,6 +121,7 @@                     Language.Fixpoint.Utils.Progress                     Language.Fixpoint.Utils.Statistics                     Language.Fixpoint.Utils.Trie+                    Language.Fixpoint.Verbosity                     Text.PrettyPrint.HughesPJ.Compat   other-modules:    Paths_liquid_fixpoint   autogen-modules:  Paths_liquid_fixpoint@@ -136,7 +137,6 @@                   , boxes                   , bytestring >= 0.10.2.1                   , cereal-                  , cmdargs                   , containers                   , deepseq                   , directory

@@ -22,7 +22,7 @@ import Text.PrettyPrint.HughesPJ.Compat ( render ) import Language.Fixpoint.Horn.Info ( hornFInfo ) -import System.Console.CmdArgs.Verbosity ( whenLoud )+import Language.Fixpoint.Verbosity ( whenLoud ) import qualified Data.Aeson as Aeson -- import Debug.Trace (traceM) 

@@ -34,7 +34,7 @@ import           Control.Monad.State import           Data.Maybe                   (catMaybes, mapMaybe, fromMaybe) import           Language.Fixpoint.Types.Visitor as V-import           System.Console.CmdArgs.Verbosity+import           Language.Fixpoint.Verbosity import           Data.Bifunctor (first, second) import System.IO (hFlush, stdout) -- import qualified Debug.Trace as DBG

@@ -31,7 +31,7 @@ import           Data.Unique import           Debug.Trace                      (trace) import           System.Console.ANSI-import           System.Console.CmdArgs.Verbosity (whenLoud)+import           Language.Fixpoint.Verbosity (whenLoud) import           System.Process                   (system) import           System.Directory                 (createDirectoryIfMissing) import           System.FilePath                  (takeDirectory)

@@ -92,7 +92,7 @@ -- import           Data.Text.Format import qualified Data.Text.Lazy.IO        as LTIO import           System.Directory-import           System.Console.CmdArgs.Verbosity+import           Language.Fixpoint.Verbosity import           System.FilePath import           System.IO import qualified Data.Attoparsec.Text     as A

@@ -32,7 +32,7 @@ import qualified Data.Text.Lazy.IO                as LT import qualified Data.Text.Lazy.Encoding          as LT import           System.Exit                        (ExitCode (..))-import           System.Console.CmdArgs.Verbosity   (whenNormal, whenLoud)+import           Language.Fixpoint.Verbosity   (whenNormal, whenLoud) import           Control.Monad                      (when) import           Control.Exception                  (SomeException, catch) import           Control.Exception.Compat

@@ -585,6 +585,8 @@ view :: Lens' s a -> s -> a view l s = getConst (l Const s) +infixr 4 %~+ (%~) :: Lens' s a -> (a -> a) -> s -> s (%~) l f s = runIdentity (l (Identity . f) s) @@ -600,7 +602,7 @@ substBindingsSimplifyingWith simplifier vLens p env =     -- Circular program here. This should terminate as long as the     -- bindings introduced by ANF don't form cycles.-    let env' = HashMap.map (vLens %~ (simplifier . inlineInSortedReft (srLookup filteredEnv))) env+    let env' = HashMap.map (vLens %~ simplifier . inlineInSortedReft (srLookup filteredEnv)) env         filteredEnv = HashMap.filterWithKey (\sym _v -> p sym) env'      in env'   where

@@ -32,7 +32,7 @@ import           Language.Fixpoint.Graph import           Text.PrettyPrint.HughesPJ import           Text.Printf-import           System.Console.CmdArgs.Verbosity -- (whenNormal, whenLoud)+import           Language.Fixpoint.Verbosity import           Control.DeepSeq import qualified Data.HashMap.Strict as M import qualified Data.HashSet        as S

@@ -1,4 +1,3 @@-{-# LANGUAGE DeriveDataTypeable        #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances      #-}@@ -41,8 +40,10 @@ import Data.Serialize                (Serialize (..)) import Control.DeepSeq import GHC.Generics-import System.Console.CmdArgs-import System.Console.CmdArgs.Explicit+import System.Console.GetOpt+import Language.Fixpoint.Verbosity   (Verbosity (..), setVerbosity, whenNormal)+import System.Environment            (getArgs)+import System.Exit                   (exitFailure, exitSuccess)  import qualified Language.Fixpoint.Conditional.Z3 as Conditional.Z3 import Language.Fixpoint.Utils.Files@@ -51,16 +52,6 @@ import Paths_liquid_fixpoint (version)  ---------------------------------------------------------------------------------withPragmas :: Config -> [String] -> IO Config----------------------------------------------------------------------------------withPragmas c s =-    processValueIO-      config { modeValue = (modeValue config) { cmdArgsValue = c } }-      s-    >>=-      cmdArgsApply---------------------------------------------------------------------------------- -- | Configuration Options ----------------------------------------------------- -------------------------------------------------------------------------------- @@ -104,7 +95,7 @@   , etabeta          :: Bool           -- ^ Eta expand and beta reduce terms to aid PLE   , localRewrites    :: Bool           -- ^ Eta expand and beta reduce terms to aid PLE   , saveBfqOnError   :: Bool           -- ^ save FInfo as .bfq only on verification failure-  , interpreter      :: Bool           -- ^ Do not use the interpreter to assist PLE+  , interpreter      :: Bool           -- ^ Use the interpreter to assist PLE   , noEnvReduction   :: Bool     -- ^ Don't use environment reduction   , inlineANFBinds   :: Bool          -- ^ Inline ANF bindings.                                        -- Sometimes improves performance and sometimes worsens it.@@ -119,18 +110,12 @@   , explicitKvars  :: Bool             -- ^ use explicitly declared kvars (horn style) which disables several "defensive simplifications"   , sortedSolution :: Bool             -- ^ leave sorts in the solution   , saveDir        :: Maybe FilePath    -- ^ output directory for --save generated files (default: .liquid/ next to source)-  } deriving (Eq,Data,Typeable,Show,Generic)--instance Default Config where-  def = defConfig+  } deriving (Eq,Show,Generic)  ---------------------------------------------------------------------------------------  data RESTOrdering = RESTKBO | RESTLPO | RESTRPO | RESTFuel Int-                 deriving (Eq, Data, Typeable, Generic)--instance Default RESTOrdering where-  def = RESTRPO+                 deriving (Eq, Generic)  instance Show RESTOrdering where   show RESTKBO      = "kbo"@@ -150,7 +135,7 @@ ---------------------------------------------------------------------------------------  data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat-                 deriving (Eq, Data, Typeable, Generic)+                 deriving (Eq, Generic)  data ElabFlags = ElabFlags { elabSetBag :: Bool, elabExplicitKvars :: Bool } @@ -164,9 +149,6 @@ solverFlags :: Config -> ElabFlags solverFlags cfg = mkElabFlags (solver cfg) (explicitKvars cfg) -instance Default SMTSolver where-  def = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3- instance Show SMTSolver where   show Z3      = "z3"   show Z3mem   = "z3 API"@@ -183,15 +165,12 @@ --   Both = scrape all concrete predicates (i.e. "rhs" + "lhs")  data Scrape = No | Head | Both-  deriving (Eq, Data, Typeable, Generic)+  deriving (Eq, Generic)  instance Serialize Scrape instance S.Store Scrape instance NFData Scrape -instance Default Scrape where-  def = No- instance Show Scrape where   show No   = "no"   show Head = "head"@@ -211,16 +190,13 @@   | All   | Horn   | Existentials-  deriving (Eq, Data, Typeable, Generic)+  deriving (Eq, Generic)  instance Serialize Eliminate instance S.Store Eliminate instance NFData SMTSolver instance NFData Eliminate -instance Default Eliminate where-  def = None- instance Show Eliminate where   show None = "none"   show Some = "some"@@ -235,95 +211,310 @@ ---------------------------------------------------------------------------------------  defConfig :: Config-defConfig = Config {-    srcFile                  = "out"   &= args    &= typFile-  , defunction               = False   &= help "Allow higher order binders into fixpoint environment"-  , solver                   = def     &= help "Name of SMT Solver"-  , linear                   = False   &= help "Use uninterpreted integer multiplication and division"-  , noStringTheory           = False   &= help "Disable use of string theory by SMT"-  , allowHO                  = False   &= help "Allow higher order binders into fixpoint environment"-  , allowHOqs                = False   &= help "Allow higher order qualifiers"-  , eliminate                = None    &= help "Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]"-  , scrape                   = def     &= help "Scrape qualifiers from constraint (Horn format only) [ no = do not, head = scrape from heads, both = scrape from everywhere ]"-  , elimBound                = Nothing &= name "elimBound"   &= help "(alpha) Maximum eliminate-chain depth"-  , smtTimeout               = Nothing &= name "smtTimeout"  &= help "SMT timeout in msec"-  , elimStats                = False   &= help "(alpha) Print eliminate stats"-  , solverStats              = False   &= help "Print solver stats"-  , save                     = False   &= help "Save Query as .fq and .bfq files"-  , saveBfqOnError           = False   &= help "Save Query as .bfq file only when verification fails"-                                       &= name "save-bfq-on-error"-                                       &= explicit-  , saveDir                  = Nothing-      &= name "save-dir"-      &= help "Output directory for --save generated files (default: .liquid/ next to source)"-      &= opt (Nothing :: Maybe FilePath)-      &= explicit-      &= typDir-  , metadata                 = False   &= help "Print meta-data associated with constraints"-  , stats                    = False   &= help "Compute constraint statistics"-  , etaElim                  = False   &= help "Eta elimination in function definition"-  , parts                    = False   &= help "Partition constraints into indepdendent .fq files"-  , cores                    = def     &= help "(numeric) Number of threads to use"-  , minPartSize              = defaultMinPartSize &= help "(numeric) Minimum partition size when solving in parallel"-  , maxPartSize              = defaultMaxPartSize &= help "(numeric) Maximum partiton size when solving in parallel."-  , minimize                 = False &= help "Delta debug to minimize fq file (unsat with min constraints)"-  , minimizeQs               = False &= help "Delta debug to minimize fq file (sat with min qualifiers)"-  , minimizeKs               = False &= help "Delta debug to minimize fq file (sat with max kvars replaced by True)"-  , minimalSol               = False &= help "Shrink fixpoint by removing implied qualifiers"-  , autoKuts                 = False &= help "Ignore given Kut vars, compute from scratch"-  , nonLinCuts               = False &= help "Treat non-linear kvars as cuts"-  , noslice                  = False &= help "Disable non-concrete KVar slicing"-  , rewriteAxioms            = False &= name "ple" &= help "Allow axiom instantiation via rewriting (PLE)"-  , pleUndecGuards   =-      False-        &= name "ple-with-undecided-guards"-        &= help "Unfold invocations with undecided guards in PLE"-        &= explicit-  , interpreter              =-      False-        &= name "interpreter"-        &= help "Use the interpreter to assist PLE"-  , etabeta                  = False &= help "Use eta expansion and beta reduction to aid PLE"-  , localRewrites            = False &= help "Perform local rewrites inside PLE"-  , noEnvReduction           = False &= help "Don't perform environment reduction"-  , inlineANFBinds           = False &= help (unwords-          [ "Inline ANF bindings."-          , "Sometimes improves performance and sometimes worsens it."-          , "Disabled by --noenvreduction"-          ])-  , checkCstr                = []    &= help "Only check these specific constraint-ids"-  , extensionality           = False &= help "Allow extensional interpretation of extensionality"-  , rwTermination       = False   &= help "Enable rewrite divergence checker"-  , stdin                    = False   &= help "Read input query from stdin"-  , json                     = False   &= help "Render result in JSON"-  , fuel                     = Nothing &= help "Maximum fuel (per-function unfoldings) for PLE"-  , restOrdering             = "rpo"   &= help "Ordering Constraint Algebra to use for REST"-  , explicitKvars            = False &= help "Use explicitly declared kvars (horn style) which disables several defensive simplifications"-  , sortedSolution           = False &= help "Leave elaborated sorts in the solution (only for machine consumption)"+defConfig = Config+  { srcFile            = "out"+  , defunction         = False+  , solver             = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3+  , linear             = False+  , noStringTheory     = False+  , allowHO            = False+  , allowHOqs          = False+  , eliminate          = None+  , scrape             = No+  , elimBound          = Nothing+  , smtTimeout         = Nothing+  , elimStats          = False+  , solverStats        = False+  , save               = False+  , saveBfqOnError     = False+  , saveDir            = Nothing+  , metadata           = False+  , stats              = False+  , etaElim            = False+  , parts              = False+  , cores              = Nothing+  , minPartSize        = defaultMinPartSize+  , maxPartSize        = defaultMaxPartSize+  , minimize           = False+  , minimizeQs         = False+  , minimizeKs         = False+  , minimalSol         = False+  , autoKuts           = False+  , nonLinCuts         = False+  , noslice            = False+  , rewriteAxioms      = False+  , pleUndecGuards     = False+  , interpreter        = False+  , etabeta            = False+  , localRewrites      = False+  , noEnvReduction     = False+  , inlineANFBinds     = False+  , checkCstr          = []+  , extensionality     = False+  , rwTermination      = False+  , stdin              = False+  , json               = False+  , fuel               = Nothing+  , restOrdering       = "rpo"+  , explicitKvars      = False+  , sortedSolution     = False   }-  &= verbosity-  &= program "fixpoint"-  &= help    "Predicate Abstraction Based Horn-Clause Solver"-  &= summary summaryInfo-  &= details [ "Predicate Abstraction Based Horn-Clause Solver"-             , ""-             , "To check a file foo.fq type:"-             , "  fixpoint foo.fq"-             ] +-- | An individual parsed flag (modifier to Config, verbosity change, or exit).+data FxFlag+  = FxMod (Config -> Config)+  | FxVerbosity Verbosity+  | FxHelp+  | FxVersion+  | FxNumericVersion++-- | All command-line options for fixpoint.+fxOptions :: [OptDescr FxFlag]+fxOptions =+  [ Option [] ["defunction", "defunct"] (NoArg (FxMod $ \c -> c { defunction = True }))+      "Allow higher order binders into fixpoint environment"+  , opt0 "linear"                  (\c -> c { linear            = True  })+      "Use uninterpreted integer multiplication and division"+  , opt0 "no-string-theory"        (\c -> c { noStringTheory    = True  })+      "Disable use of string theory by SMT"+  , opt0 "allowho"                 (\c -> c { allowHO           = True  })+      "Allow higher order binders into fixpoint environment"+  , opt0 "allowhoqs"               (\c -> c { allowHOqs         = True  })+      "Allow higher order qualifiers"+  , Option [] ["eliminate"]        (ReqArg setEliminate "ELIM")+      ( unlines+          [ "Eliminate KVars [" ++ L.intercalate " | "+            ["none", "some", "all", "horn", "existentials"] ++ "]"+          , "    none: quals for all-kvars"+          , "    some: ??"+          , "    all: eliminate all-kvars (TRUE for cuts)"+          , "    horn: ??"+          , "    existentials: ??"+          ]+      )+  , Option [] ["scrape"]           (ReqArg setScrape "SCRAPE")+      (unlines+        [ "Scrape qualifiers from constraint [" ++ L.intercalate " | "+          ["no", "head", "both"] ++ "]"+        , "    no: do not"+        , "    head: scrape from heads"+        , "    both: scrape from everywhere"+        ]+      )+  , Option [] ["solver"]           (ReqArg setSolver "SOLVER")+      ("SMT solver [" ++ L.intercalate " | " ["z3", "z3mem", "cvc4", "cvc5", "mathsat"] ++ "]")+  , Option [] ["elimBound"]        (ReqArg (\s -> FxMod $ \c -> c { elimBound   = parseInt "elimBound" s }) "N")+      "(alpha) Maximum eliminate-chain depth"+  , Option [] ["smtTimeout"]       (ReqArg (\s -> FxMod $ \c -> c { smtTimeout  = parseInt "smtTimeout" s }) "N")+      "SMT timeout in msec"+  , opt0 "elim-stats"              (\c -> c { elimStats     = True })+      "(alpha) Print eliminate stats"+  , opt0 "solver-stats"            (\c -> c { solverStats   = True })+      "Print solver stats"+  , opt0 "save"                    (\c -> c { save          = True })+      "Save Query as .fq and .bfq files"+  , Option [] ["save-bfq-on-error"] (NoArg (FxMod $ \c -> c { saveBfqOnError = True }))+      "Save Query as .bfq file only when verification fails"+  , Option [] ["save-dir"]         (ReqArg setSaveDir "DIR")+      "Output directory for --save generated files (default: .liquid/ next to source)"+  , opt0 "metadata"                (\c -> c { metadata      = True })+      "Print meta-data associated with constraints"+  , opt0 "stats"                   (\c -> c { stats         = True })+      "Compute constraint statistics"+  , Option [] ["eta-elim", "etaelim"] (NoArg (FxMod $ \c -> c { etaElim = True }))+      "Eta elimination in function definition"+  , opt0 "parts"                   (\c -> c { parts         = True })+      "Partition constraints into independent .fq files"+  , Option [] ["cores"]            (ReqArg (\s -> FxMod $ \c -> c { cores = parseInt "cores" s }) "N")+      "(numeric) Number of threads to use"+  , Option [] ["min-part-size"]    (ReqArg (\s -> FxMod $ \c -> c { minPartSize = read s }) "N")+      "(numeric) Minimum partition size when solving in parallel"+  , Option [] ["max-part-size"]    (ReqArg (\s -> FxMod $ \c -> c { maxPartSize = read s }) "N")+      "(numeric) Maximum partition size when solving in parallel"+  , opt0 "minimize"                (\c -> c { minimize       = True })+      "Delta debug to minimize fq file (unsat with min constraints)"+  , opt0 "minimize-qs"             (\c -> c { minimizeQs    = True })+      "Delta debug to minimize fq file (sat with min qualifiers)"+  , opt0 "minimize-ks"             (\c -> c { minimizeKs    = True })+      "Delta debug to minimize fq file (sat with max kvars replaced by True)"+  , opt0 "minimal-sol"             (\c -> c { minimalSol    = True })+      "Shrink fixpoint by removing implied qualifiers"+  , opt0 "auto-kuts"               (\c -> c { autoKuts      = True })+      "Ignore given Kut vars, compute from scratch"+  , opt0 "non-lin-cuts"            (\c -> c { nonLinCuts    = True })+      "Treat non-linear kvars as cuts"+  , opt0 "noslice"                 (\c -> c { noslice       = True })+      "Disable non-concrete KVar slicing"+  , Option [] ["ple", "rewrite", "rewrite-axioms"] (NoArg (FxMod $ \c -> c { rewriteAxioms = True }))+      "Allow axiom instantiation via rewriting (PLE)"+  , Option [] ["ple-with-undecided-guards"] (NoArg (FxMod $ \c -> c { pleUndecGuards = True }))+      "Unfold invocations with undecided guards in PLE"+  -- Accept optional =true/=false for backward compatibility with cmdargs Bool encoding+  , Option [] ["interpreter"]      (OptArg (parseBoolOpt interpreter (\b c -> c { interpreter = b })) "BOOL")+      "Use the interpreter to assist PLE"+  , opt0 "etabeta"                 (\c -> c { etabeta        = True })+      "Use eta expansion and beta reduction to aid PLE"+  , Option [] ["local-rewrites", "localrewrites"] (NoArg (FxMod $ \c -> c { localRewrites = True }))+      "Perform local rewrites inside PLE"+  , opt0 "no-env-reduction"        (\c -> c { noEnvReduction = True })+      "Don't perform environment reduction"+  , opt0 "inline-anf-binds"        (\c -> c { inlineANFBinds = True })+      "Inline ANF bindings (sometimes improves performance, sometimes worsens it)"+  , Option [] ["check-cstr"]       (ReqArg (\s -> FxMod $ \c -> c { checkCstr = checkCstr c ++ [read s] }) "ID")+      "Only check these specific constraint-ids (repeat for multiple)"+  , opt0 "extensionality"          (\c -> c { extensionality = True })+      "Allow extensional interpretation of function equality"+  , opt0 "rw-termination"          (\c -> c { rwTermination  = True })+      "Enable rewrite divergence checker"+  , opt0 "stdin"                   (\c -> c { stdin          = True })+      "Read input query from stdin"+  , opt0 "json"                    (\c -> c { json           = True })+      "Render result in JSON"+  , Option [] ["fuel"]             (ReqArg (\s -> FxMod $ \c -> c { fuel = parseInt "fuel" s }) "N")+      "Maximum fuel (per-function unfoldings) for PLE"+  , Option [] ["rest-ordering"]    (ReqArg (\s -> FxMod $ \c -> c { restOrdering = s }) "ORD")+      "Ordering constraint algebra to use for REST"+  , opt0 "explicit-kvars"          (\c -> c { explicitKvars  = True })+      "Use explicitly declared kvars (horn style) which disables several defensive simplifications"+  , opt0 "sorted-solution"         (\c -> c { sortedSolution = True })+      "Leave elaborated sorts in the solution (only for machine consumption)"+  , Option "v" ["verbose"]         (NoArg (FxVerbosity Loud))+      "Be more verbose"+  , Option "q" ["quiet"]           (NoArg (FxVerbosity Quiet))+      "Be quiet (suppress normal output)"+  , Option "h?" ["help"]           (NoArg FxHelp)+      "Show this help message"+  , Option "V" ["version"]         (NoArg FxVersion)+      "Show version"+  , Option [] ["numeric-version"]  (NoArg FxNumericVersion)+      "Print numeric version and exit"+  ]+  where+    opt0 name f desc =+      Option [] [name] (NoArg (FxMod f)) desc++    -- Parse an optional =true/=false/=True/=False argument (cmdargs Bool compat)+    parseBoolOpt :: (Config -> Bool) -> (Bool -> Config -> Config) -> Maybe String -> FxFlag+    parseBoolOpt _   setter Nothing          = FxMod (setter True)+    parseBoolOpt _   setter (Just "true")    = FxMod (setter True)+    parseBoolOpt _   setter (Just "True")    = FxMod (setter True)+    parseBoolOpt _   setter (Just "false")   = FxMod (setter False)+    parseBoolOpt _   setter (Just "False")   = FxMod (setter False)+    parseBoolOpt getDef _setter (Just s)         =+      error $ "Expected true/false, got: " ++ s ++ " (current default: " ++ show (getDef defConfig) ++ ")"++    setSolver s   = FxMod $ \c -> c { solver    = parseSolver s }+    setEliminate s = FxMod $ \c -> c { eliminate = parseEliminate s }+    setScrape s   = FxMod $ \c -> c { scrape    = parseScrape s }+    setSaveDir s = FxMod $ \c -> c { saveDir   = Just s }++    parseSolver "z3"        = Z3+    parseSolver "z3mem"     = Z3mem+    parseSolver "cvc4"      = Cvc4+    parseSolver "cvc5"      = Cvc5+    parseSolver "mathsat"   = Mathsat+    parseSolver s           = error $ "Unknown solver: " ++ s++    parseEliminate "none"         = None+    parseEliminate "some"         = Some+    parseEliminate "all"          = All+    parseEliminate "horn"         = Horn+    parseEliminate "existentials" = Existentials+    parseEliminate s              = error $ "Unknown eliminate mode: " ++ s++    parseScrape "no"   = No+    parseScrape "head" = Head+    parseScrape "both" = Both+    parseScrape s      = error $ "Unknown scrape mode: " ++ s++    parseInt _    s = Just (read s)++-- | Apply a list of parsed flags to a base Config; return updated config and+--   verbosity change (if any).+applyFxFlags :: Config -> [FxFlag] -> IO Config+applyFxFlags base flags = do+  mapM_ applyVerbosity flags+  return $! L.foldl' applyMod base flags+  where+    applyMod c (FxMod f) = f c+    applyMod c _         = c+    applyVerbosity (FxVerbosity vb) = setVerbosity vb+    applyVerbosity _                = return ()++--------------------------------------------------------------------------------+withPragmas :: Config -> [String] -> IO Config+--------------------------------------------------------------------------------+withPragmas base tokens =+  case getOpt Permute fxOptions tokens of+    (flags, _, [])   -> do+      -- We make fixpoint fail when given --version of --help pragmas to make+      -- it harder to miss that a file is not being checked.+      handleExits flags exitFailure (formatHelp fxOptions) summaryInfo+      applyFxFlags base flags+    (_, _, optErrs)  -> ioError $ userError $+        concat optErrs ++ "\nUse --help for usage information."++--------------------------------------------------------------------------------+ summaryInfo :: String-summaryInfo = "fixpoint " ++ showVersion version ++ " " ++ "("  ++ $(gitHash) ++ ")"-config :: Mode (CmdArgs Config)-config = cmdArgsMode defConfig+summaryInfo = "fixpoint " ++ showVersion version ++ " " ++ "(" ++ $(gitHash) ++ ")"  getOpts :: IO Config getOpts = do-  md <- cmdArgs defConfig-  whenNormal (putStrLn banner)-  return md+  args <- getArgs+  case getOpt Permute fxOptions args of+    (flags, files, []) -> do+      cfg <- applyFxFlags defConfig flags+      let srcF = case files of { (f:_) -> f; [] -> srcFile defConfig }+          cfg' = cfg { srcFile = srcF }+      whenBanner flags $ whenNormal (putStrLn banner)+      handleExits flags exitSuccess (formatHelp fxOptions) summaryInfo+      return cfg'+    (_, _, optErrs)    -> ioError $ userError $+        concat optErrs ++ "\nUse --help for usage information." +whenBanner :: [FxFlag] -> IO () -> IO ()+whenBanner (FxNumericVersion:_) _ = return ()+whenBanner (_:flags)   act = whenBanner flags act+whenBanner [] act          = act++handleExits :: [FxFlag] -> IO () -> String -> String -> IO ()+handleExits flags termination helpText ver = mapM_ go flags+  where+    go FxHelp           = putStr helpText >> termination+    go FxVersion        = putStrLn ver      >> termination+    go FxNumericVersion = putStrLn (showVersion version) >> termination+    go _                = return ()++formatHelp :: [OptDescr a] -> String+formatHelp opts =+    unlines $+      [ "Usage: fixpoint [OPTIONS] FILE.fq"+      , ""+      , "    Predicate Abstraction Based Horn-Clause Solver"+      , ""+      , "Options:"+      , ""+      ]+      ++ L.intersperse "" (map fmtOpt opts)+  where+    fmtOpt :: OptDescr a -> String+    fmtOpt (Option short long argDesc desc) =+      let shortStr = case short of+                       []    -> ""+                       (c:_) -> "-" ++ [c]+          longStrs  = map ("--" ++) long+          argStr    = case argDesc of+                        NoArg  _   -> ""+                        ReqArg _ m -> " " ++ m+                        OptArg _ m -> "[=" ++ m ++ "]"+          indentedDesc = unlines $ map ("        " ++) $ lines desc+          synopsis  = L.intercalate ", " $+                        [shortStr | not (null shortStr)] ++ longStrs+      in "  " ++ synopsis ++ argStr ++ "\n\n" ++ indentedDesc+ banner :: String-banner =  "\n\nLiquid-Fixpoint Copyright 2009-25 Regents of the University of California.\n"+banner =  "\nLiquid-Fixpoint Copyright 2009-25 Regents of the University of California.\n"        ++ "All Rights Reserved.\n"  restOC :: Config -> RESTOrdering

@@ -0,0 +1,45 @@+-- | Global verbosity IORef, replacing the one provided by @cmdargs@.+--   Use 'setVerbosity' after option parsing to control all 'whenLoud' /+--   'whenNormal' guards throughout the solver.+module Language.Fixpoint.Verbosity+  ( Verbosity (..)+  , setVerbosity+  , getVerbosity+  , whenLoud+  , whenNormal+  , isNormal+  , isLoud+  ) where++import Control.Monad      (when)+import Data.IORef         (IORef, newIORef, readIORef, writeIORef)+import System.IO.Unsafe   (unsafePerformIO)++data Verbosity = Quiet | Normal | Loud+  deriving (Eq, Ord, Show)++{-# NOINLINE verbosityRef #-}+verbosityRef :: IORef Verbosity+verbosityRef = unsafePerformIO (newIORef Normal)++setVerbosity :: Verbosity -> IO ()+setVerbosity = writeIORef verbosityRef++getVerbosity :: IO Verbosity+getVerbosity = readIORef verbosityRef++whenLoud :: IO () -> IO ()+whenLoud act = do+  v <- getVerbosity+  when (v >= Loud) act++whenNormal :: IO () -> IO ()+whenNormal act = do+  v <- getVerbosity+  when (v >= Normal) act++isNormal :: IO Bool+isNormal = (>= Normal) <$> getVerbosity++isLoud :: IO Bool+isLoud = (>= Loud) <$> getVerbosity

@@ -0,0 +1,1 @@+fixpoint "--numeric-version"

@@ -10,7 +10,7 @@ import Control.Monad (when) import qualified Control.Monad.State    as State import Control.Monad.Trans.Class (lift)-import Data.List (isSuffixOf)+import Data.List (dropWhileEnd, isSuffixOf) import Prelude hiding (log) import Data.Maybe (fromMaybe) import Data.Monoid (Sum(..))@@ -112,6 +112,14 @@         , dirHornTests "horn-smt2-pos-el" elimCmd     "tests/logs/cur/horn-pos-el" []         []             ExitSuccess         , dirHornTests "horn-smt2-neg-el" elimCmd     "tests/logs/cur/horn-neg-el" []         []            (ExitFailure 1)         ]+      , return $ testGroup "flags"+        [ testCase "--numeric-version" $ do+            (code, out, _) <- readProcessWithExitCode "fixpoint" ["--numeric-version"] ""+            assertEqual "Wrong exit code" ExitSuccess code+            let ver = dropWhileEnd (== '\n') out+            assertBool ("Expected a version number like X.Y.Z, got: " ++ show ver)+                       (not (null ver) && all isNumericSegment (splitOn '.' ver))+        ]       ]   where     posOptions = ["--save-bfq-on-error"]@@ -210,6 +218,19 @@  group :: Monad f => TestName -> [f TestTree] -> f TestTree group n xs = testGroup n <$> sequence xs++-- | Split a string on a delimiter character.+splitOn :: Char -> String -> [String]+splitOn _ [] = [""]+splitOn d (c:cs)+  | c == d    = "" : splitOn d cs+  | otherwise = case splitOn d cs of+      (w:ws) -> (c:w) : ws+      []     -> [c:""]++-- | A numeric version segment is a non-empty string of digits.+isNumericSegment :: String -> Bool+isNumericSegment s = not (null s) && all (\c -> c >= '0' && c <= '9') s  ---------------------------------------------------------------------------------------- walkDirectory :: FilePath -> IO [FilePath]

@@ -10,7 +10,7 @@  import           Control.Monad                    (when) import           System.IO.Unsafe                 (unsafePerformIO)-import           System.Console.CmdArgs.Verbosity (isNormal, getVerbosity, Verbosity(..))+import           Language.Fixpoint.Verbosity      (isNormal, getVerbosity, Verbosity(..)) import           Data.IORef import           System.Console.AsciiProgress -- import           Language.Fixpoint.Misc (traceShow)