--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 30 15:03:42 2010 +0200
@@ -306,11 +306,11 @@
ctxt
|> change_dir dir
|> Config.put Sledgehammer.measure_runtime true
- val params = Sledgehammer_Isar.default_params thy []
+ val params = Sledgehammer_Isar.default_params thy
+ [("timeout", Int.toString timeout ^ " s")]
val problem =
{subgoal = 1, goal = (ctxt', (facts, goal)),
- relevance_override = {add = [], del = [], only = false},
- axiom_clauses = NONE, filtered_clauses = NONE}
+ relevance_override = {add = [], del = [], only = false}, axioms = NONE}
val time_limit =
(case hard_timeout of
NONE => I
@@ -318,7 +318,7 @@
val ({outcome, message, used_thm_names,
atp_run_time_in_msecs = time_atp, ...} : Sledgehammer.prover_result,
time_isa) = time_limit (Mirabelle.cpu_time
- (prover params (K "") (Time.fromSeconds timeout))) problem
+ (prover params (K ""))) problem
in
case outcome of
NONE => (message, SH_OK (time_isa, time_atp, used_thm_names))
@@ -381,7 +381,6 @@
fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
let
open Metis_Clauses
- open Sledgehammer_Isar
val thy = Proof.theory_of st
val n0 = length (these (!named_thms))
val (prover_name, _) = get_atp thy args
@@ -389,8 +388,8 @@
AList.lookup (op =) args minimize_timeoutK
|> Option.map (fst o read_int o explode)
|> the_default 5
- val params = default_params thy
- [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
+ val params = Sledgehammer_Isar.default_params thy
+ [("atps", prover_name), ("minimize_timeout", Int.toString timeout ^ " s")]
val minimize =
Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
val _ = log separator
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Jul 30 15:03:42 2010 +0200
@@ -49,9 +49,10 @@
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
fun string_for_term (ATerm (s, [])) = s
+ | string_for_term (ATerm ("equal", ts)) =
+ space_implode " = " (map string_for_term ts)
| string_for_term (ATerm (s, ts)) =
- if s = "equal" then space_implode " = " (map string_for_term ts)
- else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
+ s ^ "(" ^ commas (map string_for_term ts) ^ ")"
fun string_for_quantifier AForall = "!"
| string_for_quantifier AExists = "?"
fun string_for_connective ANot = "~"
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Fri Jul 30 15:03:42 2010 +0200
@@ -13,8 +13,8 @@
MalformedOutput | UnknownError
type prover_config =
- {executable: string * string,
- required_executables: (string * string) list,
+ {exec: string * string,
+ required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -44,8 +44,8 @@
MalformedOutput | UnknownError
type prover_config =
- {executable: string * string,
- required_executables: (string * string) list,
+ {exec: string * string,
+ required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
@@ -60,14 +60,14 @@
fun string_for_failure Unprovable = "The ATP problem is unprovable."
| string_for_failure IncompleteUnprovable =
"The ATP cannot prove the problem."
- | string_for_failure CantConnect = "Can't connect to remote ATP."
+ | string_for_failure CantConnect = "Can't connect to remote server."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
| string_for_failure OldSpass =
- "Warning: Isabelle requires a more recent version of SPASS with \
- \support for the TPTP syntax. To install it, download and extract the \
- \package \"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and \
- \add the \"spass-3.7\" directory's absolute path to " ^
+ "Isabelle requires a more recent version of SPASS with support for the \
+ \TPTP syntax. To install it, download and extract the package \
+ \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
+ \\"spass-3.7\" directory's absolute path to " ^
quote (Path.implode (Path.expand (Path.appends
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"])))) ^
@@ -76,17 +76,18 @@
| string_for_failure NoLibwwwPerl =
"The Perl module \"libwww-perl\"" ^ missing_message_tail
| string_for_failure MalformedInput =
- "Internal Isabelle error: The ATP problem is malformed. Please report \
- \this to the Isabelle developers."
- | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
- | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
+ "The ATP problem is malformed. Please report this to the Isabelle \
+ \developers."
+ | string_for_failure MalformedOutput = "The ATP output is malformed."
+ | string_for_failure UnknownError = "An unknown ATP error occurred."
fun known_failure_in_output output =
find_first (fn (_, pattern) => String.isSubstring pattern output)
#> Option.map fst
val known_perl_failures =
- [(NoPerl, "env: perl"),
+ [(CantConnect, "HTTP error"),
+ (NoPerl, "env: perl"),
(NoLibwwwPerl, "Can't locate HTTP")]
(* named provers *)
@@ -124,8 +125,8 @@
("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
val e_config : prover_config =
- {executable = ("E_HOME", "eproof"),
- required_executables = [],
+ {exec = ("E_HOME", "eproof"),
+ required_execs = [],
arguments = fn _ => fn timeout =>
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
string_of_int (to_generous_secs timeout),
@@ -139,7 +140,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- max_new_relevant_facts_per_iter = 80 (* FIXME *),
+ max_new_relevant_facts_per_iter = 90 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
val e = ("e", e_config)
@@ -148,13 +149,13 @@
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
- {executable = ("ISABELLE_ATP", "scripts/spass"),
- required_executables = [("SPASS_HOME", "SPASS")],
+ {exec = ("ISABELLE_ATP", "scripts/spass"),
+ required_execs = [("SPASS_HOME", "SPASS")],
(* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
\-VarWeight=3 -TimeLimit=" ^
- string_of_int (to_generous_secs timeout div 2))
+ string_of_int ((to_generous_secs timeout + 1) div 2))
|> not complete ? prefix "-SOS=1 ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
@@ -165,7 +166,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(OldSpass, "tptp2dfg")],
- max_new_relevant_facts_per_iter = 26 (* FIXME *),
+ max_new_relevant_facts_per_iter = 35 (* FIXME *),
prefers_theory_relevant = true,
explicit_forall = true}
val spass = ("spass", spass_config)
@@ -173,8 +174,8 @@
(* Vampire *)
val vampire_config : prover_config =
- {executable = ("VAMPIRE_HOME", "vampire"),
- required_executables = [],
+ {exec = ("VAMPIRE_HOME", "vampire"),
+ required_execs = [],
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
" --input_file ",
@@ -186,9 +187,10 @@
known_failures =
[(Unprovable, "UNPROVABLE"),
(IncompleteUnprovable, "CANNOT PROVE"),
+ (TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found")],
- max_new_relevant_facts_per_iter = 40 (* FIXME *),
+ max_new_relevant_facts_per_iter = 50 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}
val vampire = ("vampire", vampire_config)
@@ -221,16 +223,15 @@
({proof_delims, known_failures, max_new_relevant_facts_per_iter,
prefers_theory_relevant, explicit_forall, ...} : prover_config)
: prover_config =
- {executable = ("ISABELLE_ATP", "scripts/remote_atp"),
- required_executables = [],
+ {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
+ required_execs = [],
arguments = fn _ => fn timeout =>
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
the_system atp_prefix,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures =
known_failures @ known_perl_failures @
- [(CantConnect, "HTTP-Error"),
- (TimedOut, "says Timeout")],
+ [(TimedOut, "says Timeout")],
max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
prefers_theory_relevant = prefers_theory_relevant,
explicit_forall = explicit_forall}
@@ -243,8 +244,8 @@
val remote_e = remote_prover e "EP---"
val remote_vampire = remote_prover vampire "Vampire---9"
-fun is_installed ({executable, required_executables, ...} : prover_config) =
- forall (curry (op <>) "" o getenv o fst) (executable :: required_executables)
+fun is_installed ({exec, required_execs, ...} : prover_config) =
+ forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
fun maybe_remote (name, config) =
name |> not (is_installed config) ? remote_name
--- a/src/HOL/Tools/ATP/scripts/remote_atp Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp Fri Jul 30 15:03:42 2010 +0200
@@ -98,7 +98,7 @@
if(!$Response->is_success) {
my $message = $Response->message;
$message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
- print $message . "\n";
+ print "HTTP error: " . $message . "\n";
exit(-1);
} elsif (exists($Options{'w'})) {
print $Response->content;
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Fri Jul 30 15:03:42 2010 +0200
@@ -16,9 +16,9 @@
TConsLit of name * name * name list |
TVarLit of name * name
datatype arity_clause =
- ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+ ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
datatype class_rel_clause =
- ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
+ ClassRelClause of {name: string, subclass: name, superclass: name}
datatype combtyp =
CombTVar of name |
CombTFree of name |
@@ -84,8 +84,6 @@
val tvar_prefix = "T_";
val tfree_prefix = "t_";
-val class_rel_clause_prefix = "clsrel_";
-
val const_prefix = "c_";
val type_const_prefix = "tc_";
val class_prefix = "class_";
@@ -259,7 +257,7 @@
TVarLit of name * name
datatype arity_clause =
- ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+ ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
fun gen_TVars 0 = []
@@ -271,12 +269,12 @@
(`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
(*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
+fun make_axiom_arity_clause (tcons, name, (cls,args)) =
let
val tvars = gen_TVars (length args)
val tvars_srts = ListPair.zip (tvars, args)
in
- ArityClause {axiom_name = axiom_name,
+ ArityClause {name = name,
conclLit = TConsLit (`make_type_class cls,
`make_fixed_type_const tcons,
tvars ~~ tvars),
@@ -287,7 +285,7 @@
(**** Isabelle class relations ****)
datatype class_rel_clause =
- ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
+ ClassRelClause of {name: string, subclass: name, superclass: name}
(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
fun class_pairs _ [] _ = []
@@ -299,10 +297,9 @@
in fold add_supers subs [] end
fun make_class_rel_clause (sub,super) =
- ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^
- ascii_of super,
+ ClassRelClause {name = sub ^ "_" ^ super,
subclass = `make_type_class sub,
- superclass = `make_type_class super};
+ superclass = `make_type_class super}
fun make_class_rel_clauses thy subs supers =
map make_class_rel_clause (class_pairs thy subs supers);
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Jul 30 15:03:42 2010 +0200
@@ -86,11 +86,11 @@
val args = map hol_term_to_fol_FO tms
in Metis.Term.Fn (c, tyargs @ args) end
| (CombVar ((v, _), _), []) => Metis.Term.Var v
- | _ => raise Fail "hol_term_to_fol_FO";
+ | _ => raise METIS ("hol_term_to_fol_FO", "non first-order combterm")
-fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
- | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
+fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
+ | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
| hol_term_to_fol_HO (CombApp (tm1, tm2)) =
Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
@@ -764,12 +764,11 @@
(_,ith)::_ =>
(trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
[ith])
- | _ => (trace_msg (fn () => "Metis: No result");
- raise METIS ("FOL_SOLVE", ""))
+ | _ => (trace_msg (fn () => "Metis: No result"); [])
end
| Metis.Resolution.Satisfiable _ =>
(trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
- raise METIS ("FOL_SOLVE", ""))
+ [])
end;
val type_has_top_sort =
@@ -798,10 +797,8 @@
if mode = HO then
(warning ("Metis: Falling back on \"metisFT\".");
generic_metis_tac FT ctxt ths i st0)
- else if msg = "" then
+ else
Seq.empty
- else
- raise error ("Metis (" ^ loc ^ "): " ^ msg)
val metis_tac = generic_metis_tac HO
val metisF_tac = generic_metis_tac FO
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jul 30 15:03:42 2010 +0200
@@ -30,8 +30,7 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option,
- filtered_clauses: (string * thm) list option}
+ axioms: (string * thm) list option}
type prover_result =
{outcome: failure option,
message: string,
@@ -41,10 +40,8 @@
output: string,
proof: string,
internal_thm_names: string Vector.vector,
- conjecture_shape: int list list,
- filtered_clauses: (string * thm) list}
- type prover =
- params -> minimize_command -> Time.time -> problem -> prover_result
+ conjecture_shape: int list list}
+ type prover = params -> minimize_command -> problem -> prover_result
val dest_dir : string Config.T
val problem_prefix : string Config.T
@@ -72,8 +69,13 @@
(** The Sledgehammer **)
+(* Identifier to distinguish Sledgehammer from other tools using
+ "Async_Manager". *)
val das_Tool = "Sledgehammer"
+(* Freshness almost guaranteed! *)
+val sledgehammer_weak_prefix = "Sledgehammer:"
+
fun kill_atps () = Async_Manager.kill_threads das_Tool "ATPs"
fun running_atps () = Async_Manager.running_threads das_Tool "ATPs"
val messages = Async_Manager.thread_messages das_Tool "ATP"
@@ -100,8 +102,7 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: (string * thm) list option,
- filtered_clauses: (string * thm) list option}
+ axioms: (string * thm) list option}
type prover_result =
{outcome: failure option,
@@ -112,11 +113,9 @@
output: string,
proof: string,
internal_thm_names: string Vector.vector,
- conjecture_shape: int list list,
- filtered_clauses: (string * thm) list}
+ conjecture_shape: int list list}
-type prover =
- params -> minimize_command -> Time.time -> problem -> prover_result
+type prover = params -> minimize_command -> problem -> prover_result
(* configuration attributes *)
@@ -163,7 +162,7 @@
(* Clause preparation *)
datatype fol_formula =
- FOLFormula of {formula_name: string,
+ FOLFormula of {name: string,
kind: kind,
combformula: (name, combterm) formula,
ctypes_sorts: typ list}
@@ -175,12 +174,12 @@
AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
(* ### FIXME: reintroduce
-fun make_clause_table xs =
+fun make_formula_table xs =
fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-(* Remove existing axiom clauses from the conjecture clauses, as this can
+(* Remove existing axioms from the conjecture, as this can
dramatically boost an ATP's performance (for some reason). *)
-fun subtract_cls ax_clauses =
- filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
+fun subtract_cls axioms =
+ filter_out (Termtab.defined (make_formula_table axioms) o prop_of)
*)
fun combformula_for_prop thy =
@@ -235,11 +234,15 @@
| aux _ t = t
in aux (maxidx_of_term t + 1) t end
-(* FIXME: Guarantee freshness *)
-fun concealed_bound_name j = "Sledgehammer" ^ Int.toString j
+fun presimplify_term thy =
+ Skip_Proof.make_thm thy
+ #> Meson.presimplify
+ #> prop_of
+
+fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
fun conceal_bounds Ts t =
subst_bounds (map (Free o apfst concealed_bound_name)
- (length Ts - 1 downto 0 ~~ rev Ts), t)
+ (0 upto length Ts - 1 ~~ Ts), t)
fun reveal_bounds Ts =
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
(0 upto length Ts - 1 ~~ Ts))
@@ -281,29 +284,42 @@
Axiom => HOLogic.true_const
| Conjecture => HOLogic.false_const
-(* making axiom and conjecture clauses *)
-fun make_clause ctxt (formula_name, kind, t) =
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
+ same in Sledgehammer to prevent the discovery of unreplable proofs. *)
+fun freeze_term t =
+ let
+ fun aux (t $ u) = aux t $ aux u
+ | aux (Abs (s, T, t)) = Abs (s, T, aux t)
+ | aux (Var ((s, i), T)) =
+ Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+ | aux t = t
+ in t |> exists_subterm is_Var t ? aux end
+
+(* making axiom and conjecture formulas *)
+fun make_formula ctxt presimp (name, kind, t) =
let
val thy = ProofContext.theory_of ctxt
- (* ### FIXME: perform other transformations previously done by
- "Clausifier.to_nnf", e.g. "HOL.If" *)
val t = t |> transform_elim_term
|> Object_Logic.atomize_term thy
+ val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
|> extensionalize_term
+ |> presimp ? presimplify_term thy
+ |> perhaps (try (HOLogic.dest_Trueprop))
|> introduce_combinators_in_term ctxt kind
+ |> kind = Conjecture ? freeze_term
val (combformula, ctypes_sorts) = combformula_for_prop thy t []
in
- FOLFormula {formula_name = formula_name, combformula = combformula,
- kind = kind, ctypes_sorts = ctypes_sorts}
+ FOLFormula {name = name, combformula = combformula, kind = kind,
+ ctypes_sorts = ctypes_sorts}
end
-fun make_axiom_clause ctxt (name, th) =
- (name, make_clause ctxt (name, Axiom, prop_of th))
-fun make_conjecture_clauses ctxt ts =
- map2 (fn j => fn t => make_clause ctxt (Int.toString j, Conjecture, t))
+fun make_axiom ctxt presimp (name, th) =
+ (name, make_formula ctxt presimp (name, Axiom, prop_of th))
+fun make_conjectures ctxt ts =
+ map2 (fn j => fn t => make_formula ctxt true (Int.toString j, Conjecture, t))
(0 upto length ts - 1) ts
-(** Helper clauses **)
+(** Helper facts **)
fun count_combterm (CombConst ((s, _), _, _)) =
Symtab.map_entry s (Integer.add 1)
@@ -328,52 +344,40 @@
Symtab.make (maps (maps (map (rpair 0) o fst))
[optional_helpers, optional_typed_helpers])
-fun get_helper_clauses ctxt is_FO full_types conjectures axclauses =
+fun get_helper_facts ctxt is_FO full_types conjectures axioms =
let
- val ct = fold (fold count_fol_formula) [conjectures, axclauses]
- init_counters
+ val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
fun is_needed c = the (Symtab.lookup ct c) > 0
- val cnfs =
- (optional_helpers
- |> full_types ? append optional_typed_helpers
- |> maps (fn (ss, ths) =>
- if exists is_needed ss then map (`Thm.get_name_hint) ths
- else [])) @
- (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
- in map (snd o make_axiom_clause ctxt) cnfs end
+ in
+ (optional_helpers
+ |> full_types ? append optional_typed_helpers
+ |> maps (fn (ss, ths) =>
+ if exists is_needed ss then map (`Thm.get_name_hint) ths
+ else [])) @
+ (if is_FO then [] else map (`Thm.get_name_hint) mandatory_helpers)
+ |> map (snd o make_axiom ctxt false)
+ end
-fun s_not (@{const Not} $ t) = t
- | s_not t = @{const Not} $ t
+fun meta_not t = @{const "==>"} $ t $ @{prop False}
-(* prepare for passing to writer,
- create additional clauses based on the information from extra_cls *)
-fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
+fun prepare_formulas ctxt full_types hyp_ts concl_t axcls =
let
val thy = ProofContext.theory_of ctxt
val goal_t = Logic.list_implies (hyp_ts, concl_t)
val is_FO = Meson.is_fol_term thy goal_t
- val axtms = map (prop_of o snd) extra_cls
+ val axtms = map (prop_of o snd) axcls
val subs = tfree_classes_of_terms [goal_t]
val supers = tvar_classes_of_terms axtms
val tycons = type_consts_of_terms thy (goal_t :: axtms)
- (* TFrees in conjecture clauses; TVars in axiom clauses *)
- val conjectures =
- map (s_not o HOLogic.dest_Trueprop) hyp_ts @
- [HOLogic.dest_Trueprop concl_t]
- |> make_conjecture_clauses ctxt
- val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
- val (clnames, axiom_clauses) =
- ListPair.unzip (map (make_axiom_clause ctxt) axcls)
- (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
- "get_helper_clauses" call? *)
- val helper_clauses =
- get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
+ (* TFrees in the conjecture; TVars in the axioms *)
+ val conjectures = map meta_not hyp_ts @ [concl_t] |> make_conjectures ctxt
+ val (clnames, axioms) = ListPair.unzip (map (make_axiom ctxt true) axcls)
+ val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in
(Vector.fromList clnames,
- (conjectures, axiom_clauses, extra_clauses, helper_clauses,
- class_rel_clauses, arity_clauses))
+ (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
end
fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
@@ -397,10 +401,15 @@
val (head, args) = strip_combterm_comb u
val (x, ty_args) =
case head of
- CombConst (name, _, ty_args) =>
- if fst name = "equal" then
+ CombConst (name as (s, s'), _, ty_args) =>
+ if s = "equal" then
(if top_level andalso length args = 2 then name
else ("c_fequal", @{const_name fequal}), [])
+ else if top_level then
+ case s of
+ "c_False" => (("$false", s'), [])
+ | "c_True" => (("$true", s'), [])
+ | _ => (name, if full_types then [] else ty_args)
else
(name, if full_types then [] else ty_args)
| CombVar (name, _) => (name, [])
@@ -424,15 +433,14 @@
(type_literals_for_types ctypes_sorts))
(formula_for_combformula full_types combformula)
-fun problem_line_for_axiom full_types
- (formula as FOLFormula {formula_name, kind, ...}) =
- Fof (axiom_prefix ^ ascii_of formula_name, kind,
- formula_for_axiom full_types formula)
+fun problem_line_for_fact prefix full_types
+ (formula as FOLFormula {name, kind, ...}) =
+ Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
-fun problem_line_for_class_rel_clause
- (ClassRelClause {axiom_name, subclass, superclass, ...}) =
+fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
+ superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
- Fof (ascii_of axiom_name, Axiom,
+ Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
AAtom (ATerm (superclass, [ty_arg]))]))
end
@@ -442,17 +450,17 @@
| fo_literal_for_arity_literal (TVarLit (c, sort)) =
(false, ATerm (c, [ATerm (sort, [])]))
-fun problem_line_for_arity_clause
- (ArityClause {axiom_name, conclLit, premLits, ...}) =
- Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
+fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
+ ...}) =
+ Fof (arity_clause_prefix ^ ascii_of name, Axiom,
mk_ahorn (map (formula_for_fo_literal o apfst not
o fo_literal_for_arity_literal) premLits)
(formula_for_fo_literal
(fo_literal_for_arity_literal conclLit)))
fun problem_line_for_conjecture full_types
- (FOLFormula {formula_name, kind, combformula, ...}) =
- Fof (conjecture_prefix ^ formula_name, kind,
+ (FOLFormula {name, kind, combformula, ...}) =
+ Fof (conjecture_prefix ^ name, kind,
formula_for_combformula full_types combformula)
fun free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =
@@ -596,17 +604,18 @@
(const_table_for_problem explicit_apply problem) problem
fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
- file (conjectures, axiom_clauses, extra_clauses,
- helper_clauses, class_rel_clauses, arity_clauses) =
+ file (conjectures, axioms, helper_facts, class_rel_clauses,
+ arity_clauses) =
let
- val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
+ val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
+ val helper_lines =
+ map (problem_line_for_fact helper_prefix full_types) helper_facts
+ val conjecture_lines =
+ map (problem_line_for_conjecture full_types) conjectures
+ val tfree_lines = problem_lines_for_free_types conjectures
val class_rel_lines =
map problem_line_for_class_rel_clause class_rel_clauses
val arity_lines = map problem_line_for_arity_clause arity_clauses
- val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
- val conjecture_lines =
- map (problem_line_for_conjecture full_types) conjectures
- val tfree_lines = problem_lines_for_free_types conjectures
(* Reordering these might or might not confuse the proof reconstruction
code or the SPASS Flotter hack. *)
val problem =
@@ -638,7 +647,8 @@
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
val parse_clause_formula_pair =
- $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")"
+ $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id
+ --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")"
--| Scan.option ($$ ",")
val parse_clause_formula_relation =
Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
@@ -664,8 +674,8 @@
|> map (fn s => find_index (curry (op =) s) seq + 1)
in
(conjecture_shape |> map (maps renumber_conjecture),
- seq |> map (the o AList.lookup (op =) name_map)
- |> map (fn s => case try (unprefix axiom_prefix) s of
+ seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the
+ |> try (unprefix axiom_prefix) of
SOME s' => undo_ascii_of s'
| NONE => "")
|> Vector.fromList)
@@ -677,33 +687,29 @@
(* generic TPTP-based provers *)
fun prover_fun name
- {executable, required_executables, arguments, proof_delims,
- known_failures, max_new_relevant_facts_per_iter,
- prefers_theory_relevant, explicit_forall}
+ {exec, required_execs, arguments, proof_delims, known_failures,
+ max_new_relevant_facts_per_iter, prefers_theory_relevant,
+ explicit_forall}
({debug, overlord, full_types, explicit_apply, relevance_threshold,
relevance_convergence, theory_relevant, defs_relevant, isar_proof,
- isar_shrink_factor, ...} : params)
- minimize_command timeout
- ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
- : problem) =
+ isar_shrink_factor, timeout, ...} : params)
+ minimize_command
+ ({subgoal, goal, relevance_override, axioms} : problem) =
let
- (* get clauses and prepare them for writing *)
val (ctxt, (_, th)) = goal;
val thy = ProofContext.theory_of ctxt
(* ### FIXME: (1) preprocessing for "if" etc. *)
val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
- val the_filtered_clauses =
- case filtered_clauses of
- SOME fcls => fcls
+ val the_axioms =
+ case axioms of
+ SOME axioms => axioms
| NONE => relevant_facts full_types relevance_threshold
relevance_convergence defs_relevant
max_new_relevant_facts_per_iter
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal hyp_ts concl_t
- val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
- val (internal_thm_names, clauses) =
- prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
- the_filtered_clauses
+ val (internal_thm_names, formulas) =
+ prepare_formulas ctxt full_types hyp_ts concl_t the_axioms
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
@@ -722,7 +728,7 @@
else error ("No such directory: " ^ the_dest_dir ^ ".")
end;
- val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable)
+ val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
(* write out problem file and call prover *)
fun command_line complete probfile =
let
@@ -746,8 +752,7 @@
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode;
in (output, as_time t) end;
fun run_on probfile =
- case filter (curry (op =) "" o getenv o fst)
- (executable :: required_executables) of
+ case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
(home_var, _) :: _ =>
error ("The environment variable " ^ quote home_var ^ " is not set.")
| [] =>
@@ -771,7 +776,7 @@
val readable_names = debug andalso overlord
val (pool, conjecture_offset) =
write_tptp_file thy readable_names explicit_forall full_types
- explicit_apply probfile clauses
+ explicit_apply probfile formulas
val conjecture_shape =
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
@@ -814,8 +819,7 @@
{outcome = outcome, message = message, pool = pool,
used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
output = output, proof = proof, internal_thm_names = internal_thm_names,
- conjecture_shape = conjecture_shape,
- filtered_clauses = the_filtered_clauses}
+ conjecture_shape = conjecture_shape}
end
fun get_prover_fun thy name = prover_fun name (get_prover thy name)
@@ -837,10 +841,9 @@
let
val problem =
{subgoal = i, goal = (ctxt, (facts, goal)),
- relevance_override = relevance_override, axiom_clauses = NONE,
- filtered_clauses = NONE}
+ relevance_override = relevance_override, axioms = NONE}
in
- prover params (minimize_command name) timeout problem |> #message
+ prover params (minimize_command name) problem |> #message
handle ERROR message => "Error: " ^ message ^ "\n"
end)
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Jul 30 15:03:42 2010 +0200
@@ -88,18 +88,9 @@
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
val fresh_prefix = "Sledgehammer.Fresh."
-
val flip = Option.map not
-
-val boring_natural_consts = [@{const_name If}]
-(* Including equality in this list might be expected to stop rules like
- subset_antisym from being chosen, but for some reason filtering works better
- with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
- because any remaining occurrences must be within comprehensions. *)
-val boring_cnf_consts =
- [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
- @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
- @{const_name "op ="}]
+(* These are typically simplified away by "Meson.presimplify". *)
+val boring_consts = [@{const_name If}, @{const_name Let}]
fun get_consts_typs thy pos ts =
let
@@ -149,7 +140,7 @@
do_term t0 #> do_formula pos t1 (* theory constant *)
| _ => do_term t
in
- Symtab.empty |> fold (Symtab.update o rpair []) boring_natural_consts
+ Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
|> fold (do_formula pos) ts
end
@@ -213,11 +204,8 @@
(the (Symtab.lookup const_tab c)
handle Option.Option => raise Fail ("Const: " ^ c)) 0
-(*A surprising number of theorems contain only a few significant constants.
- These include all induction rules, and other general theorems. Filtering
- theorems in clause form reveals these complexities in the form of Skolem
- functions. If we were instead to filter theorems in their natural form,
- some other method of measuring theorem complexity would become necessary.*)
+(* A surprising number of theorems contain only a few significant constants.
+ These include all induction rules, and other general theorems. *)
(* "log" seems best in practice. A constant function of one ignores the constant
frequencies. *)
@@ -228,13 +216,13 @@
(*Relevant constants are weighted according to frequency,
but irrelevant constants are simply counted. Otherwise, Skolem functions,
- which are rare, would harm a clause's chances of being picked.*)
-fun clause_weight const_tab gctyps consts_typs =
- let val rel = filter (uni_mem gctyps) consts_typs
- val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
- in
- rel_weight / (rel_weight + real (length consts_typs - length rel))
- end;
+ which are rare, would harm a formula's chances of being picked.*)
+fun formula_weight const_tab gctyps consts_typs =
+ let
+ val rel = filter (uni_mem gctyps) consts_typs
+ val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
+ val res = rel_weight / (rel_weight + real (length consts_typs - length rel))
+ in if Real.isFinite res then res else 0.0 end
(*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
@@ -270,13 +258,13 @@
| _ => false
end;
-type annotated_cnf_thm = (string * thm) * (string * const_typ list) list
+type annotated_thm = (string * thm) * (string * const_typ list) list
(*For a reverse sort, putting the largest values first.*)
fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
-(*Limit the number of new clauses, to prevent runaway acceptance.*)
-fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) =
+(* Limit the number of new facts, to prevent runaway acceptance. *)
+fun take_best max_new (newpairs : (annotated_thm * real) list) =
let val nnew = length newpairs
in
if nnew <= max_new then (map #1 newpairs, [])
@@ -294,8 +282,8 @@
end
end;
-fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
- ({add, del, ...} : relevance_override) const_tab =
+fun relevant_facts ctxt relevance_convergence defs_relevant max_new
+ ({add, del, ...} : relevance_override) const_tab =
let
val thy = ProofContext.theory_of ctxt
val add_thms = maps (ProofContext.get_fact ctxt) add
@@ -323,7 +311,8 @@
val weight =
if member Thm.eq_thm add_thms th then 1.0
else if member Thm.eq_thm del_thms th then 0.0
- else clause_weight const_tab rel_const_tab consts_typs
+ else formula_weight const_tab rel_const_tab consts_typs
+val _ = (if Real.isFinite weight then () else error ("*** " ^ Real.toString weight)) (*###*)
in
if weight >= threshold orelse
(defs_relevant andalso defines thy th rel_const_tab) then
@@ -335,7 +324,7 @@
relevant (newrels, ax :: rejects) axs
end
in
- trace_msg (fn () => "relevant_clauses, current threshold: " ^
+ trace_msg (fn () => "relevant_facts, current threshold: " ^
Real.toString threshold);
relevant ([], [])
end
@@ -353,7 +342,7 @@
val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
Symtab.empty
val goal_const_tab = get_consts_typs thy (SOME true) goal_ts
- val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
+ val relevance_threshold = 0.8 * relevance_threshold (* FIXME *)
val _ =
trace_msg (fn () => "Initial constants: " ^
commas (goal_const_tab
@@ -361,11 +350,11 @@
|> filter (curry (op <>) [] o snd)
|> map fst))
val relevant =
- relevant_clauses ctxt relevance_convergence defs_relevant max_new
- relevance_override const_tab relevance_threshold
- goal_const_tab
- (map (pair_consts_typs_axiom theory_relevant thy)
- axioms)
+ relevant_facts ctxt relevance_convergence defs_relevant max_new
+ relevance_override const_tab relevance_threshold
+ goal_const_tab
+ (map (pair_consts_typs_axiom theory_relevant thy)
+ axioms)
in
trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
relevant
@@ -387,11 +376,9 @@
String.isSuffix "_def" a orelse String.isSuffix "_defs" a
end;
-fun make_clause_table xs =
+fun make_fact_table xs =
fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
-
-fun make_unique xs =
- Termtab.fold (cons o snd) (make_clause_table xs) []
+fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) []
(* FIXME: put other record thms here, or declare as "no_atp" *)
val multi_base_blacklist =
@@ -427,8 +414,7 @@
| apply_depth _ = 0
fun is_formula_too_complex t =
- apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
- formula_has_too_many_lambdas [] t
+ apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
@@ -459,7 +445,8 @@
(facts, []) |-> Facts.fold_static (fn (name, ths0) =>
if Facts.is_concealed facts name orelse
(respect_no_atp andalso is_package_def name) orelse
- member (op =) multi_base_blacklist (Long_Name.base_name name) then
+ member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
+ String.isSuffix "_def_raw" (* FIXME: crude hack *) name then
I
else
let
@@ -512,12 +499,13 @@
(* ATP invocation methods setup *)
(***************************************************************)
-(**** Predicates to detect unwanted clauses (prolific or likely to cause
+(**** Predicates to detect unwanted facts (prolific or likely to cause
unsoundness) ****)
(** Too general means, positive equality literal with a variable X as one operand,
when X does not occur properly in the other operand. This rules out clearly
- inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
+ inconsistent facts such as V = a | V = b, though it by no means guarantees
+ soundness. **)
fun var_occurs_in_term ix =
let
@@ -532,6 +520,7 @@
(*Unwanted equalities include
(1) those between a variable that does not properly occur in the second operand,
(2) those between a variable and a record, since these seem to be prolific "cases" thms
+ (* FIXME: still a problem? *)
*)
fun too_general_eqterms (Var (ix,T), t) =
not (var_occurs_in_term ix t) orelse is_record_type T
@@ -544,14 +533,14 @@
fun has_typed_var tycons = exists_subterm
(fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
-(* Clauses are forbidden to contain variables of these types. The typical reason
+(* Facts are forbidden to contain variables of these types. The typical reason
is that they lead to unsoundness. Note that "unit" satisfies numerous
- equations like "?x = ()". The resulting clause will have no type constraint,
+ equations like "?x = ()". The resulting clauses will have no type constraint,
yielding false proofs. Even "bool" leads to many unsound proofs, though only
for higher-order problems. *)
val dangerous_types = [@{type_name unit}, @{type_name bool}];
-(* Clauses containing variables of type "unit" or "bool" or of the form
+(* Facts containing variables of type "unit" or "bool" or of the form
"?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are
omitted. *)
fun is_dangerous_term _ @{prop True} = true
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Jul 30 15:03:42 2010 +0200
@@ -18,7 +18,7 @@
structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
struct
-open Metis_Clauses
+open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Fact_Filter
open Sledgehammer_Proof_Reconstruct
@@ -27,44 +27,61 @@
(* wrapper for calling external prover *)
fun string_for_failure Unprovable = "Unprovable."
- | string_for_failure IncompleteUnprovable = "Failed."
| string_for_failure TimedOut = "Timed out."
- | string_for_failure OutOfResources = "Failed."
- | string_for_failure OldSpass = "Error."
- | string_for_failure MalformedOutput = "Error."
- | string_for_failure UnknownError = "Failed."
-fun string_for_outcome NONE = "Success."
- | string_for_outcome (SOME failure) = string_for_failure failure
+ | string_for_failure _ = "Unknown error."
-fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
- filtered_clauses name_thms_pairs =
+fun n_theorems name_thms_pairs =
+ let val n = length name_thms_pairs in
+ string_of_int n ^ " theorem" ^ plural_s n ^
+ (if n > 0 then
+ ": " ^ space_implode " "
+ (name_thms_pairs
+ |> map (perhaps (try (unprefix chained_prefix)))
+ |> sort_distinct string_ord)
+ else
+ "")
+ end
+
+fun test_theorems ({debug, verbose, overlord, atps, full_types,
+ relevance_threshold, relevance_convergence, theory_relevant,
+ defs_relevant, isar_proof, isar_shrink_factor,
+ ...} : params)
+ (prover : prover) explicit_apply timeout subgoal state
+ name_thms_pairs =
let
- val num_theorems = length name_thms_pairs
val _ =
- priority ("Testing " ^ string_of_int num_theorems ^
- " theorem" ^ plural_s num_theorems ^
- (if num_theorems > 0 then
- ": " ^ space_implode " "
- (name_thms_pairs
- |> map fst |> sort_distinct string_ord)
- else
- "") ^ "...")
- val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
+ priority ("Testing " ^ n_theorems (map fst name_thms_pairs) ^ "...")
+ val params =
+ {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
+ full_types = full_types, explicit_apply = explicit_apply,
+ relevance_threshold = relevance_threshold,
+ relevance_convergence = relevance_convergence,
+ theory_relevant = theory_relevant, defs_relevant = defs_relevant,
+ isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
+ timeout = timeout, minimize_timeout = timeout}
+ val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{subgoal = subgoal, goal = (ctxt, (facts, goal)),
relevance_override = {add = [], del = [], only = false},
- axiom_clauses = SOME name_thm_pairs,
- filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)}
+ axioms = SOME axioms}
+ val result as {outcome, used_thm_names, ...} =
+ prover params (K "") problem
in
- prover params (K "") timeout problem
- |> tap (fn result : prover_result =>
- priority (string_for_outcome (#outcome result)))
+ priority (case outcome of
+ NONE =>
+ if length used_thm_names = length name_thms_pairs then
+ "Found proof."
+ else
+ "Found proof with " ^ n_theorems used_thm_names ^ "."
+ | SOME failure => string_for_failure failure);
+ result
end
(* minimalization of thms *)
-fun filter_used_facts used = filter (member (op =) used o fst)
+fun filter_used_facts used =
+ filter (member (op =) used o perhaps (try (unprefix chained_prefix)) o fst)
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
@@ -75,34 +92,52 @@
(filter_used_facts used_thm_names seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
-fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
- isar_proof, isar_shrink_factor, ...})
- i n state name_thms_pairs =
+(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
+ preprocessing time is included in the estimate below but isn't part of the
+ timeout. *)
+val fudge_msecs = 250
+
+fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
+ | minimize_theorems
+ (params as {debug, verbose, overlord, atps as atp :: _, full_types,
+ relevance_threshold, relevance_convergence, theory_relevant,
+ defs_relevant, isar_proof, isar_shrink_factor,
+ minimize_timeout, ...})
+ i n state name_thms_pairs =
let
val thy = Proof.theory_of state
- val prover = case atps of
- [atp_name] => get_prover_fun thy atp_name
- | _ => error "Expected a single ATP."
+ val prover = get_prover_fun thy atp
val msecs = Time.toMilliseconds minimize_timeout
val _ =
- priority ("Sledgehammer minimizer: ATP " ^ quote (the_single atps) ^
+ priority ("Sledgehammer minimizer: ATP " ^ quote atp ^
" with a time limit of " ^ string_of_int msecs ^ " ms.")
- val test_facts =
- sledgehammer_test_theorems params prover minimize_timeout i state
- val {context = ctxt, goal, ...} = Proof.goal state;
+ val {context = ctxt, goal, ...} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i
+ val explicit_apply =
+ not (forall (Meson.is_fol_term thy)
+ (concl_t :: hyp_ts @ maps (map prop_of o snd) name_thms_pairs))
+ fun do_test timeout =
+ test_theorems params prover explicit_apply timeout i state
+ val timer = Timer.startRealTimer ()
in
- (* try prove first to check result and get used theorems *)
- (case test_facts NONE name_thms_pairs of
- result as {outcome = NONE, pool, proof, used_thm_names,
- conjecture_shape, filtered_clauses, ...} =>
+ (case do_test minimize_timeout name_thms_pairs of
+ result as {outcome = NONE, pool, used_thm_names,
+ conjecture_shape, ...} =>
let
+ val time = Timer.checkRealTimer timer
+ val new_timeout =
+ Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
+ |> Time.fromMilliseconds
val (min_thms, {proof, internal_thm_names, ...}) =
- sublinear_minimize (test_facts (SOME filtered_clauses))
- (filter_used_facts used_thm_names name_thms_pairs)
- ([], result)
- val m = length min_thms
+ sublinear_minimize (do_test new_timeout)
+ (filter_used_facts used_thm_names name_thms_pairs) ([], result)
+ val n = length min_thms
val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")
+ ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
+ (case filter (String.isPrefix chained_prefix o fst) min_thms of
+ [] => ""
+ | chained => " (including " ^ Int.toString (length chained) ^
+ " chained)") ^ ".")
in
(SOME min_thms,
proof_text isar_proof
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 30 15:03:42 2010 +0200
@@ -88,8 +88,8 @@
("no_isar_proof", "isar_proof")]
val params_for_minimize =
- ["debug", "verbose", "overlord", "full_types", "explicit_apply",
- "isar_proof", "isar_shrink_factor", "minimize_timeout"]
+ ["debug", "verbose", "overlord", "full_types", "isar_proof",
+ "isar_shrink_factor", "minimize_timeout"]
val property_dependent_params = ["atps", "full_types", "timeout"]
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Jul 30 15:03:42 2010 +0200
@@ -12,6 +12,8 @@
val axiom_prefix : string
val conjecture_prefix : string
+ val helper_prefix : string
+ val class_rel_clause_prefix : string
val arity_clause_prefix : string
val tfrees_name : string
val metis_line: bool -> int -> int -> string list -> string
@@ -40,7 +42,9 @@
val axiom_prefix = "ax_"
val conjecture_prefix = "conj_"
-val arity_clause_prefix = "clsarity_"
+val helper_prefix = "help_"
+val class_rel_clause_prefix = "clrel_";
+val arity_clause_prefix = "arity_"
val tfrees_name = "tfrees"
(* Simple simplifications to ensure that sort annotations don't leave a trail of
@@ -67,10 +71,10 @@
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
fun index_in_shape x = find_index (exists (curry (op =) x))
-fun is_axiom_clause_number thm_names num =
+fun is_axiom_number thm_names num =
num > 0 andalso num <= Vector.length thm_names andalso
Vector.sub (thm_names, num - 1) <> ""
-fun is_conjecture_clause_number conjecture_shape num =
+fun is_conjecture_number conjecture_shape num =
index_in_shape num conjecture_shape >= 0
fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
@@ -281,7 +285,7 @@
(SOME b, [T]) => (pos, b, T)
| _ => raise FO_TERM [u]
-(** Accumulate type constraints in a clause: negative type literals **)
+(** Accumulate type constraints in a formula: negative type literals **)
fun add_var (key, z) = Vartab.map_default (key, []) (cons z)
fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl)
| add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl)
@@ -407,8 +411,8 @@
| frees as (_, free_T) :: _ =>
Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t)
-(* Interpret a list of syntax trees as a clause, extracting sort constraints
- as they appear in the formula. *)
+(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
+ appear in the formula. *)
fun prop_from_formula thy full_types tfrees phi =
let
fun do_formula pos phi =
@@ -484,13 +488,13 @@
| replace_deps_in_line p (Inference (num, t, deps)) =
Inference (num, t, fold (union (op =) o replace_one_dep p) deps [])
-(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
- only in type information.*)
+(* Discard axioms; consolidate adjacent lines that prove the same formula, since
+ they differ only in type information.*)
fun add_line _ _ (line as Definition _) lines = line :: lines
| add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
- (* No dependencies: axiom, conjecture clause, or internal axioms or
- definitions (Vampire). *)
- if is_axiom_clause_number thm_names num then
+ (* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or
+ definitions. *)
+ if is_axiom_number thm_names num then
(* Axioms are not proof lines. *)
if is_only_type_information t then
map (replace_deps_in_line (num, [])) lines
@@ -499,8 +503,8 @@
(_, []) => lines (*no repetition of proof line*)
| (pre, Inference (num', _, _) :: post) =>
pre @ map (replace_deps_in_line (num', [num])) post
- else if is_conjecture_clause_number conjecture_shape num then
- Inference (num, t, []) :: lines
+ else if is_conjecture_number conjecture_shape num then
+ Inference (num, negate_term t, []) :: lines
else
map (replace_deps_in_line (num, [])) lines
| add_line _ _ (Inference (num, t, deps)) lines =
@@ -539,8 +543,8 @@
| add_desired_line isar_shrink_factor conjecture_shape thm_names frees
(Inference (num, t, deps)) (j, lines) =
(j + 1,
- if is_axiom_clause_number thm_names num orelse
- is_conjecture_clause_number conjecture_shape num orelse
+ if is_axiom_number thm_names num orelse
+ is_conjecture_number conjecture_shape num orelse
(not (is_only_type_information t) andalso
null (Term.add_tvars t []) andalso
not (exists_subterm (is_bad_free frees) t) andalso
@@ -562,10 +566,8 @@
let
fun axiom_name num =
let val j = Int.fromString num |> the_default ~1 in
- if is_axiom_clause_number thm_names j then
- SOME (Vector.sub (thm_names, j - 1))
- else
- NONE
+ if is_axiom_number thm_names j then SOME (Vector.sub (thm_names, j - 1))
+ else NONE
end
val tokens_of =
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
@@ -655,7 +657,7 @@
| smart_case_split proofs facts = CaseSplit (proofs, facts)
fun add_fact_from_dep thm_names num =
- if is_axiom_clause_number thm_names num then
+ if is_axiom_number thm_names num then
apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
else
apfst (insert (op =) (raw_prefix, num))
--- a/src/HOL/Tools/meson.ML Thu Jul 29 18:16:35 2010 +0200
+++ b/src/HOL/Tools/meson.ML Fri Jul 30 15:03:42 2010 +0200
@@ -14,6 +14,7 @@
val too_many_clauses: Proof.context option -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
val finish_cnf: thm list -> thm list
+ val presimplify: thm -> thm
val make_nnf: Proof.context -> thm -> thm
val skolemize: Proof.context -> thm -> thm
val is_fol_term: theory -> term -> bool
@@ -389,10 +390,13 @@
fun sort_clauses ths = sort (make_ord fewerlits) ths;
-(*True if the given type contains bool anywhere*)
-fun has_bool (Type("bool",_)) = true
- | has_bool (Type(_, Ts)) = exists has_bool Ts
- | has_bool _ = false;
+fun has_bool @{typ bool} = true
+ | has_bool (Type (_, Ts)) = exists has_bool Ts
+ | has_bool _ = false
+
+fun has_fun (Type (@{type_name fun}, _)) = true
+ | has_fun (Type (_, Ts)) = exists has_fun Ts
+ | has_fun _ = false
(*Is the string the name of a connective? Really only | and Not can remain,
since this code expects to be called on a clause form.*)
@@ -404,7 +408,7 @@
of any argument contains bool.*)
val has_bool_arg_const =
exists_Const
- (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
+ (fn (c,T) => not(is_conn c) andalso exists has_bool (binder_types T));
(*A higher-order instance of a first-order constant? Example is the definition of
one, 1, at a function type in theory SetsAndFunctions.*)
@@ -417,8 +421,9 @@
Also rejects functions whose arguments are Booleans or other functions.*)
fun is_fol_term thy t =
Term.is_first_order ["all","All","Ex"] t andalso
- not (exists_subterm (fn Var (_, T) => has_bool T | _ => false) t orelse
- has_bool_arg_const t orelse
+ not (exists_subterm (fn Var (_, T) => has_bool T orelse has_fun T
+ | _ => false) t orelse
+ has_bool_arg_const t orelse
exists_Const (higher_inst_const thy) t orelse
has_meta_conn t);
@@ -529,9 +534,12 @@
HOL_basic_ss addsimps nnf_extra_simps
addsimprocs [defALL_regroup,defEX_regroup, @{simproc neq}, @{simproc let_simp}];
+val presimplify =
+ rewrite_rule (map safe_mk_meta_eq nnf_simps)
+ #> simplify nnf_ss
+
fun make_nnf ctxt th = case prems_of th of
- [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
- |> simplify nnf_ss
+ [] => th |> presimplify
|> make_nnf1 ctxt
| _ => raise THM ("make_nnf: premises in argument", 0, [th]);