--- a/NEWS Thu Aug 11 13:23:00 2022 +0200
+++ b/NEWS Fri Aug 12 15:35:07 2022 +0200
@@ -145,6 +145,7 @@
INCOMPATIBILITY.
- Added support for TX0 and TX1 TPTP formats and $ite/$let expressions
in TH0 and TH1.
+ - Added support for cvc5.
- Replaced option "sledgehammer_atp_dest_dir" by
"sledgehammer_atp_problem_dest_dir", for problem files, and
"sledgehammer_atp_proof_dest_dir", for proof files. Minor INCOMPATIBILITY.
--- a/src/Doc/Sledgehammer/document/root.tex Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Aug 12 15:35:07 2022 +0200
@@ -109,8 +109,9 @@
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 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}, cvc5 \cite{barbosa-et-al-cvc5}, 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
@@ -151,15 +152,15 @@
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.
+CVC4, cvc5, veriT, and Z3 can be run locally.
There are three main ways to install automatic provers on your machine:
\begin{sloppy}
\begin{enum}
\item[\labelitemi] If you installed an official Isabelle package, it should
-already include properly set up executables for CVC4, E, SPASS, Vampire, veriT,
-Z3, and Zipperposition ready to use.
+already include properly set up executables for CVC4, cvc5, E, SPASS, Vampire,
+veriT, Z3, and Zipperposition ready to use.
\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E,
SPASS, Vampire, veriT, Z3, and Zipperposition binary packages from \download.
@@ -191,10 +192,11 @@
\texttt{LEO3\_VERSION}, \texttt{SATALLAX\_VERSION}, or
\texttt{ZIPPERPOSITION\_VERSION} to the prover's version number (e.g., ``3.6'').
-Similarly, if you want to install CVC4, veriT, or Z3, set the environment
-variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{ISABELLE\_\allowbreak VERIT},
+Similarly, if you want to install CVC4, cvc5, veriT, or Z3, set the environment
+variable \texttt{CVC4\_\allowbreak SOLVER}, \texttt{CVC5\_\allowbreak SOLVER},
+\texttt{ISABELLE\_\allowbreak VERIT},
or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including
-the file name}. Ideally, also set \texttt{CVC4\_VERSION},
+the file name}. Ideally, also set \texttt{CVC4\_VERSION}, \texttt{CVC5\_VERSION},
\texttt{VERIT\_VERSION}, or \texttt{Z3\_VERSION} to the solver's version number
(e.g., ``4.4.0'').
\end{enum}
@@ -673,11 +675,16 @@
requires Alt-Ergo 0.95.2 and Why3 0.83.
\item[\labelitemi] \textbf{\textit{cvc4}:} CVC4 is an SMT solver developed by
-Clark Barrett, Cesare Tinelli, and their colleagues \cite{cvc4}. To use CVC4,
+Barrett et al.\ \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{cvc5}:} cvc5 is an SMT solver developed by
+Barbosa et al.\ \cite{barbosa-et-al-cvc5}. To use cvc5,
+set the environment variable \texttt{CVC5\_SOLVER} to the complete path of the
+executable, including the file name.
+
\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}
@@ -776,10 +783,10 @@
version of Zipperposition runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, and
-Z3 in parallel, either locally or remotely---depending on the number of
-processor cores available and on which provers are actually installed. It is
-generally desirable to run several provers in parallel.
+By default, Sledgehammer runs a subset of CVC4, E, SPASS, Vampire, veriT, Z3,
+and Zipperposition in parallel, either locally or remotely---depending on the
+number of processor cores available and on which provers are actually installed.
+It is generally beneficial to run several provers in parallel.
\opnodefault{prover}{string}
Alias for \textit{provers}.
--- a/src/Doc/manual.bib Thu Aug 11 13:23:00 2022 +0200
+++ b/src/Doc/manual.bib Fri Aug 12 15:35:07 2022 +0200
@@ -181,6 +181,36 @@
editor = {A. Robinson and A. Voronkov}
}
+@inproceedings{barbosa-et-al-cvc5,
+ author = {Haniel Barbosa and
+ Clark W. Barrett and
+ Martin Brain and
+ Gereon Kremer and
+ Hanna Lachnitt and
+ Makai Mann and
+ Abdalrhman Mohamed and
+ Mudathir Mohamed and
+ Aina Niemetz and
+ Andres N{\"{o}}tzli and
+ Alex Ozdemir and
+ Mathias Preiner and
+ Andrew Reynolds and
+ Ying Sheng and
+ Cesare Tinelli and
+ Yoni Zohar},
+ editor = {Dana Fisman and
+ Grigore Rosu},
+ title = {{cvc5}: A Versatile and Industrial-Strength {SMT} Solver},
+ booktitle = "Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2022 (I)",
+ series = {Lecture Notes in Computer Science},
+ volume = {13243},
+ pages = {415--442},
+ publisher = {Springer},
+ year = {2022},
+ XXXurl = {https://doi.org/10.1007/978-3-030-99524-9\_24},
+ XXXdoi = {10.1007/978-3-030-99524-9\_24},
+}
+
@inproceedings{cvc3,
author = {Clark Barrett and Cesare Tinelli},
title = {{CVC3}},
--- a/src/HOL/SMT.thy Thu Aug 11 13:23:00 2022 +0200
+++ b/src/HOL/SMT.thy Fri Aug 12 15:35:07 2022 +0200
@@ -622,11 +622,11 @@
ML_file \<open>Tools/SMT/z3_proof.ML\<close>
ML_file \<open>Tools/SMT/z3_isar.ML\<close>
ML_file \<open>Tools/SMT/smt_solver.ML\<close>
-ML_file \<open>Tools/SMT/cvc4_interface.ML\<close>
+ML_file \<open>Tools/SMT/cvc_interface.ML\<close>
ML_file \<open>Tools/SMT/lethe_proof.ML\<close>
ML_file \<open>Tools/SMT/lethe_isar.ML\<close>
ML_file \<open>Tools/SMT/lethe_proof_parse.ML\<close>
-ML_file \<open>Tools/SMT/cvc4_proof_parse.ML\<close>
+ML_file \<open>Tools/SMT/cvc_proof_parse.ML\<close>
ML_file \<open>Tools/SMT/verit_proof.ML\<close>
ML_file \<open>Tools/SMT/conj_disj_perm.ML\<close>
ML_file \<open>Tools/SMT/smt_replay_methods.ML\<close>
@@ -691,6 +691,7 @@
\<close>
declare [[cvc4_options = ""]]
+declare [[cvc5_options = ""]]
declare [[verit_options = ""]]
declare [[z3_options = ""]]
@@ -705,11 +706,11 @@
text \<open>
Enable the following option to use built-in support for datatypes,
-codatatypes, and records in CVC4. Currently, this is implemented only
-in oracle mode.
+codatatypes, and records in CVC4 and cvc5. Currently, this is implemented
+only in oracle mode.
\<close>
-declare [[cvc4_extensions = false]]
+declare [[cvc_extensions = false]]
text \<open>
Enable the following option to use built-in support for div/mod, datatypes,
@@ -890,6 +891,7 @@
"(if P then \<not> Q else R) \<or> \<not> P \<or> Q"
"(if P then Q else \<not> R) \<or> P \<or> R"
by auto
+
hide_type (open) symb_list pattern
hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod
--- a/src/HOL/Tools/SMT/cvc4_interface.ML Thu Aug 11 13:23:00 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(* Title: HOL/Tools/SMT/cvc4_interface.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-Interface to CVC4 based on an extended version of SMT-LIB.
-*)
-
-signature CVC4_INTERFACE =
-sig
- val smtlib_cvc4C: SMT_Util.class
- val hosmtlib_cvc4C: SMT_Util.class
-end;
-
-structure CVC4_Interface: CVC4_INTERFACE =
-struct
-
-val cvc4C = ["cvc4"]
-val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
-val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
-
-
-(* interface *)
-
-local
- fun translate_config order ctxt =
- {order = order,
- logic = K (K "(set-logic ALL_SUPPORTED)\n"),
- fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
- serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
-in
-
-val _ = Theory.setup (Context.theory_map
- (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
- SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
-
-end
-
-end;
--- a/src/HOL/Tools/SMT/cvc4_proof_parse.ML Thu Aug 11 13:23:00 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* Title: HOL/Tools/SMT/cvc4_proof_parse.ML
- Author: Jasmin Blanchette, TU Muenchen
-
-CVC4 proof (actually, unsat core) parsing.
-*)
-
-signature CVC4_PROOF_PARSE =
-sig
- val parse_proof: SMT_Translate.replay_data ->
- ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
- SMT_Solver.parsed_proof
-end;
-
-structure CVC4_Proof_Parse: CVC4_PROOF_PARSE =
-struct
-
-fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output =
- if exists (String.isPrefix "(error \"This build of CVC4 doesn't have proof support") output then
- {outcome = NONE, fact_ids = NONE, atp_proof = K []}
- else
- let
- val num_ll_defs = length ll_defs
-
- val id_of_index = Integer.add num_ll_defs
- val index_of_id = Integer.add (~ num_ll_defs)
-
- val used_assert_ids =
- map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output
- val used_assm_js =
- map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
- used_assert_ids
-
- val conjecture_i = 0
- val prems_i = conjecture_i + 1
- val num_prems = length prems
- val facts_i = prems_i + num_prems
-
- val fact_ids' =
- map_filter (fn j =>
- let val ((i, _), _) = nth assms j in
- try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
- end) used_assm_js
- in
- {outcome = NONE, fact_ids = SOME fact_ids', atp_proof = K []}
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/cvc_interface.ML Fri Aug 12 15:35:07 2022 +0200
@@ -0,0 +1,37 @@
+(* Title: HOL/Tools/SMT/cvc_interface.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+Interface to CVC4 and cvc5 based on an extended version of SMT-LIB.
+*)
+
+signature CVC_INTERFACE =
+sig
+ val smtlib_cvcC: SMT_Util.class
+ val hosmtlib_cvcC: SMT_Util.class
+end;
+
+structure CVC_Interface: CVC_INTERFACE =
+struct
+
+val cvcC = ["cvc"]
+val smtlib_cvcC = SMTLIB_Interface.smtlibC @ cvcC
+val hosmtlib_cvcC = SMTLIB_Interface.hosmtlibC @ cvcC
+
+
+(* interface *)
+
+local
+ fun translate_config order ctxt =
+ {order = order,
+ logic = K (K "(set-logic ALL_SUPPORTED)\n"),
+ fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+ serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
+in
+
+val _ = Theory.setup (Context.theory_map
+ (SMT_Translate.add_config (smtlib_cvcC, translate_config SMT_Util.First_Order) #>
+ SMT_Translate.add_config (hosmtlib_cvcC, translate_config SMT_Util.Higher_Order)))
+
+end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/cvc_proof_parse.ML Fri Aug 12 15:35:07 2022 +0200
@@ -0,0 +1,47 @@
+(* Title: HOL/Tools/SMT/cvc_proof_parse.ML
+ Author: Jasmin Blanchette, TU Muenchen
+
+CVC4 and cvc5 proof (actually, unsat core) parsing.
+*)
+
+signature CVC_PROOF_PARSE =
+sig
+ val parse_proof: SMT_Translate.replay_data ->
+ ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
+ SMT_Solver.parsed_proof
+end;
+
+structure CVC_Proof_Parse: CVC_PROOF_PARSE =
+struct
+
+fun parse_proof ({ll_defs, assms, ...} : SMT_Translate.replay_data) xfacts prems _ output =
+ if exists (String.isPrefix "(error \"This build of CVC4 doesn't have proof support") output then
+ {outcome = NONE, fact_ids = NONE, atp_proof = K []}
+ else
+ let
+ val num_ll_defs = length ll_defs
+
+ val id_of_index = Integer.add num_ll_defs
+ val index_of_id = Integer.add (~ num_ll_defs)
+
+ val used_assert_ids =
+ map_filter (try (snd o SMTLIB_Interface.role_and_index_of_assert_name)) output
+ val used_assm_js =
+ map_filter (fn id => let val i = index_of_id id in if i >= 0 then SOME i else NONE end)
+ used_assert_ids
+
+ val conjecture_i = 0
+ val prems_i = conjecture_i + 1
+ val num_prems = length prems
+ val facts_i = prems_i + num_prems
+
+ val fact_ids' =
+ map_filter (fn j =>
+ let val ((i, _), _) = nth assms j in
+ try (apsnd (nth xfacts)) (id_of_index j, i - facts_i)
+ end) used_assm_js
+ in
+ {outcome = NONE, fact_ids = SOME fact_ids', atp_proof = K []}
+ end
+
+end;
--- a/src/HOL/Tools/SMT/smt_systems.ML Thu Aug 11 13:23:00 2022 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Fri Aug 12 15:35:07 2022 +0200
@@ -6,7 +6,7 @@
signature SMT_SYSTEMS =
sig
- val cvc4_extensions: bool Config.T
+ val cvc_extensions: bool Config.T
val z3_extensions: bool Config.T
end;
@@ -59,9 +59,9 @@
on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines)
-(* CVC4 *)
+(* CVC4 and cvc5 *)
-val cvc4_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc4_extensions\<close> (K false)
+val cvc_extensions = Attrib.setup_config_bool \<^binding>\<open>cvc_extensions\<close> (K false)
local
fun cvc4_options ctxt =
@@ -72,12 +72,20 @@
NONE => []
| SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)])
+ fun cvc5_options ctxt =
+ ["--no-stats",
+ "--sat-random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
+ "--lang=smt2"] @
+ (case SMT_Config.get_timeout ctxt of
+ NONE => []
+ | SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)])
+
fun select_class ctxt =
- if Config.get ctxt cvc4_extensions then
+ if Config.get ctxt cvc_extensions then
if Config.get ctxt SMT_Config.higher_order then
- CVC4_Interface.hosmtlib_cvc4C
+ CVC_Interface.hosmtlib_cvcC
else
- CVC4_Interface.smtlib_cvc4C
+ CVC_Interface.smtlib_cvcC
else
if Config.get ctxt SMT_Config.higher_order then
SMTLIB_Interface.hosmtlibC
@@ -104,7 +112,27 @@
((1, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
((1, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
- parse_proof = SOME (K CVC4_Proof_Parse.parse_proof),
+ parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
+ replay = NONE }
+
+val cvc5: SMT_Solver.solver_config = {
+ name = "cvc5",
+ class = select_class,
+ avail = make_avail "CVC5",
+ command = make_command "CVC5",
+ options = cvc5_options,
+ smt_options = [(":produce-unsat-cores", "true")],
+ good_slices =
+ (* FUDGE *)
+ [((1, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]),
+ ((1, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]),
+ ((1, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]),
+ ((1, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]),
+ ((1, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]),
+ ((1, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]),
+ ((1, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])],
+ outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"),
+ parse_proof = SOME (K CVC_Proof_Parse.parse_proof),
replay = NONE }
end
@@ -228,6 +256,7 @@
val _ = Theory.setup (
SMT_Solver.add_solver cvc4 #>
+ SMT_Solver.add_solver cvc5 #>
SMT_Solver.add_solver veriT #>
SMT_Solver.add_solver z3)