# HG changeset patch # User blanchet # Date 1626698872 -7200 # Node ID a0c9fc9c7dbeda95ceba91c61b02d8c74b3834e5 # Parent a2b470e315eeecd1fddc664c2618515dcc0042fe removed setup for outdated CVC3 from Isabelle diff -r a2b470e315ee -r a0c9fc9c7dbe src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Mon Jul 19 14:47:52 2021 +0200 +++ b/src/Doc/Sledgehammer/document/root.tex Mon Jul 19 14:47:52 2021 +0200 @@ -109,8 +109,8 @@ Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely via the System\-On\-TPTP web service \cite{sutcliffe-2000}. The supported SMT -solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, -and Z3 \cite{de-moura-2008}. These are always run locally. +solvers are CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, and Z3 +\cite{de-moura-2008}. These are always run locally. The problem passed to the external provers (or solvers) consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the @@ -147,12 +147,11 @@ Sledgehammer is part of Isabelle, so you do not need to install it. However, it relies on third-party automatic provers (ATPs and SMT solvers). -Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, -Vampire, and Zipperposition can be run locally; in addition, agsyHOL, -Alt-Ergo, E, iProver, LEO-II, Leo-III, Satallax, Vampire, Waldmeister, -and Zipperposition are available remotely via System\-On\-TPTP -\cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run -locally. +Among the ATPs, agsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, +and Zipperposition can be run locally; in addition, agsyHOL, Alt-Ergo, E, +iProver, LEO-II, Leo-III, Satallax, Vampire, Waldmeister, and Zipperposition are +available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers +CVC4, veriT, and Z3 can be run locally. There are three main ways to install automatic provers on your machine: @@ -164,9 +163,9 @@ noncommercial user, as indicated by the message that is displayed when Sledgehammer is invoked the first time. -\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, -CVC4, E, SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract -the archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash +\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E, +SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract the +archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash components}% \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at startup. Its value can be retrieved by executing \texttt{isabelle} @@ -194,12 +193,12 @@ \texttt{LEO3\_VERSION}, or \texttt{SATALLAX\_VERSION} to the prover's version number (e.g., ``3.6''). -Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment -variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER}, -\texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path -of the executable, \emph{including the file name}. Ideally, also set -\texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or -\texttt{Z3\_VERSION} to the solver's version number (e.g., ``4.4.0''). +Similarly, if you want to install CVC4, veriT, or Z3, set the environment +variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{VERIT\_\allowbreak SOLVER}, +or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including +the file name}. Ideally, also set \texttt{CVC4\_VERSION}, +\texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number +(e.g., ``4.4.0''). \end{enum} \end{sloppy} @@ -691,17 +690,12 @@ to the directory that contains the \texttt{why3} executable. Sledgehammer requires Alt-Ergo 0.95.2 and Why3 0.83. -\item[\labelitemi] \textbf{\textit{cvc3}:} CVC3 is an SMT solver developed by -Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc3}. To use CVC3, -set the environment variable \texttt{CVC3\_SOLVER} to the complete path of the -executable, including the file name, or install the prebuilt CVC3 package from +\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 is an SMT solver developed by +Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc4}. To use CVC4, +set the environment variable \texttt{CVC4\_SOLVER} to the complete path of the +executable, including the file name, or install the prebuilt CVC4 package from \download. -\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 \cite{cvc4} is the successor to -CVC3. To use CVC4, set the environment variable \texttt{CVC4\_SOLVER} to the -complete path of the executable, including the file name, or install the -prebuilt CVC4 package from \download. - \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} diff -r a2b470e315ee -r a0c9fc9c7dbe src/HOL/SMT.thy --- a/src/HOL/SMT.thy Mon Jul 19 14:47:52 2021 +0200 +++ b/src/HOL/SMT.thy Mon Jul 19 14:47:52 2021 +0200 @@ -687,7 +687,6 @@ options. \ -declare [[cvc3_options = ""]] declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] declare [[verit_options = ""]] declare [[z3_options = ""]] diff -r a2b470e315ee -r a0c9fc9c7dbe src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML Mon Jul 19 14:47:52 2021 +0200 +++ b/src/HOL/Tools/SMT/smt_systems.ML Mon Jul 19 14:47:52 2021 +0200 @@ -54,31 +54,6 @@ fun on_first_non_unsupported_line test_outcome solver_name lines = on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines) -(* CVC3 *) - -local - fun cvc3_options ctxt = - ["-seed", string_of_int (Config.get ctxt SMT_Config.random_seed), - "-lang", "smt2"] @ - (case SMT_Config.get_timeout ctxt of - NONE => [] - | SOME t => ["-timeout", string_of_int (Real.ceil (Time.toReal t))]) -in - -val cvc3: SMT_Solver.solver_config = { - name = "cvc3", - class = K SMTLIB_Interface.smtlibC, - avail = make_avail "CVC3", - command = make_command "CVC3", - options = cvc3_options, - smt_options = [], - default_max_relevant = 400 (* FUDGE *), - outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), - parse_proof = NONE, - replay = NONE } - -end - (* CVC4 *) @@ -219,7 +194,6 @@ (* overall setup *) val _ = Theory.setup ( - SMT_Solver.add_solver cvc3 #> SMT_Solver.add_solver cvc4 #> SMT_Solver.add_solver veriT #> SMT_Solver.add_solver z3)