# HG changeset patch # User blanchet # Date 1292867293 -3600 # Node ID 33e1077885958c4dbf735b0745be39d0726ba822 # Parent 054a4e5ac5fb1ab4321de312bc6571571b3bd82e# Parent adcb92c0513b65021d7fb435091e13207512bfb2 merged diff -r 054a4e5ac5fb -r 33e107788595 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon Dec 20 17:31:58 2010 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Dec 20 18:48:13 2010 +0100 @@ -12,7 +12,7 @@ type atp_config = {exec: string * string, required_execs: (string * string) list, - arguments: bool -> Time.time -> string, + arguments: bool -> Time.time -> (unit -> (string * real) list) -> string, has_incomplete_mode: bool, proof_delims: (string * string) list, known_failures: (failure * string) list, @@ -20,6 +20,11 @@ explicit_forall: bool, use_conjecture_for_hypotheses: bool} + (* for experimentation purposes -- do not use in production code *) + val e_generate_weights : bool Unsynchronized.ref + val e_weight_factor : real Unsynchronized.ref + val e_default_weight : real Unsynchronized.ref + val eN : string val spassN : string val vampireN : string @@ -44,7 +49,7 @@ type atp_config = {exec: string * string, required_execs: (string * string) list, - arguments: bool -> Time.time -> string, + arguments: bool -> Time.time -> (unit -> (string * real) list) -> string, has_incomplete_mode: bool, proof_delims: (string * string) list, known_failures: (failure * string) list, @@ -94,12 +99,35 @@ val tstp_proof_delims = ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") +val e_generate_weights = Unsynchronized.ref false +val e_weight_factor = Unsynchronized.ref 60.0 +val e_default_weight = Unsynchronized.ref 0.5 + +fun e_weights weights = + if !e_generate_weights then + "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ + \--destructive-er-aggressive --destructive-er --presat-simplify \ + \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ + \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ + \-H'(4*FunWeight(SimulateSOS, " ^ + string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^ + ",20,1.5,1.5,1" ^ + (weights () + |> map (fn (s, w) => "," ^ s ^ ":" ^ + string_of_int (Real.ceil (w * !e_weight_factor))) + |> implode) ^ + "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ + \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ + \FIFOWeight(PreferProcessed))'" + else + "-xAutoDev" + val e_config : atp_config = {exec = ("E_HOME", "eproof"), required_execs = [], - arguments = fn _ => fn timeout => - "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \ - \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), + arguments = fn _ => fn timeout => fn weights => + "--tstp-in --tstp-out -l5 " ^ e_weights weights ^ " -tAutoDev \ + \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), has_incomplete_mode = false, proof_delims = [tstp_proof_delims], known_failures = @@ -125,7 +153,7 @@ val spass_config : atp_config = {exec = ("ISABELLE_ATP", "scripts/spass"), required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")], - arguments = fn complete => fn timeout => + arguments = fn complete => fn timeout => fn _ => ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout)) |> not complete ? prefix "-SOS=1 ", @@ -152,7 +180,7 @@ val vampire_config : atp_config = {exec = ("VAMPIRE_HOME", "vampire"), required_execs = [], - arguments = fn complete => fn timeout => + arguments = fn complete => fn timeout => fn _ => (* This would work too but it's less tested: "--proof tptp " ^ *) "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^ " --thanks \"Andrei and Krystof\" --input_file" @@ -214,7 +242,7 @@ : atp_config = {exec = ("ISABELLE_ATP", "scripts/remote_atp"), required_execs = [], - arguments = fn _ => fn timeout => + arguments = fn _ => fn timeout => fn _ => " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout))) ^ " -s " ^ the_system system_name system_versions, has_incomplete_mode = false, diff -r 054a4e5ac5fb -r 33e107788595 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Dec 20 17:31:58 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Dec 20 18:48:13 2010 +0100 @@ -29,6 +29,7 @@ Proof.context -> bool -> bool -> type_system -> bool -> term list -> term -> (translated_formula option * ((string * 'a) * thm)) list -> string problem * string Symtab.table * int * (string * 'a) list vector + val atp_problem_weights : string problem -> (string * real) list end; structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE = @@ -253,13 +254,15 @@ (** Helper facts **) +fun fold_formula f (AQuant (_, _, phi)) = fold_formula f phi + | fold_formula f (AConn (_, phis)) = fold (fold_formula f) phis + | fold_formula f (AAtom tm) = f tm + fun count_term (ATerm ((s, _), tms)) = (if is_atp_variable s then I else Symtab.map_entry s (Integer.add 1)) #> fold count_term tms -fun count_formula (AQuant (_, _, phi)) = count_formula phi - | count_formula (AConn (_, phis)) = fold count_formula phis - | count_formula (AAtom tm) = count_term tm +val count_formula = fold_formula count_term val init_counters = metis_helpers |> map fst |> sort_distinct string_ord |> map (rpair 0) @@ -316,14 +319,13 @@ val supers = tvar_classes_of_terms fact_ts val tycons = type_consts_of_terms thy (goal_t :: fact_ts) (* TFrees in the conjecture; TVars in the facts *) - val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t]) + val conjs = make_conjecture ctxt (hyp_ts @ [concl_t]) val (supers', arity_clauses) = if type_sys = No_Types then ([], []) else make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in - (fact_names |> map single, - (conjectures, facts, class_rel_clauses, arity_clauses)) + (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses)) end fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) @@ -473,9 +475,9 @@ fun problem_line_for_free_type j lit = Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit) -fun problem_lines_for_free_types type_sys conjectures = +fun problem_lines_for_free_types type_sys conjs = let - val litss = map (free_type_literals_for_conjecture type_sys) conjectures + val litss = map (free_type_literals_for_conjecture type_sys) conjs val lits = fold (union (op =)) litss [] in map2 problem_line_for_free_type (0 upto length lits - 1) lits end @@ -602,7 +604,7 @@ val aritiesN = "Arity declarations" val helpersN = "Helper facts" val conjsN = "Conjectures" -val tfreesN = "Type variables" +val free_typesN = "Type variables" fun offset_of_heading_in_problem _ [] j = j | offset_of_heading_in_problem needle ((heading, lines) :: problem) j = @@ -613,7 +615,7 @@ explicit_apply hyp_ts concl_t facts = let val thy = ProofContext.theory_of ctxt - val (fact_names, (conjectures, facts, class_rel_clauses, arity_clauses)) = + val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt type_sys hyp_ts concl_t facts (* Reordering these might or might not confuse the proof reconstruction code or the SPASS Flotter hack. *) @@ -622,8 +624,8 @@ (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), (aritiesN, map problem_line_for_arity_clause arity_clauses), (helpersN, []), - (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjectures), - (tfreesN, problem_lines_for_free_types type_sys conjectures)] + (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), + (free_typesN, problem_lines_for_free_types type_sys conjs)] val const_tab = const_table_for_problem explicit_apply problem val problem = problem |> repair_problem thy explicit_forall type_sys const_tab @@ -643,4 +645,42 @@ fact_names |> Vector.fromList) end +(* FUDGE *) +val conj_weight = 0.0 +val hyp_weight = 0.05 +val fact_min_weight = 0.1 +val fact_max_weight = 1.0 + +fun add_term_weights weight (ATerm (s, tms)) = + (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight) + #> fold (add_term_weights weight) tms +val add_formula_weights = fold_formula o add_term_weights +fun add_problem_line_weights weight (Fof (_, _, phi)) = + add_formula_weights weight phi + +fun add_conjectures_weights [] = I + | add_conjectures_weights conjs = + let val (hyps, conj) = split_last conjs in + add_problem_line_weights conj_weight conj + #> fold (add_problem_line_weights hyp_weight) hyps + end + +fun add_facts_weights facts = + let + val num_facts = length facts + fun weight_of j = + fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j + / Real.fromInt num_facts + in + map weight_of (0 upto num_facts - 1) ~~ facts + |> fold (uncurry add_problem_line_weights) + end + +(* Weights are from 0.0 (most important) to 1.0 (least important). *) +fun atp_problem_weights problem = + Symtab.empty + |> add_conjectures_weights (these (AList.lookup (op =) problem conjsN)) + |> add_facts_weights (these (AList.lookup (op =) problem factsN)) + |> Symtab.dest + end; diff -r 054a4e5ac5fb -r 33e107788595 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 20 17:31:58 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 20 18:48:13 2010 +0100 @@ -53,6 +53,8 @@ type prover = params -> minimize_command -> prover_problem -> prover_result (* for experimentation purposes -- do not use in production code *) + val atp_run_twice_threshold : int Unsynchronized.ref + val atp_first_iter_time_frac : real Unsynchronized.ref val smt_weights : bool Unsynchronized.ref val smt_weight_min_facts : int Unsynchronized.ref val smt_min_weight : int Unsynchronized.ref @@ -318,15 +320,17 @@ | smt_weighted_fact thy num_facts (fact, j) = (untranslated_fact fact, j) |> weight_smt_fact thy num_facts +fun overlord_file_location_for_prover prover = + (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) + + (* generic TPTP-based ATPs *) fun int_opt_add (SOME m) (SOME n) = SOME (m + n) | int_opt_add _ _ = NONE -fun overlord_file_location_for_prover prover = - (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) - -val atp_first_iter_time_frac = 0.67 +val atp_run_twice_threshold = Unsynchronized.ref 50 +val atp_first_iter_time_frac = Unsynchronized.ref 0.67 (* Important messages are important but not so important that users want to see them each time. *) @@ -358,15 +362,6 @@ error ("No such directory: " ^ quote dest_dir ^ ".") val measure_run_time = verbose orelse Config.get ctxt measure_run_time val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec) - (* write out problem file and call ATP *) - fun command_line complete timeout probfile = - let - val core = File.shell_path command ^ " " ^ arguments complete timeout ^ - " " ^ File.shell_path probfile - in - (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" - else "exec " ^ core) ^ " 2>&1" - end fun split_time s = let val split = String.tokens (fn c => str c = "\n"); @@ -378,16 +373,35 @@ val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); val as_time = Scan.read Symbol.stopper time o raw_explode in (output, as_time t) end; - fun run_on probfile = + fun run_on prob_file = case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of (home_var, _) :: _ => error ("The environment variable " ^ quote home_var ^ " is not set.") | [] => if File.exists command then let + val readable_names = debug andalso overlord + val (atp_problem, pool, conjecture_offset, fact_names) = + prepare_atp_problem ctxt readable_names explicit_forall type_sys + explicit_apply hyp_ts concl_t facts + val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses + atp_problem + val _ = File.write_list prob_file ss + val conjecture_shape = + conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 + |> map single fun run complete timeout = let - val command = command_line complete timeout probfile + fun weights () = atp_problem_weights atp_problem + val core = + File.shell_path command ^ " " ^ + arguments complete timeout weights ^ " " ^ + File.shell_path prob_file + val command = + (if measure_run_time then + "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }" + else + "exec " ^ core) ^ " 2>&1" val ((output, msecs), res_code) = bash_output command |>> (if overlord then @@ -399,22 +413,14 @@ extract_tstplike_proof_and_outcome verbose complete res_code proof_delims known_failures output in (output, msecs, tstplike_proof, outcome) end - val readable_names = debug andalso overlord - val (atp_problem, pool, conjecture_offset, fact_names) = - prepare_atp_problem ctxt readable_names explicit_forall type_sys - explicit_apply hyp_ts concl_t facts - val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses - atp_problem - val _ = File.write_list probfile ss - val conjecture_shape = - conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 - |> map single - val run_twice = has_incomplete_mode andalso not auto + val run_twice = + has_incomplete_mode andalso not auto andalso + length facts >= !atp_run_twice_threshold val timer = Timer.startRealTimer () val result = - run false + run (not run_twice) (if run_twice then - seconds (0.001 * atp_first_iter_time_frac + seconds (0.001 * !atp_first_iter_time_frac * Real.fromInt (Time.toMilliseconds timeout)) else timeout) @@ -431,13 +437,13 @@ (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) - fun cleanup probfile = - if dest_dir = "" then try File.rm probfile else NONE - fun export probfile (_, (output, _, _, _)) = + fun cleanup prob_file = + if dest_dir = "" then try File.rm prob_file else NONE + fun export prob_file (_, (output, _, _, _)) = if dest_dir = "" then () else - File.write (Path.explode (Path.implode probfile ^ "_proof")) output + File.write (Path.explode (Path.implode prob_file ^ "_proof")) output val ((pool, conjecture_shape, fact_names), (output, msecs, tstplike_proof, outcome)) = with_path cleanup export run_on problem_path_name diff -r 054a4e5ac5fb -r 33e107788595 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 20 17:31:58 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Dec 20 18:48:13 2010 +0100 @@ -254,7 +254,8 @@ val facts = get_facts "SMT solver" true smt_relevance_fudge smts val weight = SMT_Weighted_Fact oo weight_smt_fact thy fun smt_head facts = - try (SMT_Solver.smt_filter_head state (facts ())) + (if debug then curry (op o) SOME else try) + (SMT_Solver.smt_filter_head state (facts ())) in smts |> map (`(class_of_smt_solver ctxt)) |> AList.group (op =)