author | paulson |
Wed, 21 Dec 2005 12:06:08 +0100 | |
changeset 18449 | e314fb38307d |
parent 18420 | 9470061ab283 |
child 18509 | d2d96f12a1fc |
permissions | -rw-r--r-- |
16795 | 1 |
(* ID: $Id$ |
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
2 |
Author: Claire Quigley |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
3 |
Copyright 2004 University of Cambridge |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
4 |
*) |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15782
diff
changeset
|
5 |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
6 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
7 |
structure ReduceAxiomsN = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
8 |
(* Author: Jia Meng, Cambridge University Computer Laboratory |
17234 | 9 |
Remove irrelevant axioms used for a proof of a goal, with with iteration control |
10 |
||
11 |
Initial version. Needs elaboration. *) |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
12 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
13 |
struct |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
14 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
15 |
fun add_term_consts_rm ncs (Const(c, _)) cs = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
16 |
if (c mem ncs) then cs else (c ins_string cs) |
16795 | 17 |
| add_term_consts_rm ncs (t $ u) cs = |
18 |
add_term_consts_rm ncs t (add_term_consts_rm ncs u cs) |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
19 |
| add_term_consts_rm ncs (Abs(_,_,t)) cs = add_term_consts_rm ncs t cs |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
20 |
| add_term_consts_rm ncs _ cs = cs; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
21 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
22 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
23 |
fun term_consts_rm ncs t = add_term_consts_rm ncs t []; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
24 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
25 |
fun thm_consts_rm ncs thm = term_consts_rm ncs (prop_of thm); |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
26 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
27 |
fun consts_of_thm (n,thm) = thm_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] thm; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
28 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
29 |
fun consts_of_term term = term_consts_rm ["Trueprop","==>","all","Ex","op &", "op |", "Not", "All", "op -->", "op =", "==", "True", "False"] term; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
30 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
31 |
fun make_pairs [] _ = [] |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
32 |
| make_pairs (x::xs) y = (x,y)::(make_pairs xs y); |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
33 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
34 |
fun const_thm_list_aux [] cthms = cthms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
35 |
| const_thm_list_aux (thm::thms) cthms = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
36 |
let val consts = consts_of_thm thm |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
37 |
val cthms' = make_pairs consts thm |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
38 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
39 |
const_thm_list_aux thms (cthms' @ cthms) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
40 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
41 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
42 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
43 |
fun const_thm_list thms = const_thm_list_aux thms []; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
44 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
45 |
fun make_thm_table thms = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
46 |
let val consts_thms = const_thm_list thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
47 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
48 |
Symtab.make_multi consts_thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
49 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
50 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
51 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
52 |
fun consts_in_goal goal = consts_of_term goal; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
53 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
54 |
fun axioms_having_consts_aux [] tab thms = thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
55 |
| axioms_having_consts_aux (c::cs) tab thms = |
17412 | 56 |
let val thms1 = Symtab.lookup tab c |
17261 | 57 |
val thms2 = |
58 |
case thms1 of (SOME x) => x |
|
59 |
| NONE => [] |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
60 |
in |
17261 | 61 |
axioms_having_consts_aux cs tab (thms2 union thms) |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
62 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
63 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
64 |
fun axioms_having_consts cs tab = axioms_having_consts_aux cs tab []; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
65 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
66 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
67 |
fun relevant_axioms goal thmTab n = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
68 |
let val consts = consts_in_goal goal |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
69 |
fun relevant_axioms_aux1 cs k = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
70 |
let val thms1 = axioms_having_consts cs thmTab |
17764 | 71 |
val cs1 = foldl (op union_string) [] (map consts_of_thm thms1) |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
72 |
in |
16795 | 73 |
if ((cs1 subset cs) orelse n <= k) then (k,thms1) |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
74 |
else (relevant_axioms_aux1 (cs1 union cs) (k+1)) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
75 |
end |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
76 |
|
16795 | 77 |
in relevant_axioms_aux1 consts 1 end; |
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
78 |
|
16795 | 79 |
fun relevant_filter n goal thms = |
80 |
if n<=0 then thms |
|
81 |
else #2 (relevant_axioms goal (make_thm_table thms) n); |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
82 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
83 |
(* find the thms from thy that contain relevant constants, n is the iteration number *) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
84 |
fun find_axioms_n thy goal n = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
85 |
let val clasetR = ResAxioms.claset_rules_of_thy thy |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
86 |
val simpsetR = ResAxioms.simpset_rules_of_thy thy |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
87 |
val table = make_thm_table (clasetR @ simpsetR) |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
88 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
89 |
relevant_axioms goal table n |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
90 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
91 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
92 |
fun find_axioms_n_c thy goal n = |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
93 |
let val current_thms = PureThy.thms_of thy |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
94 |
val table = make_thm_table current_thms |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
95 |
in |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
96 |
relevant_axioms goal table n |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
97 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
98 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
99 |
end; |
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
100 |
|
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
101 |
|
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
102 |
signature RES_CLASIMP = |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
103 |
sig |
16795 | 104 |
val relevant : int ref |
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
105 |
val use_simpset: bool ref |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
106 |
val get_clasimp_lemmas : |
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
107 |
Proof.context -> term -> |
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
108 |
(ResClause.clause * thm) Array.array * ResClause.clause list |
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
109 |
end; |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
110 |
|
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
111 |
structure ResClasimp : RES_CLASIMP = |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
112 |
struct |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
113 |
val use_simpset = ref false; (*Performance is much better without simprules*) |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
114 |
|
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
115 |
val relevant = ref 0; (*Relevance filtering is off by default*) |
16795 | 116 |
|
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
117 |
(*The "name" of a theorem is its statement, if nothing else is available.*) |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
118 |
val plain_string_of_thm = |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
119 |
setmp show_question_marks false |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
120 |
(setmp print_mode [] |
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
121 |
(Pretty.setmp_margin 999 string_of_thm)); |
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
122 |
|
17828 | 123 |
(*Returns the first substring enclosed in quotation marks, typically omitting |
124 |
the [.] of meta-level assumptions.*) |
|
125 |
val firstquoted = hd o (String.tokens (fn c => c = #"\"")) |
|
126 |
||
16957
8dcd14e8db7a
nameless theorems: better names, flag to omit them
paulson
parents:
16956
diff
changeset
|
127 |
fun fake_thm_name th = |
17828 | 128 |
Context.theory_name (theory_of_thm th) ^ "." ^ firstquoted (plain_string_of_thm th); |
16061 | 129 |
|
17828 | 130 |
fun put_name_pair ("",th) = (fake_thm_name th, th) |
16956
5b413c866593
invents theorem names; also patches write_out_clasimp
paulson
parents:
16950
diff
changeset
|
131 |
| put_name_pair (a,th) = (a,th); |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
132 |
|
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
133 |
(* outputs a list of (thm,clause) pairs *) |
15643 | 134 |
|
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
135 |
fun multi x 0 xlist = xlist |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
136 |
|multi x n xlist = multi x (n-1) (x::xlist); |
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
137 |
|
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
138 |
fun clause_numbering ((clause, theorem), num_of_cls) = |
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
139 |
let val numbers = 0 upto (num_of_cls - 1) |
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset
|
140 |
in |
17305
6cef3aedd661
axioms now included in tptp files, no /bin/cat and various tidying
paulson
parents:
17261
diff
changeset
|
141 |
multi (clause, theorem) num_of_cls [] |
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset
|
142 |
end; |
17234 | 143 |
|
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
144 |
(*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
145 |
Some primes from http://primes.utm.edu/: |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
146 |
*) |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
147 |
|
18449 | 148 |
exception HASH_CLAUSE and HASH_STRING; |
149 |
||
150 |
(*Catches (for deletion) theorems automatically generated from other theorems*) |
|
151 |
fun insert_suffixed_names ht x = |
|
152 |
(Polyhash.insert ht (x^"_iff1", ()); |
|
153 |
Polyhash.insert ht (x^"_iff2", ()); |
|
154 |
Polyhash.insert ht (x^"_dest", ())); |
|
155 |
||
156 |
fun make_suffix_test xs = |
|
157 |
let val ht = Polyhash.mkTable (Polyhash.hash_string, op =) |
|
158 |
(6000, HASH_STRING) |
|
159 |
fun suffixed s = isSome (Polyhash.peek ht s) |
|
160 |
in app (insert_suffixed_names ht) xs; suffixed end; |
|
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
161 |
|
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
162 |
(*Create a hash table for clauses, of the given size*) |
18449 | 163 |
fun mk_clause_table n = |
164 |
Polyhash.mkTable (ResClause.hash_clause, ResClause.clause_eq) |
|
165 |
(n, HASH_CLAUSE); |
|
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
166 |
|
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
167 |
(*Use a hash table to eliminate duplicates from xs*) |
18449 | 168 |
fun make_unique ht xs = |
169 |
(app (ignore o Polyhash.peekInsert ht) xs; Polyhash.listItems ht); |
|
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
170 |
|
16741
7a6c17b826c0
inserted basic relevance-checking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
paulson
parents:
16357
diff
changeset
|
171 |
(*Write out the claset and simpset rules of the supplied theory. |
16906 | 172 |
FIXME: argument "goal" is a hack to allow relevance filtering. |
173 |
To reduce the number of clauses produced, set ResClasimp.relevant:=1*) |
|
17484
f6a225f97f0a
simplification of the Isabelle-ATP code; hooks for batch generation of problems
paulson
parents:
17412
diff
changeset
|
174 |
fun get_clasimp_lemmas ctxt goal = |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
175 |
let val claset_thms = |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
176 |
map put_name_pair |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
177 |
(ReduceAxiomsN.relevant_filter (!relevant) goal |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
178 |
(ResAxioms.claset_rules_of_ctxt ctxt)) |
18449 | 179 |
val simpset_thms = |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
180 |
if !use_simpset then |
18449 | 181 |
map put_name_pair |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
182 |
(ReduceAxiomsN.relevant_filter (!relevant) goal |
18449 | 183 |
(ResAxioms.simpset_rules_of_ctxt ctxt)) |
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
184 |
else [] |
18449 | 185 |
val suffixed = make_suffix_test (map #1 (claset_thms@simpset_thms)) |
186 |
fun ok (a,_) = not (suffixed a) |
|
187 |
val claset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok claset_thms) |
|
188 |
val simpset_cls_thms = ResAxioms.clausify_rules_pairs (filter ok simpset_thms) |
|
189 |
val cls_thms_list = make_unique (mk_clause_table 2200) |
|
18420
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
190 |
(List.concat (simpset_cls_thms@claset_cls_thms)) |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
191 |
(* Identify the set of clauses to be written out *) |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
192 |
val clauses = map #1(cls_thms_list); |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
193 |
val cls_nums = map ResClause.num_of_clauses clauses; |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
194 |
(*Note: in every case, cls_num = 1. I think that only conjecture clauses |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
195 |
can have any other value.*) |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
196 |
val whole_list = List.concat |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
197 |
(map clause_numbering (ListPair.zip (cls_thms_list, cls_nums))); |
9470061ab283
hashing to eliminate the output of duplicate clauses
paulson
parents:
18144
diff
changeset
|
198 |
|
17828 | 199 |
in (* create array of put clausename, number pairs into it *) |
200 |
(Array.fromList whole_list, clauses) |
|
16061 | 201 |
end; |
15643 | 202 |
|
16950
e7f0f41d513a
Added flag ResClasimp.use_simpset to allow exclusion of simpset rules from ATP problem files
quigley
parents:
16906
diff
changeset
|
203 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15907
diff
changeset
|
204 |
end; |
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15956
diff
changeset
|
205 |
|
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
206 |
|
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16061
diff
changeset
|
207 |