118 | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses |
118 | shape_of_clauses j ([] :: clauses) = [] :: shape_of_clauses j clauses |
119 | shape_of_clauses j ((_ :: lits) :: clauses) = |
119 | shape_of_clauses j ((_ :: lits) :: clauses) = |
120 let val shape = shape_of_clauses (j + 1) (lits :: clauses) in |
120 let val shape = shape_of_clauses (j + 1) (lits :: clauses) in |
121 (j :: hd shape) :: tl shape |
121 (j :: hd shape) :: tl shape |
122 end |
122 end |
|
123 |
|
124 |
|
125 (* Clause preparation *) |
|
126 |
|
127 fun make_clause_table xs = |
|
128 fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty |
|
129 |
|
130 (* Remove existing axiom clauses from the conjecture clauses, as this can |
|
131 dramatically boost an ATP's performance (for some reason). *) |
|
132 fun subtract_cls ax_clauses = |
|
133 filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of) |
|
134 |
|
135 fun is_false_literal (Literal (pos, CombConst ((c, _), _, _))) = |
|
136 (pos andalso c = "c_False") orelse (not pos andalso c = "c_True") |
|
137 | is_false_literal _ = false |
|
138 fun is_true_literal (Literal (pol, CombConst ((c, _), _, _))) = |
|
139 (pol andalso c = "c_True") orelse |
|
140 (not pol andalso c = "c_False") |
|
141 | is_true_literal _ = false; |
|
142 fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals |
|
143 |
|
144 (* making axiom and conjecture clauses *) |
|
145 fun make_clause thy (clause_id, axiom_name, kind, th) skolem_somes = |
|
146 let |
|
147 val (skolem_somes, t) = |
|
148 th |> prop_of |> conceal_skolem_somes clause_id skolem_somes |
|
149 val (lits, ctypes_sorts) = literals_of_term thy t |
|
150 in |
|
151 if forall is_false_literal lits then |
|
152 raise TRIVIAL () |
|
153 else |
|
154 (skolem_somes, |
|
155 HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th, |
|
156 kind = kind, literals = lits, ctypes_sorts = ctypes_sorts}) |
|
157 end |
|
158 |
|
159 fun add_axiom_clause thy ((name, k), th) (skolem_somes, clss) = |
|
160 let |
|
161 val (skolem_somes, cls) = make_clause thy (k, name, Axiom, th) skolem_somes |
|
162 in (skolem_somes, clss |> not (is_tautology cls) ? cons (name, cls)) end |
|
163 |
|
164 fun make_axiom_clauses thy clauses = |
|
165 ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd |
|
166 |
|
167 fun make_conjecture_clauses thy = |
|
168 let |
|
169 fun aux _ _ [] = [] |
|
170 | aux n skolem_somes (th :: ths) = |
|
171 let |
|
172 val (skolem_somes, cls) = |
|
173 make_clause thy (n, "conjecture", Conjecture, th) skolem_somes |
|
174 in cls :: aux (n + 1) skolem_somes ths end |
|
175 in aux 0 [] end |
|
176 |
|
177 (** Helper clauses **) |
|
178 |
|
179 fun count_combterm (CombConst ((c, _), _, _)) = |
|
180 Symtab.map_entry c (Integer.add 1) |
|
181 | count_combterm (CombVar _) = I |
|
182 | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2 |
|
183 fun count_literal (Literal (_, t)) = count_combterm t |
|
184 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals |
|
185 |
|
186 fun cnf_helper_thms thy raw = |
|
187 map (`Thm.get_name_hint) |
|
188 #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy) |
|
189 |
|
190 val optional_helpers = |
|
191 [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})), |
|
192 (["c_COMBB", "c_COMBC"], (false, @{thms COMBB_def COMBC_def})), |
|
193 (["c_COMBS"], (false, @{thms COMBS_def}))] |
|
194 val optional_typed_helpers = |
|
195 [(["c_True", "c_False"], (true, @{thms True_or_False})), |
|
196 (["c_If"], (true, @{thms if_True if_False True_or_False}))] |
|
197 val mandatory_helpers = @{thms fequal_imp_equal equal_imp_fequal} |
|
198 |
|
199 val init_counters = |
|
200 Symtab.make (maps (maps (map (rpair 0) o fst)) |
|
201 [optional_helpers, optional_typed_helpers]) |
|
202 |
|
203 fun get_helper_clauses thy is_FO full_types conjectures axcls = |
|
204 let |
|
205 val axclauses = map snd (make_axiom_clauses thy axcls) |
|
206 val ct = fold (fold count_clause) [conjectures, axclauses] init_counters |
|
207 fun is_needed c = the (Symtab.lookup ct c) > 0 |
|
208 val cnfs = |
|
209 (optional_helpers |
|
210 |> full_types ? append optional_typed_helpers |
|
211 |> maps (fn (ss, (raw, ths)) => |
|
212 if exists is_needed ss then cnf_helper_thms thy raw ths |
|
213 else [])) |
|
214 @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers) |
|
215 in map snd (make_axiom_clauses thy cnfs) end |
|
216 |
|
217 (* prepare for passing to writer, |
|
218 create additional clauses based on the information from extra_cls *) |
|
219 fun prepare_clauses full_types goal_cls axcls extra_cls thy = |
|
220 let |
|
221 val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls |
|
222 val ccls = subtract_cls extra_cls goal_cls |
|
223 val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls |
|
224 val ccltms = map prop_of ccls |
|
225 and axtms = map (prop_of o snd) extra_cls |
|
226 val subs = tfree_classes_of_terms ccltms |
|
227 and supers = tvar_classes_of_terms axtms |
|
228 and tycons = type_consts_of_terms thy (ccltms @ axtms) |
|
229 (*TFrees in conjecture clauses; TVars in axiom clauses*) |
|
230 val conjectures = make_conjecture_clauses thy ccls |
|
231 val (_, extra_clauses) = ListPair.unzip (make_axiom_clauses thy extra_cls) |
|
232 val (clnames, axiom_clauses) = ListPair.unzip (make_axiom_clauses thy axcls) |
|
233 val helper_clauses = |
|
234 get_helper_clauses thy is_FO full_types conjectures extra_cls |
|
235 val (supers', arity_clauses) = make_arity_clauses thy tycons supers |
|
236 val classrel_clauses = make_classrel_clauses thy subs supers' |
|
237 in |
|
238 (Vector.fromList clnames, |
|
239 (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses)) |
|
240 end |
|
241 |
123 |
242 |
124 (* generic TPTP-based provers *) |
243 (* generic TPTP-based provers *) |
125 |
244 |
126 fun generic_tptp_prover |
245 fun generic_tptp_prover |
127 (name, {home_var, executable, arguments, proof_delims, known_failures, |
246 (name, {home_var, executable, arguments, proof_delims, known_failures, |