--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 18:15:40 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Mon Jun 28 18:46:42 2010 +0200
@@ -8,7 +8,6 @@
signature ATP_MANAGER =
sig
- type cnf_thm = Clausifier.cnf_thm
type name_pool = Metis_Clauses.name_pool
type relevance_override = Sledgehammer_Fact_Filter.relevance_override
type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
@@ -31,8 +30,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: cnf_thm list option,
- filtered_clauses: cnf_thm list option}
+ axiom_clauses: ((string * int) * thm) list option,
+ filtered_clauses: ((string * int) * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
MalformedInput | MalformedOutput | UnknownError
@@ -46,7 +45,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: cnf_thm list}
+ filtered_clauses: ((string * int) * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
@@ -98,8 +97,8 @@
{subgoal: int,
goal: Proof.context * (thm list * thm),
relevance_override: relevance_override,
- axiom_clauses: cnf_thm list option,
- filtered_clauses: cnf_thm list option}
+ axiom_clauses: ((string * int) * thm) list option,
+ filtered_clauses: ((string * int) * thm) list option}
datatype failure =
Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
@@ -115,7 +114,7 @@
proof: string,
internal_thm_names: string Vector.vector,
conjecture_shape: int list list,
- filtered_clauses: cnf_thm list}
+ filtered_clauses: ((string * int) * thm) list}
type prover =
params -> minimize_command -> Time.time -> problem -> prover_result
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 28 18:15:40 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Mon Jun 28 18:46:42 2010 +0200
@@ -139,12 +139,13 @@
val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
val goal_cls = List.concat goal_clss
val the_filtered_clauses =
- (case filtered_clauses of
- NONE => relevant_facts full_types relevance_threshold
+ case filtered_clauses of
+ SOME fcls => fcls
+ | NONE => relevant_facts full_types relevance_threshold
relevance_convergence defs_relevant max_axiom_clauses
(the_default prefers_theory_relevant theory_relevant)
relevance_override goal goal_cls
- | SOME fcls => fcls);
+ |> cnf_rules_pairs thy
val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
val (internal_thm_names, clauses) =
prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses