# HG changeset patch # User blanchet # Date 1660311307 -7200 # Node ID 2b106aae897c7fa635d3e82ffe45cbd3d066edd6 # Parent 3581dcee70dbc5166ca6f7e3d456a056076e57d2 added support for cvc5 (whose interface is almost identical to CVC4) diff -r 3581dcee70db -r 2b106aae897c NEWS --- 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. diff -r 3581dcee70db -r 2b106aae897c src/Doc/Sledgehammer/document/root.tex --- 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}. diff -r 3581dcee70db -r 2b106aae897c src/Doc/manual.bib --- 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}}, diff -r 3581dcee70db -r 2b106aae897c src/HOL/SMT.thy --- 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 \Tools/SMT/z3_proof.ML\ ML_file \Tools/SMT/z3_isar.ML\ ML_file \Tools/SMT/smt_solver.ML\ -ML_file \Tools/SMT/cvc4_interface.ML\ +ML_file \Tools/SMT/cvc_interface.ML\ ML_file \Tools/SMT/lethe_proof.ML\ ML_file \Tools/SMT/lethe_isar.ML\ ML_file \Tools/SMT/lethe_proof_parse.ML\ -ML_file \Tools/SMT/cvc4_proof_parse.ML\ +ML_file \Tools/SMT/cvc_proof_parse.ML\ ML_file \Tools/SMT/verit_proof.ML\ ML_file \Tools/SMT/conj_disj_perm.ML\ ML_file \Tools/SMT/smt_replay_methods.ML\ @@ -691,6 +691,7 @@ \ declare [[cvc4_options = ""]] +declare [[cvc5_options = ""]] declare [[verit_options = ""]] declare [[z3_options = ""]] @@ -705,11 +706,11 @@ text \ 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. \ -declare [[cvc4_extensions = false]] +declare [[cvc_extensions = false]] text \ Enable the following option to use built-in support for div/mod, datatypes, @@ -890,6 +891,7 @@ "(if P then \ Q else R) \ \ P \ Q" "(if P then Q else \ R) \ P \ R" by auto + hide_type (open) symb_list pattern hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod diff -r 3581dcee70db -r 2b106aae897c src/HOL/Tools/SMT/cvc4_interface.ML --- 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; diff -r 3581dcee70db -r 2b106aae897c src/HOL/Tools/SMT/cvc4_proof_parse.ML --- 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; diff -r 3581dcee70db -r 2b106aae897c src/HOL/Tools/SMT/cvc_interface.ML --- /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; diff -r 3581dcee70db -r 2b106aae897c src/HOL/Tools/SMT/cvc_proof_parse.ML --- /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; diff -r 3581dcee70db -r 2b106aae897c src/HOL/Tools/SMT/smt_systems.ML --- 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>\cvc4_extensions\ (K false) +val cvc_extensions = Attrib.setup_config_bool \<^binding>\cvc_extensions\ (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)