# HG changeset patch # User nipkow # Date 1676897956 -3600 # Node ID fa247805669d2c819e8d3fa3bf6f7cdae3dc9a97 # Parent f02c8a45c4c11a58d8181903455811fac9ce1785# Parent 6470353996f54fa79bc098fa200973ce5fc8c75a merge in backouts diff -r f02c8a45c4c1 -r fa247805669d NEWS --- a/NEWS Mon Feb 20 13:55:58 2023 +0100 +++ b/NEWS Mon Feb 20 13:59:16 2023 +0100 @@ -224,6 +224,15 @@ * Mirabelle: - Added session to output directory structure. Minor INCOMPATIBILITY. +* Metis: + - Made clausifier more robust in the face of nested lambdas. + Minor INCOMPATIBILITY. + +* Sledgehammer: + - Added refutational mode to find likely unprovable conectures. It is + enabled by default in addition to the usual proving mode and can be + enabled or disabled using the 'refute' option. + *** ML *** diff -r f02c8a45c4c1 -r fa247805669d src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Mon Feb 20 13:55:58 2023 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Mon Feb 20 13:59:16 2023 +0100 @@ -99,9 +99,10 @@ \label{introduction} Sledgehammer is a tool that applies automatic theorem provers (ATPs) -and satisfiability-modulo-theories (SMT) solvers on the current goal.% -\footnote{The distinction between ATPs and SMT solvers is convenient but mostly -historical.} +and satisfiability-modulo-theories (SMT) solvers on the current goal, mostly +to find proofs but also to find inconsistencies.% +\footnote{The distinction between ATPs and SMT solvers is mostly +historical but convenient.} % The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E \cite{schulz-2019}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III @@ -113,9 +114,9 @@ \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 -current theory context, filtered by relevance. +The problem passed to the automatic provers (or solvers) consists of your +current goal together with a heuristic selection of hundreds of facts (theorems) +from the current theory context, filtered by relevance. The result of a successful proof search is some source text that typically reconstructs the proof within Isabelle. For ATPs, the reconstructed proof @@ -123,6 +124,10 @@ integrates the Metis ATP in Isabelle/HOL with explicit inferences going through the kernel. Thus its results are correct by construction. +Sometimes the automatic provers might detect that the goal is inconsistent with +the background facts---or even that the background facts are inconsistent +regardless of of the goal. + For Isabelle/jEdit users, Sledgehammer provides an automatic mode that can be enabled via the ``Auto Sledgehammer'' option under ``Plugins > Plugin Options > Isabelle > General.'' In this mode, a reduced version of Sledgehammer is run on @@ -162,9 +167,9 @@ 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. -Extract the archives, then add a line to your +\item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, +cvc5, E, SPASS, Vampire, veriT, Z3, and Zipperposition 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} @@ -225,8 +230,8 @@ \postw Instead of issuing the \textbf{sledgehammer} command, you can also use the -Sledgehammer panel in Isabelle/jEdit. Sledgehammer might produce something like -the following output after a few seconds: +Sledgehammer panel in Isabelle/jEdit. Either way, Sledgehammer will produce +something like the following output after a few seconds: \prew \slshape @@ -238,7 +243,7 @@ cvc4: Try this: \textbf{by} \textit{simp} (0.4 ms) \\ z3: Try this: \textbf{by} \textit{simp} (0.5 ms) \\ vampire: Try this: \textbf{by} \textit{simp} (0.3 ms) \\ -QED +Done \postw Sledgehammer ran CVC4, E, Vampire, Z3, and possibly other provers in parallel. @@ -260,6 +265,23 @@ readable and also faster than \textit{metis} or \textit{smt} one-line proofs. This feature is experimental. +For goals that are inconsistent with the background theory (and hence unprovable +unless the theory is itself inconsistent), such as + +\prew +\textbf{lemma} ``$\mathit{length}\; (\mathit{zip}\; \mathit{xs}\; \mathit{ys}) = \mathit{length}\; \mathit{xs}$'' \\ +\textbf{sledgehammer} +\postw + +Sledgehammer's output might look as follows: + +\prew +\slshape +vampire found an inconsistency\ldots \\ +vampire: The goal is inconsistent with these facts: append\_Cons, nth\_append\_length, self\_append\_conv2, zip\_eq\_Nil\_iff +Done +\postw + \section{Hints} \label{hints} @@ -791,6 +813,16 @@ \opnodefault{prover}{string} Alias for \textit{provers}. +\opsmart{check\_consistent}{dont\_check\_consistent} +Specifies whether Sledgehammer should look for inconsistencies or for proofs. By +default, it looks for both proofs and inconsistencies. + +An inconsistency indicates that the goal, taken as an axiom, would be +inconsistent with some specific background facts if it were added as a lemma, +indicating a likely issue with the goal. Sometimes the inconsistency involves +only the background theory; this might happen, for example, if an axiom is used +or if a lemma was introduced with \textbf{sorry}. + \optrue{minimize}{dont\_minimize} Specifies whether the proof minimization tool should be invoked automatically after proof search. diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Data_Structures/RBT_Map.thy --- a/src/HOL/Data_Structures/RBT_Map.thy Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Data_Structures/RBT_Map.thy Mon Feb 20 13:59:16 2023 +0100 @@ -24,11 +24,11 @@ fun del :: "'a::linorder \ ('a*'b)rbt \ ('a*'b)rbt" where "del x Leaf = Leaf" | -"del x (Node l ((a,b), c) r) = (case cmp x a of +"del x (Node l (ab, _) r) = (case cmp x (fst ab) of LT \ if l \ Leaf \ color l = Black - then baldL (del x l) (a,b) r else R (del x l) (a,b) r | + then baldL (del x l) ab r else R (del x l) ab r | GT \ if r \ Leaf\ color r = Black - then baldR l (a,b) (del x r) else R l (a,b) (del x r) | + then baldR l ab (del x r) else R l ab (del x r) | EQ \ join l r)" definition delete :: "'a::linorder \ ('a*'b) rbt \ ('a*'b) rbt" where @@ -46,10 +46,14 @@ "sorted1(inorder t) \ inorder(update x y t) = upd_list x y (inorder t)" by(simp add: update_def inorder_upd inorder_paint) +(* This lemma became necessary below when \del\ was converted from pattern-matching to \fst\ *) +lemma del_list_id: "\ab\set ps. y < fst ab \ x \ y \ del_list x ps = ps" +by(rule del_list_idem) auto + lemma inorder_del: "sorted1(inorder t) \ inorder(del x t) = del_list x (inorder t)" by(induction x t rule: del.induct) - (auto simp: del_list_simps inorder_join inorder_baldL inorder_baldR) + (auto simp: del_list_simps del_list_id inorder_join inorder_baldL inorder_baldR) lemma inorder_delete: "sorted1(inorder t) \ inorder(delete x t) = del_list x (inorder t)" @@ -81,19 +85,19 @@ (color t = Red \ bheight (del x t) = bheight t \ invc (del x t) \ color t = Black \ bheight (del x t) = bheight t - 1 \ invc2 (del x t))" proof (induct x t rule: del.induct) -case (2 x _ y _ c) - have "x = y \ x < y \ x > y" by auto +case (2 x _ ab c) + have "x = fst ab \ x < fst ab \ x > fst ab" by auto thus ?case proof (elim disjE) - assume "x = y" + assume "x = fst ab" with 2 show ?thesis by (cases c) (simp_all add: invh_join invc_join) next - assume "x < y" + assume "x < fst ab" with 2 show ?thesis by(cases c) (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD) next - assume "y < x" + assume "fst ab < x" with 2 show ?thesis by(cases c) (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD) diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Metis.thy --- a/src/HOL/Metis.thy Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Metis.thy Mon Feb 20 13:59:16 2023 +0100 @@ -27,7 +27,8 @@ lemma not_atomize_select: "(\ A \ select False) \ Trueprop A" unfolding select_def by (rule not_atomize) -lemma select_FalseI: "False \ select False" by simp +lemma select_FalseI: "False \ select False" +by simp definition lambda :: "'a \ 'a" where "lambda = (\x. x)" diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Feb 20 13:59:16 2023 +0100 @@ -24,7 +24,6 @@ ProofMissing | ProofIncomplete | ProofUnparsable | - UnsoundProof of bool * string list | TimedOut | Inappropriate | OutOfResources | @@ -143,7 +142,6 @@ ProofMissing | ProofIncomplete | ProofUnparsable | - UnsoundProof of bool * string list | TimedOut | Inappropriate | OutOfResources | @@ -160,21 +158,12 @@ else "" -fun from_lemmas [] = "" - | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) - fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" | string_of_atp_failure Unprovable = "Unprovable problem" | string_of_atp_failure GaveUp = "Gave up" | string_of_atp_failure ProofMissing = "Proof missing" | string_of_atp_failure ProofIncomplete = "Proof incomplete" | string_of_atp_failure ProofUnparsable = "Proof unparsable" - | string_of_atp_failure (UnsoundProof (false, ss)) = - "Derived the lemma \"False\"" ^ from_lemmas ss ^ - ", probably due to the use of an unsound type encoding" - | string_of_atp_failure (UnsoundProof (true, ss)) = - "Derived the lemma \"False\"" ^ from_lemmas ss ^ - ", which could be due to a bug in Sledgehammer or to inconsistent axioms (including \"sorry\"s)" | string_of_atp_failure TimedOut = "Timed out" | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" | string_of_atp_failure OutOfResources = "Out of resources" @@ -184,8 +173,7 @@ | string_of_atp_failure Crashed = "Crashed" | string_of_atp_failure InternalError = "Internal prover error" | string_of_atp_failure (UnknownError s) = - "Prover error" ^ - (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s) + "Prover error" ^ (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s) fun extract_delimited (begin_delim, end_delim) output = (case first_field begin_delim output of diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Feb 20 13:59:16 2023 +0100 @@ -46,8 +46,6 @@ val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof -> (string * stature) list - val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list -> 'a atp_proof -> - string list option val atp_proof_prefers_lifting : string atp_proof -> bool val is_typed_helper_used_in_atp_proof : string atp_proof -> bool val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step -> @@ -519,19 +517,6 @@ fun used_facts_in_atp_proof ctxt facts atp_proof = if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof [] -fun used_facts_in_unsound_atp_proof _ _ [] = NONE - | used_facts_in_unsound_atp_proof ctxt facts atp_proof = - let - val used_facts = used_facts_in_atp_proof ctxt facts atp_proof - val all_global_facts = forall (fn (_, (sc, _)) => sc = Global) used_facts - val axiom_used = is_axiom_used_in_proof (is_some o resolve_conjecture) atp_proof - in - if all_global_facts andalso not axiom_used then - SOME (map fst used_facts) - else - NONE - end - val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix (* overapproximation (good enough) *) diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Mon Feb 20 13:59:16 2023 +0100 @@ -54,8 +54,21 @@ let val T = fastype_of t in \<^Const>\Meson.skolem T for t\ end +fun eta_expand_All_Ex_arg ((cst as (Const _)) $ Abs (s, T, t')) = + cst $ Abs (s, T, eta_expand_All_Ex_arg t') + | eta_expand_All_Ex_arg ((cst as (Const (cst_s, cst_T))) $ t') = + if member (op =) [\<^const_name>\All\, \<^const_name>\Ex\] cst_s then + cst $ Abs (Name.uu, domain_type (domain_type cst_T), + incr_boundvars 1 (eta_expand_All_Ex_arg t') $ Bound 0) + else + cst $ eta_expand_All_Ex_arg t' + | eta_expand_All_Ex_arg (Abs (s, T, t')) = Abs (s, T, eta_expand_All_Ex_arg t') + | eta_expand_All_Ex_arg (t1 $ t2) = + eta_expand_All_Ex_arg t1 $ eta_expand_All_Ex_arg t2 + | eta_expand_All_Ex_arg t = t + fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t') - | beta_eta_in_abs_body t = Envir.beta_eta_contract t + | beta_eta_in_abs_body t = eta_expand_All_Ex_arg (Envir.beta_eta_contract t) (*Traverse a theorem, accumulating Skolem function definitions.*) fun old_skolem_defs th = diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/SMT/smt_solver.ML Mon Feb 20 13:59:16 2023 +0100 @@ -21,7 +21,7 @@ command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, - good_slices: ((int * int * string) * string list) list, + good_slices: ((int * bool * bool * int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> @@ -30,7 +30,8 @@ (*registry*) val add_solver: solver_config -> theory -> theory - val good_slices: Proof.context -> string -> ((int * int * string) * string list) list + val good_slices: Proof.context -> string -> + ((int * bool * bool * int * string) * string list) list (*filter*) val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list -> @@ -155,7 +156,7 @@ command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, - good_slices: ((int * int * string) * string list) list, + good_slices: ((int * bool * bool * int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> @@ -180,7 +181,7 @@ type solver_info = { command: unit -> string list, smt_options: (string * string) list, - good_slices: ((int * int * string) * string list) list, + good_slices: ((int * bool * bool * int * string) * string list) list, parse_proof: Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof, diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/SMT/smt_systems.ML Mon Feb 20 13:59:16 2023 +0100 @@ -104,13 +104,13 @@ smt_options = [(":produce-unsat-cores", "true")], good_slices = (* FUDGE *) - [((2, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), - ((2, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), - ((2, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), - ((2, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), - ((2, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), - ((2, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]), - ((2, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])], + [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), + ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), + ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), + ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), + ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), + ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]), + ((2, false, false, 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 } @@ -124,13 +124,13 @@ smt_options = [(":produce-unsat-cores", "true")], good_slices = (* FUDGE *) - [((2, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), - ((2, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), - ((2, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), - ((2, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), - ((2, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), - ((2, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]), - ((2, 256, meshN), ["--finite-model-find", "--fmf-inst-engine"])], + [((2, false, false, 512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), + ((2, false, false, 64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), + ((2, false, true, 256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), + ((2, false, false, 1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), + ((2, false, false, 32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), + ((2, false, false, 128, meshN), ["--no-e-matching", "--full-saturate-quant"]), + ((2, false, false, 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 } @@ -169,12 +169,12 @@ smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) - [((2, 1024, meshN), []), - ((2, 512, mashN), []), - ((2, 64, meshN), []), - ((2, 128, meshN), []), - ((2, 256, mepoN), []), - ((2, 32, meshN), [])], + [((2, false, false, 1024, meshN), []), + ((2, false, false, 512, mashN), []), + ((2, false, true, 128, meshN), []), + ((2, false, false, 64, meshN), []), + ((2, false, false, 256, mepoN), []), + ((2, false, false, 32, meshN), [])], outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"), parse_proof = SOME (K Lethe_Proof_Parse.parse_proof), replay = SOME Verit_Replay.replay } @@ -210,12 +210,12 @@ smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) - [((2, 1024, meshN), []), - ((2, 512, mepoN), []), - ((2, 64, meshN), []), - ((2, 256, meshN), []), - ((2, 128, mashN), []), - ((2, 32, meshN), [])], + [((2, false, false, 1024, meshN), []), + ((2, false, false, 512, mepoN), []), + ((2, false, false, 64, meshN), []), + ((2, false, true, 256, meshN), []), + ((2, false, false, 128, mashN), []), + ((2, false, false, 32, meshN), [])], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME Z3_Replay.parse_proof, replay = SOME Z3_Replay.replay } @@ -250,7 +250,7 @@ Theory.setup (Method.setup \<^binding>\smt\ (Scan.lift parse_smt_options -- Attrib.thms >> (METHOD oo smt_method)) - "Call to the SMT solvers veriT or z3") + "Call to the SMT solver veriT or z3") (* overall setup *) diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 20 13:59:16 2023 +0100 @@ -70,6 +70,12 @@ | alternative _ NONE (y as SOME _) = y | alternative _ NONE NONE = NONE +fun varify_nonfixed_terms_global nonfixeds tm = tm + |> Same.commit (Term_Subst.map_aterms_same + (fn Free (x, T) => if member (op =) nonfixeds x then Var ((x, 0), T) else raise Same.SAME + | Var (xi, _) => raise TERM (Logic.bad_schematic xi, [tm]) + | _ => raise Same.SAME)) + fun max_outcome outcomes = let val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes @@ -148,17 +154,20 @@ fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) - (slice as ((slice_size, num_facts, fact_filter), _)) name = + (slice as ((slice_size, abduce, check_consistent, num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state - val _ = spying spy (fn () => (state, subgoal, name, "Launched")) + val _ = spying spy (fn () => (state, subgoal, name, + "Launched" ^ (if abduce then " (abduce)" else "") ^ + (if check_consistent then " (check_consistent)" else ""))) val _ = if verbose then writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slice_size slices timeout) ^ - "...") + (if abduce then " (abduce)" else "") ^ + (if check_consistent then " (check_consistent)" else "") ^ "...") else () @@ -168,7 +177,8 @@ |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas - |> prefix ("Facts in " ^ name ^ " proof: ") + |> prefix ("Facts in " ^ name ^ " " ^ + (if check_consistent then "inconsistency" else "proof") ^ ": ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = @@ -196,8 +206,8 @@ |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in - "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ - plural_s num_used_facts ^ + "Success: Found " ^ (if check_consistent then "inconsistency" else "proof") ^ " with " ^ + string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) end | spying_str_of_res {outcome = SOME failure, ...} = @@ -233,6 +243,21 @@ (output, output_message) end +fun analyze_prover_result_for_consistency (result as {outcome, used_facts, ...} : prover_result) = + if outcome = SOME ATP_Proof.TimedOut then + (SH_Timeout, K "") + else if is_some outcome then + (SH_None, K "") + else + (SH_Some (result, []), fn () => + (if member (op = o apsnd fst) used_facts sledgehammer_goal_as_fact then + (case map fst (filter_out (equal sledgehammer_goal_as_fact o fst) used_facts) of + [] => "The goal is inconsistent" + | facts => "The goal is inconsistent with these facts: " ^ commas facts) + else + "The following facts are inconsistent: " ^ + commas (map fst used_facts))) + fun check_expected_outcome ctxt prover_name expect outcome = let val outcome_code = short_string_of_sledgehammer_outcome outcome @@ -248,22 +273,48 @@ if exists (fn (_, (Played _, _)) => true | _ => false) preplay_results then () else - error ("Unexpected outcome: the external prover found a some proof but preplay failed") + error ("Unexpected outcome: the external prover found a proof but preplay failed") | ("unknown", SH_Unknown) => () | ("timeout", SH_Timeout) => () | ("none", SH_None) => () | _ => error ("Unexpected outcome: " ^ quote outcome_code)) end -fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn - (problem as {state, subgoal, ...}) slice prover_name = +fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode found_something + writeln_result learn (problem as {state, subgoal, ...}) + (slice as ((_, _, check_consistent, _, _), _)) prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout + fun flip_problem {comment, state, goal, subgoal, factss = factss, ...} = + let + val thy = Proof_Context.theory_of ctxt + val assms = Assumption.all_assms_of ctxt + val assm_ts = map Thm.term_of assms + val subgoal_t = Logic.get_goal (Thm.prop_of goal) subgoal + val polymorphic_subgoal_t = (Logic.list_implies (assm_ts, subgoal_t)) + |> Logic.varify_global + val nonfixeds = + subtract (op =) (fold Term.add_free_names assm_ts []) (Term.add_free_names subgoal_t []) + val monomorphic_subgoal_t = subgoal_t + |> varify_nonfixed_terms_global nonfixeds + val subgoal_thms = map (Skip_Proof.make_thm thy) + [polymorphic_subgoal_t, monomorphic_subgoal_t] + val new_facts = + map (fn thm => (((sledgehammer_goal_as_fact, (Assum, General)), thm))) subgoal_thms + in + {comment = comment, state = state, goal = Thm.trivial @{cprop False}, subgoal = 1, + subgoal_count = 1, factss = map (apsnd (append new_facts)) factss, + found_something = found_something "an inconsistency"} + end + + val problem = problem |> check_consistent ? flip_problem + fun really_go () = launch_prover params mode learn problem slice prover_name - |> preplay_prover_result params state subgoal + |> (if check_consistent then analyze_prover_result_for_consistency else + preplay_prover_result params state subgoal) fun go () = if debug then @@ -330,13 +381,15 @@ end fun prover_slices_of_schedule ctxt factss - ({max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule = + ({abduce, check_consistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, + ...} : params) + schedule = let fun triplicate_slices original = let val shift = - map (apfst (fn (slice_size, num_facts, fact_filter) => - (slice_size, num_facts, + map (apfst (fn (slice_size, abduce, check_consistent, num_facts, fact_filter) => + (slice_size, abduce, check_consistent, num_facts, if fact_filter = mashN then mepoN else if fact_filter = mepoN then meshN else mashN))) @@ -353,14 +406,17 @@ the_default uncurried_aliases0 uncurried_aliases, extra_extra0) | adjust_extra (extra as SMT_Slice _) = extra - fun adjust_slice max_slice_size ((slice_size0, num_facts0, fact_filter0), extra) = + fun adjust_slice max_slice_size + ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) = let val slice_size = Int.min (max_slice_size, slice_size0) + val abduce = abduce |> the_default abduce0 + val check_consistent = check_consistent |> the_default check_consistent0 val fact_filter = fact_filter |> the_default fact_filter0 val max_facts = max_facts |> the_default num_facts0 val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss)) in - ((slice_size, num_facts, fact_filter), adjust_extra extra) + ((slice_size, abduce, check_consistent, num_facts, fact_filter), adjust_extra extra) end val provers = distinct (op =) schedule @@ -378,7 +434,7 @@ SOME (slice0 :: slices) => let val prover_slices' = AList.update (op =) (prover, slices) prover_slices - val slice as ((slice_size, _, _), _) = + val slice as ((slice_size, _, _, _, _), _) = adjust_slice ((slices_left + max_threads - 1) div max_threads) slice0 in (prover, slice) :: translate_schedule prover_slices' (slices_left - slice_size) schedule @@ -389,8 +445,8 @@ |> distinct (op =) end -fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs, - slices, ...}) +fun run_sledgehammer (params as {verbose, spy, provers, check_consistent, induction_rules, + max_facts, max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set" @@ -402,12 +458,13 @@ val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none writeln_result then writeln else K () - val found_proofs = Synchronized.var "found_proofs" 0 + val found_proofs_and_inconsistencies = Synchronized.var "found_proofs_and_inconsistencies" 0 - fun found_proof prover_name = + fun found_something a_proof_or_inconsistency prover_name = if mode = Normal then - (Synchronized.change found_proofs (fn n => n + 1); - (the_default writeln writeln_result) (prover_name ^ " found a proof...")) + (Synchronized.change found_proofs_and_inconsistencies (fn n => n + 1); + (the_default writeln writeln_result) (prover_name ^ " found " ^ + a_proof_or_inconsistency ^ "...")) else () @@ -437,7 +494,8 @@ SOME n => n | NONE => fold (fn prover => - fold (fn ((_, n, _), _) => Integer.max n) (get_slices ctxt prover)) + fold (fn ((_, _, _, max_facts, _), _) => Integer.max max_facts) + (get_slices ctxt prover)) provers 0) * 51 div 50 (* some slack to account for filtering of induction facts below *) @@ -463,9 +521,9 @@ val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = factss, found_proof = found_proof} + factss = factss, found_something = found_something "a proof"} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) - val launch = launch_prover_and_preplay params mode writeln_result learn + val launch = launch_prover_and_preplay params mode found_something writeln_result learn val schedule = if mode = Auto_Try then provers @@ -487,7 +545,7 @@ else (learn chained_thms; Par_List.map (fn (prover, slice) => - if Synchronized.value found_proofs < max_proofs then + if Synchronized.value found_proofs_and_inconsistencies < max_proofs then launch problem slice prover else (SH_None, "")) @@ -499,11 +557,19 @@ handle Timeout.TIMEOUT _ => (SH_Timeout, "")) |> `(fn (outcome, message) => (case outcome of - SH_Some _ => (the_default writeln writeln_result "QED"; true) + SH_Some _ => (the_default writeln writeln_result "Done"; true) | SH_Unknown => (the_default writeln writeln_result message; false) - | SH_Timeout => (the_default writeln writeln_result "No proof found"; false) + | SH_Timeout => + (the_default writeln writeln_result + ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^ + " found"); + false) | SH_None => (the_default writeln writeln_result - (if message = "" then "No proof found" else "Warning: " ^ message); + (if message = "" then + "No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^ + " found" + else + "Warning: " ^ message); false))) end) diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Feb 20 13:59:16 2023 +0100 @@ -11,7 +11,7 @@ type atp_formula_role = ATP_Problem.atp_formula_role type atp_failure = ATP_Proof.atp_failure - type base_slice = int * int * string + type base_slice = int * bool * bool * int * string type atp_slice = atp_format * string * string * bool * string type atp_config = {exec : string list * string list, @@ -67,8 +67,8 @@ val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) -(* desired slice size, desired number of facts, fact filter *) -type base_slice = int * int * string +(* desired slice size, abduce, check_consistent, desired number of facts, fact filter *) +type base_slice = int * bool * bool * int * string (* problem file format, type encoding, lambda translation scheme, uncurried aliases?, prover-specific extra information *) @@ -142,7 +142,7 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((2, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((2, false, false, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -165,7 +165,7 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((1000 (* infinity *), 100, meshN), (TF1, "poly_native", liftingN, false, ""))], + K [((1000 (* infinity *), false, false, 100, meshN), (TF1, "poly_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -200,12 +200,12 @@ (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule") in (* FUDGE *) - K [((1000 (* infinity *), 512, meshN), (format, type_enc, lam_trans, false, extra_options)), - ((1000 (* infinity *), 1024, meshN), (format, type_enc, lam_trans, false, extra_options)), - ((1000 (* infinity *), 128, mepoN), (format, type_enc, lam_trans, false, extra_options)), - ((1000 (* infinity *), 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)), - ((1000 (* infinity *), 256, mepoN), (format, type_enc, liftingN, false, extra_options)), - ((1000 (* infinity *), 64, mashN), (format, type_enc, combsN, false, extra_options))] + K [((1000 (* infinity *), false, false, 512, meshN), (format, type_enc, lam_trans, false, extra_options)), + ((1000 (* infinity *), false, false, 1024, meshN), (format, type_enc, lam_trans, false, extra_options)), + ((1000 (* infinity *), false, false, 128, mepoN), (format, type_enc, lam_trans, false, extra_options)), + ((1000 (* infinity *), false, false, 724, meshN), (TF0, "poly_guards??", lam_trans, false, extra_options)), + ((1000 (* infinity *), false, true, 256, mepoN), (format, type_enc, liftingN, false, extra_options)), + ((1000 (* infinity *), false, false, 64, mashN), (format, type_enc, combsN, false, extra_options))] end, good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -229,11 +229,11 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((2, 32, meshN), (TF0, "mono_native", liftingN, false, "")), - ((2, 512, meshN), (TX0, "mono_native", liftingN, false, "")), - ((2, 128, mashN), (TF0, "mono_native", combsN, false, "")), - ((2, 1024, meshN), (TF0, "mono_native", liftingN, false, "")), - ((2, 256, mepoN), (TF0, "mono_native", combsN, false, ""))], + K [((2, false, false, 32, meshN), (TF0, "mono_native", liftingN, false, "")), + ((2, false, false, 512, meshN), (TX0, "mono_native", liftingN, false, "")), + ((2, false, false, 128, mashN), (TF0, "mono_native", combsN, false, "")), + ((2, false, false, 1024, meshN), (TF0, "mono_native", liftingN, false, "")), + ((2, false, true, 256, mepoN), (TF0, "mono_native", combsN, false, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -259,7 +259,7 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((2, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((2, false, false, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -281,8 +281,8 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((6, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), - ((6, 512, meshN), (TF0, "mono_native", liftingN, false, ""))], + K [((6, false, false, 512, meshN), (TH0, "mono_native_higher", keep_lamsN, false, "")), + ((6, false, false, 512, meshN), (TF0, "mono_native", liftingN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -306,7 +306,7 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((12, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], + K [((12, false, false, 256, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, ""))], good_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), good_max_new_mono_instances = default_max_new_mono_instances} @@ -341,14 +341,14 @@ generate_isabelle_info = true, good_slices = (* FUDGE *) - K [((2, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")), - ((2, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)), - ((2, 50, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2LR0LT0)), - ((2, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)), - ((2, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)), - ((2, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), - ((2, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)), - ((2, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))], + K [((2, false, false, 150, meshN), (DFG Monomorphic, "mono_native", combsN, true, "")), + ((2, false, false, 500, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2SOS)), + ((2, false, false, 50, meshN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H2LR0LT0)), + ((2, false, false, 250, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2NuVS0)), + ((2, false, false, 1000, mepoN), (DFG Monomorphic, "mono_native", liftingN, true, spass_H1SOS)), + ((2, false, true, 150, meshN), (DFG Monomorphic, "poly_guards??", liftingN, false, spass_H2NuVS0Red2)), + ((2, false, false, 300, meshN), (DFG Monomorphic, "mono_native", combsN, true, spass_H2SOS)), + ((2, false, false, 100, meshN), (DFG Monomorphic, "mono_native", combs_and_liftingN, true, spass_H2))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} @@ -387,14 +387,14 @@ generate_isabelle_info = false, good_slices = (* FUDGE *) - K [((2, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), - ((2, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)), - ((2, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), - ((2, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), - ((2, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), - ((2, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)), - ((2, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)), - ((2, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))], + K [((2, false, false, 512, meshN), (TX1, "mono_native_fool", combsN, false, sosN)), + ((2, false, false, 1024, meshN), (TX1, "mono_native_fool", liftingN, false, sosN)), + ((2, false, false, 256, mashN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), + ((2, false, true, 512, mepoN), (TF1, "poly_native", liftingN, false, no_sosN)), + ((2, false, false, 16, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN)), + ((2, false, false, 32, meshN), (TX1, "mono_native_fool", combsN, false, no_sosN)), + ((2, false, false, 64, meshN), (TX1, "mono_native_fool", combs_or_liftingN, false, no_sosN)), + ((2, false, false, 128, meshN), (TX1, "mono_native_fool", liftingN, false, no_sosN))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = 2 * default_max_new_mono_instances (* FUDGE *)} @@ -419,21 +419,21 @@ prem_role = Hypothesis, generate_isabelle_info = true, good_slices = - K [((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), (* sh5_sh1.sh *) - ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), (* sh8_shallow_sine.sh *) - ((1, 256, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")), (* sh10_new_c.s3.sh *) - ((1, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")), (* sh10_c_ic.sh *) - ((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")), (* sh8_b.comb.sh (modified) *) - ((1, 1024, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true --avatar=eager --split-only-ground=true")), (* sh5_add_var_l_av.sh *) - ((1, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")), (* sh10_e_lift.sh *) - ((1, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")), (* sh5_shallow_sine.sh *) - ((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")), (* sh5_e_short1.sh *) - ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")), (* sh5_32.sh *) - ((1, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")), (* sh5_sh4.sh *) - ((1, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")), (* sh5_lifting2.sh *) - ((1, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")), (* sh5_noforms.sh *) - ((1, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")), (* sh8_old_zip1.sh *) - ((1, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))], (* sh5_sh.eqenc.sh *) + K [((1, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=1 --ho-unif-max-depth=1 --ho-max-elims=0 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --boolean-reasoning=bool-hoist --bool-hoist-simpl=true --bool-select=LI --recognize-injectivity=true --ext-rules=ext-family --ext-rules-max-depth=1 --ho-choice-inst=true --ho-prim-enum=none --ho-elim-leibniz=0 --interpret-bool-funs=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --ho-unif-level=pragmatic-framework --select=bb+e-selection2 --post-cnf-lambda-lifting=true -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" -q \"6|prefer-processed|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|fifo\" -q \"4|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-struct(1,5,2,3)\" --avatar=off --recognize-injectivity=true --ho-neg-ext=true --e-timeout=2 --ho-pattern-decider=true --ho-fixpoint-decider=true --e-max-derived=50 --ignore-orphans=true --e-auto=true --presaturate=true --e-call-point=0.1")), (* sh5_sh1.sh *) + ((1, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic -nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=3 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=7 --sine=50 --sine-tolerance=1 --sine-depth-max=2 --sine-depth-min=1 --e-max-derived=64 --sine-ignore-k-most-common-syms=2 --sine-trim-implications=true --e-encode-lambdas=lift --scan-clause-ac=false --lambdasup=0 --kbo-weight-fun=lambda-def-invfreqrank --demod-in-var-args=true --bool-demod=true --lambda-demod=true --e-call-point=0.1")), (* sh10_c_ic.sh *) + ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=none --avatar=off --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars --max-inferences=2 --ho-unif-max-depth=1 -q \"6|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"6|const|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-easy-ho|conjecture-relative-var(1.01,s,f)\" --select=e-selection16 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true --ho-unif-level=pragmatic-framework --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=lambda-def-invfreqrank --e-call-point=0.1")), (* sh8_shallow_sine.sh *) + ((1, false, false, 256, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=simpl-only --ext-rules=off --ho-prim-enum=full --ho-prim-max=1 --avatar=off --recognize-injectivity=true --ho-elim-leibniz=4 --ho-unif-level=full-framework --no-max-vars -q \"2|prefer-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1)\" -q \"4|const|conjecture-relative-e(0.1,1,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.5,1,100,100,100,100,1.5,1.5,1.5)\" -q \"4|prefer-sos|pnrefined(1,1,1,1,2,1.5,2)\" --select=ho-selection5 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=5 --e-call-point=0.25 --e-auto=true --sine=50 --sine-tolerance=2 --sine-depth-max=4 --sine-depth-min=1 --e-max-derived=96 --e-encode-lambdas=lift --scan-clause-ac=false --kbo-weight-fun=arity0 --prec-gen-fun=invfreq_conj")), (* sh10_new_c.s3.sh *) + ((1, false, true, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-comb-complete --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-sqarity --ho-prim-enum=none --tptp-def-as-rewrite -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --select=NoSelection --solve-formulas=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=8 --sine=60 --sine-tolerance=2 --sine-depth-max=5 --sine-depth-min=1 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-auto=true --e-max-derived=50 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --comb-b-penalty=3 --comb-c-penalty=3 --comb-k-penalty=1 --comb-s-penalty=5 --subvarsup=false --e-call-point=0.15")), (* sh8_b.comb.sh (modified) *) + ((1, false, false, 1024, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=0 --ho-prim-enum=none -q \"2|prefer-ho-steps|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|default\" -q \"2|prefer-empty-trail|conjecture-relative-e(0.1,0.5,100,100,100,100,1.5,1.5,1.5)\" -q \"1|prefer-processed|fifo\" --select=bb+e-selection7 --ho-pattern-decider=false --ho-fixpoint-decider=true --ho-solid-decider=false --sine=150 --sine-tolerance=2 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=2 --fluid-log-hoist=false --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-prim-enum=eq --ho-prim-enum-add-var=true --ho-prim-max=1 --ho-prim-enum-early-bird=true --avatar=eager --split-only-ground=true")), (* sh5_add_var_l_av.sh *) + ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=2 --max-inferences=3 --boolean-reasoning=bool-hoist --bool-select=LO --ext-rules=off --kbo-weight-fun=lambda-def-invfreqrank --ho-prim-enum=none --ho-unif-level=pragmatic-framework -q \"1|prefer-sos|conjecture-relative-var(1.01,s,f)\" -q \"4|const|conjecture-relative-var(1.05,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1.02,l,f)\" -q \"4|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection2 --solve-formulas=true --lambdasup=0 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=3 --e-max-derived=48 --e-encode-lambdas=lift --presaturate=true --prec-gen-fun=invfreq --e-call-point=0.2 --e-auto=true --sine-trim-implications=true")), (* sh10_e_lift.sh *) + ((1, false, false, 512, mepoN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --mode=ho-pragmatic --max-inferences=4 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=1 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=simpl-only --ext-rules=off --kbo-weight-fun=lambda-def-const --ho-prim-enum=neg --ho-prim-enum-early-bird=true --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework --ho-unif-max-depth=1 --sine=50 --sine-tolerance=1.0 --sine-depth-max=3 --sine-depth-min=1 --sine-trim-implications=true -q \"4|prefer-sos|orient-lmax(2,1,2,1,1)\" -q \"4|defer-sos|conjecture-relative-var(1,s,f)\" -q \"3|const|default\" -q \"1|prefer-processed|fifo\" --ho-elim-leibniz=1 --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=false --select=e-selection10 --solve-formulas=true --sup-at-vars=false --sup-at-var-headed=false --sup-from-var-headed=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=4 --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-max-derived=32 --e-encode-lambdas=lift --scan-clause-ac=false --presaturate=true --e-call-point=0.16")), (* sh5_shallow_sine.sh *) + ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --mode=ho-competitive --boolean-reasoning=bool-hoist --ext-rules=off --recognize-injectivity=true --ho-unif-level=full-framework -q \"4|prefer-goals|pnrefined(1,1,1,2,2,2,0.5)\" -q \"1|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-ho-steps|conjecture-relative-var(1.01,s,f)\" -q \"1|prefer-processed|fifo\" --select=bb+ho-selection --scan-clause-ac=false --kbo-weight-fun=invfreqrank --fluidsup=true --boolean-reasoning=bool-hoist --fluid-log-hoist=true --fluid-hoist=true --ite-axioms=true --lazy-cnf=true --ho-solid-decider=true --ho-fixpoint-decider=true --bool-select=\"sel1(pos_ctx)\" --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --e-call-point=0.35 --avatar=off --e-max-derived=50")), (* sh5_e_short1.sh *) + ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --boolean-reasoning=simpl-only --select=e-selection12 --prec-gen-fun=invfreq_conj --ord=lambda_kbo --ho-unif-level=full-framework --ho-pattern-decider=true --ho-solid-decider=false --ho-fixpoint-decider=true --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=1 --sine=100 --sine-depth-min=1 --sine-depth-max=5 --sine-tolerance=1.5 -q \"1|prefer-sos|default\" -q \"8|prefer-processed|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --kbo-weight-fun=arity0")), (* sh5_32.sh *) + ((1, false, false, 256, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --ho-unif-max-depth=2 --ho-max-app-projections=0 --ho-max-rigid-imitations=1 --ho-max-elims=0 --ho-max-identifications=1 --max-inferences=3 --ext-rules=off --recognize-injectivity=true --ho-prim-enum=none --ho-choice-inst=true -q \"3|prefer-fo|conjecture-relative-var(1.02,l,f)\" -q \"3|prefer-sos|pnrefined(1,1,1,2,2,2,0.5)\" -q \"2|prefer-ground|orient-lmax(2,1,2,1,1)\" -q \"1|prefer-processed|fifo\" --select=MaxGoalNS --sine=60 --sine-tolerance=1.5 --sine-depth-max=3 --sine-depth-min=1 --prec-gen-fun=invfreqhack --lazy-cnf=true --lazy-cnf-kind=simp --lazy-cnf-renaming-threshold=3 --kbo-weight-fun-from-precedence=true --kbo-weight-fun-from-precedence-rank=5 --trigger-bool-inst=1 --avatar=lazy --tptp-def-as-rewrite --rewrite-before-cnf=true --sup-from-var-headed=false --sup-at-vars=false")), (* sh5_sh4.sh *) + ((1, false, false, 512, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--tptp-def-as-rewrite --rewrite-before-cnf=true --mode=lambda-free-intensional --check-lambda-free=false --boolean-reasoning=simpl-only --post-cnf-lambda-lifting=true --ext-rules=off --ho-prim-enum=none --recognize-injectivity=true --no-max-vars --select=e-selection8 --prec-gen-fun=invfreq --kbo-weight-fun=invfreqrank --kbo-const-weight=2 --ord=lambdafree_kbo --ignore-orphans=true -q \"1|prefer-sos|conjecture-relative-struct(1.5,3.5,2,3)\" -q \"1|const|conj_pref_weight(0.5,100,0.2,0.2,4)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-e(0.3,0.25,100,100,100,100,1.5,1.5,1)\" -q \"1|prefer-sos|pnrefined(3,2,3,2,2,1.5,2)\" --lazy-cnf=true --lazy-cnf-renaming-threshold=2")), (* sh5_lifting2.sh *) + ((1, false, false, 512, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "-nc --tptp-def-as-rewrite --rewrite-before-cnf=true --tptp-rewrite-formulas-only=true --mode=ho-pragmatic --boolean-reasoning=simpl-only --ext-rules=ext-family --ext-rules-max-depth=1 --ho-prim-enum=neg --ho-prim-max=1 --recognize-injectivity=true --ho-elim-leibniz=1 --ho-unif-level=pragmatic-framework --no-max-vars -q \"1|prefer-sos|conjecture-relative-var(1.02,l,f)\" -q \"4|const|conjecture-relative-var(1,s,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-non-goals|conjecture-relative-var(1,l,f)\" -q \"4|prefer-sos|pnrefined(2,1,1,1,2,2,2)\" --select=e-selection7 --ho-choice-inst=true --try-e=\"$E_HOME/eprover\" --tmp-dir=\"$ISABELLE_TMP_PREFIX\" --e-timeout=2 --e-auto=true --sine=50 --sine-tolerance=10 --sine-depth-max=5 --sine-depth-min=1 --e-max-derived=64 --e-encode-lambdas=lift --scan-clause-ac=false --prec-gen-fun=invfreq_conj --ord=lambda_kbo --solid-subsumption=true --ignore-orphans=true --e-call-point=0.2")), (* sh5_noforms.sh *) + ((1, false, false, 1024, meshN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --tptp-def-as-rewrite --rewrite-before-cnf=true --max-inferences=4 --ho-unif-max-depth=3 --ho-max-elims=0 --ho-max-app-projections=1 --ho-max-identifications=0 --ho-max-rigid-imitations=2 --ho-unif-level=pragmatic-framework --boolean-reasoning=simpl-only --kbo-weight-fun=freqrank --ext-rules=ext-family --ext-rules-max-depth=2 --ho-prim-enum=eq --ho-prim-max=2 --interpret-bool-funs=false -q \"2|prefer-goals|default\" -q \"8|prefer-sos|conjecture-relative-var(1,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|prefer-lambdas|explore\" -q \"1|prefer-non-goals|explore\" -q \"1|prefer-processed|conjecture-relative-var(1,s,f)\" --recognize-injectivity=true --ho-selection-restriction=none --select=ho-selection2 --solve-formulas=true")), (* sh8_old_zip1.sh *) + ((1, false, false, 256, mashN), (format, "mono_native_higher_fool", keep_lamsN, false, "--mode=ho-pragmatic --boolean-reasoning=simpl-only --tptp-def-as-rewrite --rewrite-before-cnf=true --kbo-weight-fun=freqrank -q \"1|prefer-sos|default\" -q \"1|prefer-goals|conjecture-relative-var(1.03,s,f)\" -q \"1|prefer-non-goals|default\" -q \"5|const|conjecture-relative-var(1.01,l,f)\" -q \"1|prefer-processed|fifo\" -q \"1|const|conjecture-relative-var(1.05,l,f)\" -q \"1|defer-sos|conjecture-relative-var(1.1,s,f)\" --select=e-selection9 --recognize-injectivity=true --ho-choice-inst=false --ho-selection-restriction=none --sine=50 --sine-tolerance=3 --sine-depth-max=3 --sine-depth-min=1 --eq-encode=true --avatar=eager --sine-trim-implications=true"))], (* sh5_sh.eqenc.sh *) good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} end @@ -515,30 +515,30 @@ (Crashed, "Unrecoverable Segmentation Fault")] @ known_szs_status_failures) Hypothesis false - (K ((1000 (* infinity *), 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 50, meshN), (CNF_UEQ, type_enc, combsN, false, "")) (* FUDGE *)) val remote_agsyhol = remotify_atp agsyhol "agsyHOL" ["1.0", "1"] - (K ((1000 (* infinity *), 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 60, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) val remote_alt_ergo = remotify_atp alt_ergo "Alt-Ergo" ["0.95.2"] - (K ((1000 (* infinity *), 250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 250, meshN), (TF1, "poly_native", keep_lamsN, false, "")) (* FUDGE *)) val remote_e = remotify_atp e "E" ["2.0", "1.9.1", "1.8"] - (K ((1000 (* infinity *), 750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 750, meshN), (TF0, "mono_native", combsN, false, "")) (* FUDGE *)) val remote_iprover = remotify_atp iprover "iProver" ["0.99"] - (K ((1000 (* infinity *), 150, meshN), (FOF, "mono_guards??", liftingN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 150, meshN), (FOF, "mono_guards??", liftingN, false, "")) (* FUDGE *)) val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] - (K ((1000 (* infinity *), 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 40, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", liftingN, false, "")) (* FUDGE *)) val remote_leo3 = remotify_atp leo3 "Leo-III" ["1.1"] - (K ((1000 (* infinity *), 150, meshN), (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 150, meshN), (THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "poly_native_higher", keep_lamsN, false, "")) (* FUDGE *)) val remote_waldmeister = gen_remote_waldmeister waldmeisterN "raw_mono_tags??" val remote_zipperposition = remotify_atp zipperposition "Zipperpin" ["2.1", "2.0"] - (K ((1000 (* infinity *), 512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) + (K ((1000 (* infinity *), false, false, 512, meshN), (THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, false, "")) (* FUDGE *)) (* Dummy prover *) @@ -551,7 +551,7 @@ prem_role = prem_role, generate_isabelle_info = false, good_slices = - K [((2, 256, "mepo"), (format, type_enc, + K [((2, false, false, 256, "mepo"), (format, type_enc, if is_format_higher_order format then keep_lamsN else combsN, uncurried_aliases, ""))], good_max_mono_iters = default_max_mono_iters, good_max_new_mono_instances = default_max_new_mono_instances} diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 20 13:59:16 2023 +0100 @@ -53,6 +53,8 @@ ("verbose", "false"), ("overlord", "false"), ("spy", "false"), + ("abduce", "smart"), + ("check_consistent", "smart"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), @@ -84,6 +86,8 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), + ("dont_abduce", "abduce"), + ("dont_check_consistent", "check_consistent"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), @@ -228,6 +232,16 @@ val overlord = lookup_bool "overlord" val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd + val check_consistent = + if mode = Auto_Try then + SOME false + else + lookup_option lookup_bool "check_consistent" + val abduce = + if mode = Auto_Try then + SOME false + else + lookup_option lookup_bool "abduce" val type_enc = if mode = Auto_Try then NONE @@ -261,13 +275,14 @@ val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, - type_enc = type_enc, strict = strict, lam_trans = lam_trans, - uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, - induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds, - max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, - max_proofs = max_proofs, isar_proofs = isar_proofs, compress = compress, try0 = try0, - smt_proofs = smt_proofs, minimize = minimize, slices = slices, timeout = timeout, - preplay_timeout = preplay_timeout, expect = expect} + abduce = abduce, check_consistent = check_consistent, type_enc = type_enc, strict = strict, + lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = learn, + fact_filter = fact_filter, induction_rules = induction_rules, max_facts = max_facts, + fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, + max_new_mono_instances = max_new_mono_instances, max_proofs = max_proofs, + isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, + minimize = minimize, slices = slices, timeout = timeout, preplay_timeout = preplay_timeout, + expect = expect} end fun get_params mode = extract_params mode o default_raw_params diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Feb 20 13:59:16 2023 +0100 @@ -18,6 +18,7 @@ del : (Facts.ref * Token.src list) list, only : bool} + val sledgehammer_goal_as_fact : string val no_fact_override : fact_override val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table -> @@ -64,6 +65,8 @@ val max_facts_for_complex_check = 25000 val max_simps_for_clasimpset = 10000 +val sledgehammer_goal_as_fact = "Sledgehammer.goal_as_fact" + val no_fact_override = {add = [], del = [], only = false} fun needs_quoting keywords s = diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Feb 20 13:59:16 2023 +0100 @@ -868,7 +868,7 @@ let val problem = {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, - subgoal_count = 1, factss = [("", facts)], found_proof = K ()} + subgoal_count = 1, factss = [("", facts)], found_something = K ()} val slice = hd (get_slices ctxt prover) in get_minimizing_prover ctxt MaSh (K ()) prover params problem slice diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 20 13:59:16 2023 +0100 @@ -29,6 +29,8 @@ overlord : bool, spy : bool, provers : string list, + abduce : bool option, + check_consistent : bool option, type_enc : string option, strict : bool, lam_trans : string option, @@ -61,7 +63,7 @@ subgoal : int, subgoal_count : int, factss : (string * fact list) list, - found_proof : string -> unit} + found_something : string -> unit} datatype prover_slice_extra = ATP_Slice of atp_slice @@ -134,6 +136,8 @@ overlord : bool, spy : bool, provers : string list, + abduce : bool option, + check_consistent : bool option, type_enc : string option, strict : bool, lam_trans : string option, @@ -160,8 +164,8 @@ YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100))) fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list = - induction_rules = Exclude ? - filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false) + induction_rules = Exclude ? + filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false) fun slice_timeout slice_size slices timeout = let @@ -178,7 +182,7 @@ subgoal : int, subgoal_count : int, factss : (string * fact list) list, - found_proof : string -> unit} + found_something : string -> unit} datatype prover_slice_extra = ATP_Slice of atp_slice @@ -234,9 +238,14 @@ SOME facts => facts | NONE => snd (hd factss)) -fun facts_of_basic_slice (_, num_facts, fact_filter) factss = - facts_of_filter fact_filter factss - |> take num_facts +fun facts_of_basic_slice (_, _, _, num_facts, fact_filter) factss = + let + val facts = facts_of_filter fact_filter factss + val (goal_facts, nongoal_facts) = + List.partition (equal sledgehammer_goal_as_fact o fst o fst) facts + in + goal_facts @ take num_facts nongoal_facts + end fun is_fact_chained ((_, (sc, _)), _) = sc = Chained diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 20 13:59:16 2023 +0100 @@ -104,10 +104,10 @@ fun run_atp mode name ({debug, verbose, overlord, strict, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params) - ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) + ({comment, state, goal, subgoal, subgoal_count, factss, found_something} : prover_problem) slice = let - val (basic_slice as (slice_size, _, _), + val (basic_slice as (slice_size, _, _, _, _), ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = slice val facts = facts_of_basic_slice basic_slice factss @@ -237,18 +237,10 @@ (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) - val outcome = + val _ = (case outcome of - NONE => - (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of - SOME facts => - let - val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) - in - if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure - end - | NONE => (found_proof name; NONE)) - | _ => outcome) + NONE => found_something name + | _ => ()) in (atp_problem_data, (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, outcome), diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Feb 20 13:59:16 2023 +0100 @@ -83,7 +83,8 @@ fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, induction_rules, ...} : params) - slice silent (prover : prover) timeout i n state goal facts = + (slice as ((_, abduce, check_consistent, _, _), _)) silent (prover : prover) timeout i n state + goal facts = let val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") @@ -91,9 +92,9 @@ val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, - type_enc = type_enc, strict = strict, lam_trans = lam_trans, - uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, - induction_rules = induction_rules, max_facts = SOME (length facts), + type_enc = type_enc, abduce = SOME abduce, check_consistent = SOME check_consistent, + strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, + fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, max_proofs = 1, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, @@ -101,7 +102,7 @@ expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)], found_proof = K ()} + factss = [("", facts)], found_something = K ()} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = prover params problem slice @@ -117,7 +118,7 @@ (case outcome of SOME failure => string_of_atp_failure failure | NONE => - "Found proof" ^ + "Found " ^ (if check_consistent then "inconsistency" else "proof") ^ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ " (" ^ string_of_time run_time ^ ")")); result diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 20 13:59:16 2023 +0100 @@ -120,10 +120,10 @@ fun run_smt_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, ...}) - ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) + ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice = let - val (basic_slice as (slice_size, _, _), SMT_Slice options) = slice + val (basic_slice as (slice_size, _, _, _, _), SMT_Slice options) = slice val facts = facts_of_basic_slice basic_slice factss val ctxt = Proof.context_of state @@ -139,7 +139,7 @@ (case outcome of NONE => let - val _ = found_proof name; + val _ = found_something name; val preferred = if smt_proofs then SMT_Method (if name = "z3" then SMT_Z3 else SMT_Verit "default") diff -r f02c8a45c4c1 -r fa247805669d src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Feb 20 13:55:58 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Mon Feb 20 13:59:16 2023 +0100 @@ -33,7 +33,7 @@ val params as {provers, induction_rules, max_facts, ...} = default_params thy override_params val name = hd provers val prover = get_prover ctxt mode name - val default_max_facts = #2 (fst (hd (get_slices ctxt name))) + val default_max_facts = #4 (fst (hd (get_slices ctxt name))) val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt val keywords = Thy_Header.get_keywords' ctxt val css_table = clasimpset_rule_table_of ctxt @@ -45,7 +45,7 @@ |> hd |> snd val problem = {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, - factss = [("", facts)], found_proof = K ()} + factss = [("", facts)], found_something = K ()} val slice = hd (get_slices ctxt name) in (case prover params problem slice of