90 Metis_Resolution.Contradiction mth => |
90 Metis_Resolution.Contradiction mth => |
91 let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
91 let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
92 Metis_Thm.toString mth) |
92 Metis_Thm.toString mth) |
93 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
93 val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
94 (*add constraints arising from converting goal to clause form*) |
94 (*add constraints arising from converting goal to clause form*) |
95 val new_skolem_var_count = Unsynchronized.ref 1 |
|
96 val proof = Metis_Proof.proof mth |
95 val proof = Metis_Proof.proof mth |
97 val result = |
96 val result = fold (replay_one_inference ctxt' mode old_skolems) |
98 fold (replay_one_inference ctxt' mode |
97 proof axioms |
99 (old_skolems, new_skolem_var_count)) proof axioms |
|
100 and used = map_filter (used_axioms axioms) proof |
98 and used = map_filter (used_axioms axioms) proof |
101 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") |
99 val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") |
102 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
100 val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
103 val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => |
101 val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => |
104 if have_common_thm used cls then NONE else SOME name) |
102 if have_common_thm used cls then NONE else SOME name) |