# HG changeset patch # User blanchet # Date 1677654051 -3600 # Node ID 779faa014564458c7a334a9686e7336c679efb5f # Parent e10f15652026a7a2b7058a312e6be6e92ff1b6fd renamed new Sledgehammer option diff -r e10f15652026 -r 779faa014564 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Mar 01 08:00:51 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Mar 01 08:00:51 2023 +0100 @@ -159,20 +159,20 @@ fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) - (slice as ((slice_size, abduce, check_consistent, num_facts, fact_filter), _)) name = + (slice as ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched" ^ (if abduce then " (abduce)" else "") ^ - (if check_consistent then " (check_consistent)" else ""))) + (if check_inconsistent then " (check_inconsistent)" 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 "") ^ "...") + (if check_inconsistent then " (check_inconsistent)" else "") ^ "...") else () @@ -183,7 +183,7 @@ |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas |> prefix ("Facts in " ^ name ^ " " ^ - (if check_consistent then "inconsistency" else "proof") ^ ": ") + (if check_inconsistent then "inconsistency" else "proof") ^ ": ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = @@ -211,7 +211,7 @@ |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in - "Success: Found " ^ (if check_consistent then "inconsistency" else "proof") ^ " with " ^ + "Success: Found " ^ (if check_inconsistent 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 @@ -250,7 +250,7 @@ (output, output_message) end -fun analyze_prover_result_for_consistency (result as {outcome, used_facts, ...} : prover_result) = +fun analyze_prover_result_for_inconsistency (result as {outcome, used_facts, ...} : prover_result) = if outcome = SOME ATP_Proof.TimedOut then (SH_TimeOut, K "") else if outcome = SOME ATP_Proof.OutOfResources then @@ -292,7 +292,8 @@ fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode has_already_found_something found_something writeln_result learn - (problem as {state, subgoal, ...}) (slice as ((_, _, check_consistent, _, _), _)) prover_name = + (problem as {state, subgoal, ...}) (slice as ((_, _, check_inconsistent, _, _), _)) + prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout @@ -320,11 +321,11 @@ found_something = found_something "an inconsistency"} end - val problem as {goal, ...} = problem |> check_consistent ? flip_problem + val problem as {goal, ...} = problem |> check_inconsistent ? flip_problem fun really_go () = launch_prover params mode learn problem slice prover_name - |> (if check_consistent then analyze_prover_result_for_consistency else + |> (if check_inconsistent then analyze_prover_result_for_inconsistency else preplay_prover_result params state goal subgoal) fun go () = @@ -366,7 +367,7 @@ val default_slice_schedule = (* FUDGE (loosely inspired by Seventeen evaluation) *) [cvc4N, zipperpositionN, vampireN, veritN, spassN, zipperpositionN, eN, cvc4N, zipperpositionN, - cvc4N, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, eN, cvc4N, iproverN, zipperpositionN, + cvc4N, eN, zipperpositionN, vampireN, cvc4N, cvc4N, vampireN, cvc4N, iproverN, zipperpositionN, spassN, vampireN, zipperpositionN, vampireN, zipperpositionN, z3N, zipperpositionN, vampireN, iproverN, spassN, zipperpositionN, vampireN, cvc4N, zipperpositionN, z3N, z3N, cvc4N, zipperpositionN] @@ -391,15 +392,15 @@ end fun prover_slices_of_schedule ctxt goal subgoal factss - ({abduce, check_consistent, max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, + ({abduce, check_inconsistent, 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, abduce, check_consistent, num_facts, fact_filter) => - (slice_size, abduce, check_consistent, num_facts, + map (apfst (fn (slice_size, abduce, check_inconsistent, num_facts, fact_filter) => + (slice_size, abduce, check_inconsistent, num_facts, if fact_filter = mashN then mepoN else if fact_filter = mepoN then meshN else mashN))) @@ -417,7 +418,7 @@ | adjust_extra (extra as SMT_Slice _) = extra fun adjust_slice max_slice_size - ((slice_size0, abduce0, check_consistent0, num_facts0, fact_filter0), extra) = + ((slice_size0, abduce0, check_inconsistent0, num_facts0, fact_filter0), extra) = let val slice_size = Int.min (max_slice_size, slice_size0) val goal_not_False = not (Logic.get_goal (Thm.prop_of goal) subgoal aconv @{prop False}) @@ -425,15 +426,15 @@ (case abduce of NONE => abduce0 andalso goal_not_False | SOME max_candidates => max_candidates > 0) - val check_consistent = - (case check_consistent of - NONE => check_consistent0 andalso goal_not_False - | SOME check_consistent => check_consistent) + val check_inconsistent = + (case check_inconsistent of + NONE => check_inconsistent0 andalso goal_not_False + | SOME check_inconsistent => check_inconsistent) 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, abduce, check_consistent, num_facts, fact_filter), adjust_extra extra) + ((slice_size, abduce, check_inconsistent, num_facts, fact_filter), adjust_extra extra) end val provers = distinct (op =) schedule @@ -462,7 +463,7 @@ |> distinct (op =) end -fun run_sledgehammer (params as {verbose, spy, provers, check_consistent, induction_rules, +fun run_sledgehammer (params as {verbose, spy, provers, check_inconsistent, induction_rules, max_facts, max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then @@ -580,7 +581,7 @@ fun normal_failure () = (the_default writeln writeln_result - ("No " ^ (if check_consistent = SOME true then "inconsistency" else "proof") ^ + ("No " ^ (if check_inconsistent = SOME true then "inconsistency" else "proof") ^ " found"); false) in diff -r e10f15652026 -r 779faa014564 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Mar 01 08:00:51 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Mar 01 08:00:51 2023 +0100 @@ -67,7 +67,7 @@ val default_max_mono_iters = 3 (* FUDGE *) val default_max_new_mono_instances = 100 (* FUDGE *) -(* desired slice size, abduce, check_consistent, desired number of facts, fact filter *) +(* desired slice size, abduce, check_inconsistent, desired number of facts, fact filter *) type base_slice = int * bool * bool * int * string (* problem file format, type encoding, lambda translation scheme, uncurried aliases?, diff -r e10f15652026 -r 779faa014564 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Mar 01 08:00:51 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Mar 01 08:00:51 2023 +0100 @@ -54,7 +54,7 @@ ("overlord", "false"), ("spy", "false"), ("abduce", "smart"), - ("check_consistent", "smart"), + ("check_inconsistent", "smart"), ("type_enc", "smart"), ("strict", "false"), ("lam_trans", "smart"), @@ -87,7 +87,7 @@ ("quiet", "verbose"), ("no_overlord", "overlord"), ("dont_spy", "spy"), - ("dont_check_consistent", "check_consistent"), + ("dont_check_inconsistent", "check_inconsistent"), ("non_strict", "strict"), ("no_uncurried_aliases", "uncurried_aliases"), ("dont_learn", "learn"), @@ -235,9 +235,9 @@ val abduce = if mode = Auto_Try then SOME 0 else lookup_option lookup_int "abduce" - val check_consistent = + val check_inconsistent = if mode = Auto_Try then SOME false - else lookup_option lookup_bool "check_consistent" + else lookup_option lookup_bool "check_inconsistent" val type_enc = if mode = Auto_Try then NONE @@ -271,7 +271,7 @@ val expect = lookup_string "expect" in {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, - abduce = abduce, check_consistent = check_consistent, type_enc = type_enc, strict = strict, + abduce = abduce, check_inconsistent = check_inconsistent, 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, diff -r e10f15652026 -r 779faa014564 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Mar 01 08:00:51 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Wed Mar 01 08:00:51 2023 +0100 @@ -30,7 +30,7 @@ spy : bool, provers : string list, abduce : int option, - check_consistent : bool option, + check_inconsistent : bool option, type_enc : string option, strict : bool, lam_trans : string option, @@ -141,7 +141,7 @@ spy : bool, provers : string list, abduce : int option, - check_consistent : bool option, + check_inconsistent : bool option, type_enc : string option, strict : bool, lam_trans : string option, diff -r e10f15652026 -r 779faa014564 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Mar 01 08:00:51 2023 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Wed Mar 01 08:00:51 2023 +0100 @@ -83,7 +83,7 @@ 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 as ((_, _, check_consistent, _, fact_filter), slice_extra)) silent + (slice as ((_, _, check_inconsistent, _, fact_filter), slice_extra)) silent (prover : prover) timeout i n state goal facts = let val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ @@ -92,7 +92,7 @@ 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, abduce = SOME 0, check_consistent = SOME false, strict = strict, + type_enc = type_enc, abduce = SOME 0, check_inconsistent = SOME false, 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, @@ -118,7 +118,7 @@ (case outcome of SOME failure => string_of_atp_failure failure | NONE => - "Found " ^ (if check_consistent then "inconsistency" else "proof") ^ + "Found " ^ (if check_inconsistent then "inconsistency" else "proof") ^ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ " (" ^ string_of_time run_time ^ ")")); result