Merge pull request #2513 from clayrat/cvc5-opt

scan for cvc5 before cvc4 + generate the error msg for missing smt

Author: facundominguez

liquidhaskell-boot/src/Language/Haskell/Liquid/UX/CmdLine.hs

@@ -59,7 +59,7 @@ import System.Console.CmdArgs.Implicit     hiding (Verbosity(..))
 import System.Console.CmdArgs.Text
 import GitHash
 
-import Data.List                           (nub)
+import Data.List                           (nub, intercalate)
 
 
 import System.FilePath                     (isAbsolute, takeDirectory, (</>))
@@ -376,7 +376,7 @@ config = cmdArgsMode $ Config {
     = def
         &= help "Eta expand and beta reduce terms to aid PLE"
         &= name "etabeta"
-  
+
   , dependantCase
     = def
         &= help "Allow PLE to reason about dependent cases"
@@ -524,12 +524,13 @@ withSmtSolver cfg =
                    case found of
                      Just _ -> return cfg
                      Nothing -> panic Nothing (missingSmtError smt)
-    Nothing  -> do smts <- mapM findSmtSolver [FC.Z3, FC.Cvc4, FC.Mathsat]
+    Nothing  -> do smts <- mapM findSmtSolver smtLookupOrder
                    case catMaybes smts of
                      (s:_) -> return (cfg {smtsolver = Just s})
                      _     -> panic Nothing noSmtError
   where
-    noSmtError = "LiquidHaskell requires an SMT Solver, i.e. z3, cvc4, or mathsat to be installed."
+    smtLookupOrder = [FC.Z3, FC.Cvc5, FC.Cvc4, FC.Mathsat]
+    noSmtError = "LiquidHaskell requires one of the following SMT solvers to be installed: " ++ intercalate ", " (show <$> smtLookupOrder) ++ "."
     missingSmtError smt = "Could not find SMT solver '" ++ show smt ++ "'. Is it on your PATH?"
 
 findSmtSolver :: FC.SMTSolver -> IO (Maybe FC.SMTSolver)

liquidhaskell-boot/src/Language/Haskell/Liquid/UX/Config.hs

@@ -74,7 +74,7 @@ data Config = Config
   , minPartSize              :: Int        -- ^ Minimum size of a partition
   , maxPartSize              :: Int        -- ^ Maximum size of a partition. Overrides minPartSize
   , maxParams                :: Int        -- ^ the maximum number of parameters to accept when mining qualifiers
-  , smtsolver                :: Maybe SMTSolver  -- ^ name of smtsolver to use [default: try z3, cvc4, mathsat in order]
+  , smtsolver                :: Maybe SMTSolver  -- ^ SMT solver to use [if `Nothing`, try looking one up using the order defined in L.H.L.UX.CmdLine.withSmtSolver]
   , shortNames               :: Bool       -- ^ drop module qualifers from pretty-printed names.
   , shortErrors              :: Bool       -- ^ don't show subtyping errors and contexts.
   , cabalDir                 :: Bool       -- ^ find and use .cabal file to include paths to sources for imported modules
@@ -111,11 +111,11 @@ data Config = Config
   , compileSpec              :: Bool       -- ^ Only "compile" the spec -- into .bspec file -- don't do any checking.
   , noCheckImports           :: Bool       -- ^ Do not check the transitive imports
   , typeclass                :: Bool        -- ^ enable typeclass support.
-  , auxInline                :: Bool        -- ^ 
+  , auxInline                :: Bool        -- ^
   , rwTerminationCheck       :: Bool       -- ^ Enable termination checking for rewriting
   , skipModule               :: Bool       -- ^ Skip this module entirely (don't even compile any specs in it)
   , noLazyPLE                :: Bool
-  , fuel                     :: Maybe Int  -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite) 
+  , fuel                     :: Maybe Int  -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite)
   , environmentReduction     :: Bool       -- ^ Perform environment reduction
   , noEnvironmentReduction   :: Bool       -- ^ Don't perform environment reduction
   , inlineANFBindings        :: Bool       -- ^ Inline ANF bindings.