--- 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,
--- 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;
--- 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
--- 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 =)