# HG changeset patch # User blanchet # Date 1292843555 -3600 # Node ID a96ac4d180b7e5e6199e5af1a061cac45dded9e3 # Parent fc8419fd47353c56e8c28d440f5d6ae133d9353f optionally supply constant weights to E -- turned off by default until properly parameterized diff -r fc8419fd4735 -r a96ac4d180b7 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon Dec 20 08:55:36 2010 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Dec 20 12:12:35 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,28 @@ 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 4.0 +val e_default_weight = Unsynchronized.ref 0.5 + +fun e_weights weights = + if !e_generate_weights then + "(1*FunWeight(ConstPrio," ^ + string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^ + ",1,1.5,1.5,1.5" ^ + (weights () + |> map (fn (s, w) => "," ^ s ^ ":" ^ + string_of_int (Real.ceil (w * !e_weight_factor))) + |> implode) ^ ")+5*AutoDev)" + else + "AutoDev" + 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 -x'" ^ 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 +146,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 +173,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 +235,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 fc8419fd4735 -r a96ac4d180b7 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Dec 20 08:55:36 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Dec 20 12:12:35 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 fc8419fd4735 -r a96ac4d180b7 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 20 08:55:36 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Dec 20 12:12:35 2010 +0100 @@ -53,6 +53,7 @@ type prover = params -> minimize_command -> prover_problem -> prover_result (* for experimentation purposes -- do not use in production code *) + 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 +319,16 @@ | 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_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 +360,7 @@ 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 +val command = Path.explode ("/Users/blanchet/misc/E-weights/PROVER/" ^ snd exec) (*###*) fun split_time s = let val split = String.tokens (fn c => str c = "\n"); @@ -378,16 +372,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 +412,12 @@ 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 timer = Timer.startRealTimer () val result = run false (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 +434,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