1 (******************************************************************************)
2 (* FILE : waterfall.ml *)
3 (* DESCRIPTION : `Waterfall' of heuristics. Clauses pour over. *)
4 (* Some evaporate. Others collect in a pool to be cleaned up. *)
5 (* Heuristics that act on a clause send the new clauses to *)
6 (* the top of the waterfall. *)
8 (* READS FILES : <none> *)
9 (* WRITES FILES : <none> *)
11 (* AUTHOR : R.J.Boulton *)
12 (* DATE : 9th May 1991 *)
14 (* LAST MODIFIED : R.J.Boulton *)
15 (* DATE : 12th August 1992 *)
17 (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
18 (* DATE : July 2009 *)
19 (******************************************************************************)
21 (*============================================================================*)
22 (* Some auxiliary functions *)
23 (*============================================================================*)
26 (*----------------------------------------------------------------------------*)
27 (* proves : thm -> term -> bool *)
29 (* Returns true if and only if the theorem proves the term without making any *)
31 (*----------------------------------------------------------------------------*)
34 (let (hyp,concl) = dest_thm th
35 in (hyp = []) & (concl = tm));;
37 (*----------------------------------------------------------------------------*)
38 (* apply_proof : proof -> term list -> proof *)
40 (* Converts a proof into a new proof that checks that the theorems it is *)
41 (* given have no hypotheses and have conclusions equal to the specified *)
42 (* terms. Used to make a proof robust. *)
43 (*----------------------------------------------------------------------------*)
45 let apply_proof f tms ths =
47 (if (itlist (fun (tm,th) b -> (proves th tm) & b) (List.combine tms ths) true)
50 ) with Failure _ -> failwith "apply_proof";;
52 (*============================================================================*)
53 (* The `waterfall' for heuristics *)
54 (*============================================================================*)
56 (*----------------------------------------------------------------------------*)
57 (* proof_printing : bool *)
59 (* Assignable variable. If true, clauses are printed as they are `poured' *)
60 (* over the waterfall. *)
61 (*----------------------------------------------------------------------------*)
63 let proof_printing = ref false;;
65 (*----------------------------------------------------------------------------*)
66 (* proof_printer : bool -> bool *)
68 (* Function for setting the flag that controls the printing of clauses as *)
69 (* are `poured' over the waterfall. *)
70 (*----------------------------------------------------------------------------*)
72 let proof_printer state =
73 let old_state = !proof_printing
74 in proof_printing := state; old_state;;
76 (*----------------------------------------------------------------------------*)
77 (* proof_print_depth : int *)
79 (* Assignable variable. A number indicating the `depth' of the proof and more *)
80 (* practically the number of spaces printed before a term. *)
81 (*----------------------------------------------------------------------------*)
83 let proof_print_depth = ref 0;;
85 (*----------------------------------------------------------------------------*)
86 (* inc_print_depth : * -> * *)
88 (* Identity function that has the side-effect of incrementing the *)
89 (* print_proof_depth. *)
90 (*----------------------------------------------------------------------------*)
92 let inc_print_depth x = (proof_print_depth := !proof_print_depth + 1; x);;
94 (*----------------------------------------------------------------------------*)
95 (* dec_print_depth : * -> * *)
97 (* Identity function that has the side-effect of decrementing the *)
98 (* print_proof_depth. *)
99 (*----------------------------------------------------------------------------*)
101 let dec_print_depth x =
102 if (!proof_print_depth < 1)
103 then (proof_print_depth := 0; x)
104 else (proof_print_depth := !proof_print_depth - 1; x);;
106 (*----------------------------------------------------------------------------*)
107 (* proof_print_term : term -> term *)
109 (* Identity function on terms that has the side effect of printing the term *)
110 (* if the `proof_printing' flag is set to true. *)
111 (*----------------------------------------------------------------------------*)
113 let proof_print_term tm =
115 then (print_string (implode (replicate " " !proof_print_depth));
116 print_term tm; print_newline () ; tm)
119 let proof_print_thm thm =
121 then ( print_thm thm; print_newline (); print_newline());;
123 let proof_print_tmi (tm,i) =
125 then ( proof_print_term tm; print_string " ("; print_bool i; print_string ")"; (tm,i) )
130 let proof_print_clause cl =
134 | Clause_proved thm -> (print_thm thm; print_newline (); cl)
139 (*----------------------------------------------------------------------------*)
140 (* proof_print_newline : * -> * *)
142 (* Identity function that has the side effect of printing a newline if the *)
143 (* `proof_printing' flag is set to true. *)
144 (*----------------------------------------------------------------------------*)
146 let proof_print_newline x =
148 then (print_newline (); x)
151 let proof_print_string s x =
153 then (print_string s; x)
156 let proof_print_string_l s x =
158 then (print_string s; print_newline (); x)
161 (*----------------------------------------------------------------------------*)
162 (* Recursive type for holding partly processed clauses. *)
164 (* A clause is either still to be proved, has been proved, or can be proved *)
165 (* once sub-clauses have been. A clause that is still to be proved carries a *)
166 (* flag indicating whether or not it is an induction step. *)
167 (*----------------------------------------------------------------------------*)
169 type clause_tree = Clause of (term * bool)
170 | Clause_proved of thm
171 | Clause_split of clause_tree list * (thm list -> thm);;
173 let rec proof_print_clausetree cl =
175 then ( proof_print_string_l "Clause tree:" (); match cl with
176 | Clause (tm,bool) -> (print_term tm; print_newline ())
177 | Clause_proved thm -> (print_thm thm; print_newline())
178 | Clause_split (tlist,proof) -> (print_string "Split -> "; print_int (length tlist); print_newline () ;
179 let void = map proof_print_clausetree tlist in () ));;
181 (*----------------------------------------------------------------------------*)
182 (* waterfall : ((term # bool) -> ((term # bool) list # proof)) list -> *)
183 (* (term # bool) -> *)
186 (* `Waterfall' of heuristics. Takes a list of heuristics and a term as *)
187 (* arguments. Each heuristic should fail if it can do nothing with its input. *)
188 (* Otherwise the heuristic should return a list of new clauses to be proved *)
189 (* together with a proof of the original clause from these new clauses. *)
191 (* Clauses that are not processed by any of the heuristics are placed in a *)
192 (* leaf node of the tree, to be proved later. The heuristics are attempted in *)
193 (* turn. If a heuristic returns an empty list of new clauses, the proof is *)
194 (* applied to an empty list, and the resultant theorem is placed in the tree *)
195 (* as a leaf node. Otherwise, the tree is split, and each of the new clauses *)
196 (* is passed to ALL of the heuristics. *)
197 (*----------------------------------------------------------------------------*)
199 let nth_tail n l = if (n > length l) then []
200 else let rec repeattl l i =
202 else tl (repeattl l (i-1))
206 let rec waterfall heuristics tmi =
207 bm_steps := hashI ((+) 1) !bm_steps;
208 let rec flow_on_down rest_of_heuristics tmi =
209 if (is_F (fst tmi)) then (failwith "cannot prove")
210 else if (rest_of_heuristics = []) then (Clause tmi)
211 else try ((let (tms,f) = hd rest_of_heuristics tmi
212 in if (tms = []) then (proof_print_string "Proven:" (); proof_print_thm (f []) ; Clause_proved (f []))
213 else if ((tl tms) = []) then
214 (Clause_split ([waterfall heuristics (hd tms)],f))
217 map (waterfall heuristics o proof_print_newline) o
218 inc_print_depth) tms,
220 )with Failure s -> (if (s = "cannot prove")
222 else (flow_on_down (tl rest_of_heuristics) tmi)
224 in flow_on_down heuristics (proof_print_tmi tmi);;
227 let rec filtered_waterfall heuristics warehouse tmi =
228 bm_steps := hashI ((+) 1) !bm_steps;
229 if (max_var_depth (fst tmi) > 12) then let void = (warn true "Reached maximum depth!") in failwith "cannot prove"
231 let heurn = try (assoc (fst tmi) warehouse) with Failure _ -> 0 in
232 let warehouse = (if (heurn > 0) then
233 let void = proof_print_string ("Warehouse kicking in! Skipping " ^ string_of_int(heurn) ^ " heuristic(s)") () ; in
234 let void = proof_print_newline () in
235 (List.remove_assoc (fst tmi) warehouse) else (warehouse)) in
236 let rec flow_on_down rest_of_heuristics tmi it =
237 if (is_F (fst tmi)) then (failwith "cannot prove")
238 else let rest_of_heuristics = nth_tail heurn rest_of_heuristics in
239 if (rest_of_heuristics = []) then (Clause tmi)
240 else try (let (tms,f) = hd rest_of_heuristics tmi
241 in if (tms = []) then (proof_print_string "Proven:" (); proof_print_thm (f []) ; Clause_proved (f []))
242 else if ((tl tms) = []) then Clause_split ([filtered_waterfall heuristics (((fst tmi),it)::warehouse) (hd tms)],f)
245 map (filtered_waterfall heuristics (((fst tmi),it)::warehouse) o proof_print_newline) o
246 inc_print_depth) tms,
249 if (s = "cannot prove")
251 else (flow_on_down (tl rest_of_heuristics) tmi (it+1))
253 in flow_on_down heuristics ((hashI proof_print_term) tmi) 1;;
256 let fringe = fringe_of_clause_tree restree in
257 if (fringe = []) then restree
258 else ( waterfall_warehouse := ((fst tmi),it)::(!waterfall_warehouse) ; restree ) *)
261 (*----------------------------------------------------------------------------*)
262 (* fringe_of_clause_tree : clause_tree -> (term # bool) list *)
264 (* Computes the fringe of a clause_tree, including in the resultant list only *)
265 (* those clauses that remain to be proved. *)
266 (*----------------------------------------------------------------------------*)
268 let rec fringe_of_clause_tree tree =
270 | (Clause tmi) -> [tmi]
271 | (Clause_proved _) -> []
272 | (Clause_split (trees,_)) -> (flat (map fringe_of_clause_tree trees));;
274 (*----------------------------------------------------------------------------*)
275 (* prove_clause_tree : clause_tree -> proof *)
277 (* Given a clause_tree, returns a proof that if given theorems for the *)
278 (* unproved clauses in the tree, returns a theorem for the clause at the root *)
279 (* of the tree. The list of theorems must be in the same order as the clauses *)
280 (* appear in the fringe of the tree. *)
281 (*----------------------------------------------------------------------------*)
283 let prove_clause_tree tree ths =
285 let rec prove_clause_trees trees ths =
286 if (trees = []) then ([],ths)
287 else let (th,ths') = prove_clause_tree' (hd trees) ths
288 in let (thl,ths'') = prove_clause_trees (tl trees) ths'
290 and prove_clause_tree' tree ths =
296 else failwith "prove_clause_tree")
297 | (Clause_proved th) -> (th,ths)
298 | (Clause_split (trees,f)) ->
299 (let (thl,ths') = prove_clause_trees trees ths
301 in (let (th,[]) = (prove_clause_tree' tree ths) in th)
302 ) with Failure _ -> failwith "prove_clause_tree";;
304 (*============================================================================*)
305 (* Eliminating instances in the `pool' of clauses remaining to be proved *)
307 (* Constructing partial orderings is probably overkill. It may only be *)
308 (* necessary to split the clauses into two sets, one of most general clauses *)
309 (* and the rest. This would still be computationally intensive, but it would *)
310 (* avoid comparing two clauses that are both instances of some other clause. *)
311 (*============================================================================*)
313 (*----------------------------------------------------------------------------*)
314 (* inst_of : term -> term -> thm -> thm *)
316 (* Takes two terms and computes whether the first is an instance of the *)
317 (* second. If this is the case, a proof of the first term from the second *)
318 (* (assuming they are formulae) is returned. Otherwise the function fails. *)
319 (*----------------------------------------------------------------------------*)
321 let inst_of tm patt =
323 (let (_,tm_bind,ty_bind) = term_match [] patt tm
324 in let (insts,vars) = List.split tm_bind
325 in let f = (SPECL insts) o (GENL vars) o (INST_TYPE ty_bind)
326 in fun th -> apply_proof (f o hd) [patt] [th]
327 )) with Failure _ -> failwith "inst_of";;
329 (*----------------------------------------------------------------------------*)
330 (* Recursive datatype for a partial ordering of terms using the *)
331 (* `is an instance of' relation. *)let proof_print_thm thm =
333 then ( print_thm thm; print_newline (); print_newline());;
336 (* The leaf nodes of the tree are terms that have no instances. The other *)
337 (* nodes have a list of instance trees and proofs of each instance from the *)
338 (* term at that node. *)
340 (* Each term carries a number along with it. This is used to keep track of *)
341 (* where the term came from in a list. The idea is to take the fringe of a *)
342 (* clause tree, number the elements, then form partial orderings so that *)
343 (* only the most general theorems have to be proved. *)
344 (*----------------------------------------------------------------------------*)
346 type inst_tree = No_insts of (term * int)
347 | Insts of (term * int * (inst_tree * (thm -> thm)) list);;
349 (*----------------------------------------------------------------------------*)
350 (* insert_into_inst_tree : (term # int) -> inst_tree -> inst_tree *)
351 (* insert_into_inst_trees : (term # int # (thm -> thm)) -> *)
352 (* (inst_tree # (thm -> thm)) list -> *)
353 (* (inst_tree # (thm -> thm)) list *)
355 (* Mutually recursive functions for constructing partial orderings, ordered *)
356 (* by `is an instance of' relation. The algorithm is grossly inefficient. *)
357 (* Structures are repeatedly destroyed and rebuilt. Reference variables *)
358 (* should be used for efficiency. *)
360 (* Inserting into a single tree: *)
362 (* If tm' is an instance of tm, tm is put in the root node, with the old tree *)
363 (* as its single child. If tm is not an instance of tm', the function fails. *)
364 (* Assume now that tm is an instance of tm'. If the tree is a leaf, it is *)
365 (* made into a branch and tm is inserted as the one and only child. If the *)
366 (* tree is a branch, an attempt is made to insert tm in the list of *)
367 (* sub-trees. If this fails, tm is added as a leaf to the list of instances. *)
368 (* Note that if tm is not an instance of tm', then it cannot be an instance *)
369 (* of the instances of tm'. *)
371 (* Inserting into a list of trees: *)
373 (* The list of trees carry proofs with them. The list is split into those *)
374 (* whose root is an instance of tm, and those whose root is not. The proof *)
375 (* associated with a tree that is an instance is replaced by a proof of the *)
376 (* term from tm. If the list of trees that are instances is non-empty, they *)
377 (* are made children of a node containing tm, and this new tree is added to *)
378 (* the list of trees that are n't instances. If tm has instances in the list, *)
379 (* it cannot be the case that tm is an instance of one of the other trees in *)
380 (* the list, for the trees in a list must be unrelated. *)
382 (* If there are no instances of tm in the list of trees, an attempt is made *)
383 (* to insert tm into the list. If it is unrelated to all of the trees, this *)
384 (* attempt fails, in which case tm is made into a leaf and added to the list. *)
385 (*----------------------------------------------------------------------------*)
387 let rec insert_into_inst_tree (tm,n) tree =
389 | (No_insts (tm',n')) ->
390 (try ( (let f = inst_of tm' tm
391 in Insts (tm,n,[No_insts (tm',n'),f]))
392 ) with Failure _ -> try( let f = inst_of tm tm'
393 in Insts (tm',n',[No_insts (tm,n),f])) with Failure _ -> failwith "insert_into_inst_tree"
395 | (Insts (tm',n',insts)) ->
396 (try (let f = inst_of tm' tm
397 in Insts (tm,n,[Insts (tm',n',insts),f]))
398 with Failure _ -> try(let f = inst_of tm tm'
399 in try( Insts (tm',n',insert_into_inst_trees (tm,n,f) insts))
400 with Failure _ -> (Insts (tm',n',(No_insts (tm,n),f)::insts))
402 with Failure _ -> failwith "insert_into_inst_tree" )
403 and insert_into_inst_trees (tm,n,f) insts =
404 let rec instances (tm,n) insts =
407 else let (not_instl,instl) = instances (tm,n) (tl insts)
411 | (No_insts (tm',n')) -> (tm',n')
412 | (Insts (tm',n',_)) -> (tm',n')
413 in (try( (let f' = inst_of tm' tm
414 in (not_instl,(h,f')::instl))
415 ) with Failure _ -> ((h,f)::not_instl,instl)
417 and insert_into_inst_trees' (tm,n) trees =
419 then failwith "insert_into_inst_trees'"
420 else (try( ((insert_into_inst_tree (tm,n) (hd trees))::(tl trees))
421 ) with Failure _ -> ((hd trees)::(insert_into_inst_trees' (tm,n) (tl trees)))
423 in let (not_instl,instl) = instances (tm,n) insts
425 then try( (lcombinep o (hashI (insert_into_inst_trees' (tm,n)))) (List.split insts)
426 ) with Failure _ -> ((No_insts (tm,n),f)::insts)
427 else (Insts (tm,n,instl),f)::not_instl;;
429 (*----------------------------------------------------------------------------*)
430 (* mk_inst_trees : (term # int) list -> inst_tree list *)
432 (* Constructs a partial ordering of terms under the `is an instance of' *)
433 (* relation from a list of numbered terms. *)
435 (* A dummy proof is passed to the call of insert_into_inst_trees. The result *)
436 (* of the call has a proof associated with the root of each tree. These *)
437 (* proofs are dummies and so are discarded before the final result is *)
439 (*----------------------------------------------------------------------------*)
441 let mk_inst_trees tmnl =
442 let rec mk_inst_trees' insts tmnl =
445 else let (tm,n) = hd tmnl
447 (insert_into_inst_trees (tm,n,I) insts) (tl tmnl)
448 in map fst (mk_inst_trees' [] tmnl);;
450 (*----------------------------------------------------------------------------*)
451 (* roots_of_inst_trees : inst_tree list -> term list *)
453 (* Computes the terms at the roots of a list of partial orderings. *)
454 (*----------------------------------------------------------------------------*)
456 let rec roots_of_inst_trees trees =
460 match (hd trees) with
461 | (No_insts (tm,_)) -> tm
462 | (Insts (tm,_,_)) -> tm
463 in tm::(roots_of_inst_trees (tl trees));;
465 (*----------------------------------------------------------------------------*)
466 (* prove_inst_tree : inst_tree -> thm -> (thm # int) list *)
468 (* Given a partial ordering of terms and a theorem for its root, returns a *)
469 (* list of theorems for the terms in the tree. *)
470 (*----------------------------------------------------------------------------*)
472 let rec prove_inst_tree tree th =
474 | (No_insts (tm,n)) ->
475 (if (proves th tm) then [(th,n)] else failwith "prove_inst_tree")
476 | (Insts (tm,n,insts)) ->
478 then (th,n)::(flat (map (fun (tr,f) -> prove_inst_tree tr (f th)) insts))
479 else failwith "prove_inst_tree");;
481 (*----------------------------------------------------------------------------*)
482 (* prove_inst_trees : inst_tree list -> thm list -> thm list *)
484 (* Given a list of partial orderings of terms and a list of theorems for *)
485 (* their roots, returns a sorted list of theorems for the terms in the trees. *)
486 (* The sorting is done based on the integer labels attached to each term in *)
488 (*----------------------------------------------------------------------------*)
490 let prove_inst_trees trees ths =
492 (sort_on_snd (flat (map (uncurry prove_inst_tree) (lcombinep (trees,ths)))))
493 ) with Failure _ -> failwith "prove_inst_trees";;
495 (*----------------------------------------------------------------------------*)
496 (* prove_pool : conv -> term list -> thm list *)
498 (* Attempts to prove the pool of clauses left over from the waterfall, by *)
499 (* applying the conversion, conv, to the most general clauses. *)
500 (*----------------------------------------------------------------------------*)
502 let prove_pool conv tml =
503 let tmnl = number_list tml
504 in let trees = mk_inst_trees tmnl
505 in let most_gen_terms = roots_of_inst_trees trees
506 in let ths = map conv most_gen_terms
507 in prove_inst_trees trees ths;;
509 (*============================================================================*)
510 (* Boyer-Moore prover *)
511 (*============================================================================*)
513 (*----------------------------------------------------------------------------*)
514 (* WATERFALL : ((term # bool) -> ((term # bool) list # proof)) list -> *)
515 (* ((term # bool) -> ((term # bool) list # proof)) -> *)
516 (* (term # bool) -> *)
519 (* Boyer-Moore style automatic proof procedure. Takes a list of heuristics, *)
520 (* and a single heuristic that does induction, as arguments. The result is a *)
521 (* function that, given a term and a Boolean, attempts to prove the term. The *)
522 (* Boolean is used to indicate whether the term is the step of an induction. *)
523 (* It will normally be set to false for an external call. *)
524 (*----------------------------------------------------------------------------*)
526 let rec WATERFALL heuristics induction (tm,(ind:bool)) =
528 proof_print_string "Doing induction on:" () ; bm_steps := hash ((+) 1) ((+) 1) !bm_steps ;
529 let void = proof_print_term tm ; proof_print_newline ()
530 in let (tmil,proof) = induction (tm,false)
533 (map (WATERFALL heuristics induction) (inc_print_depth tmil)))
534 in let void = proof_print_newline ()
535 in let tree = waterfall heuristics (tm,ind)
536 in let tmil = fringe_of_clause_tree tree
537 in let thl = prove_pool conv (map fst tmil)
538 in prove_clause_tree tree thl;;
541 let rec FILTERED_WATERFALL heuristics induction warehouse (tm,(ind:bool)) =
543 (* let constr_check = ind && not((find_bm_terms (fun t -> count_constructors t > 5) tm) = []) in *)
544 let constr_check = (max_var_depth tm > 12) in
545 if (constr_check) then let void = (warn true "Reached maximum depth!") in failwith "cannot prove"
547 let heurn = try (assoc tm warehouse) with Failure _ -> 0 in
548 let warehouse = (if (heurn > 0) then (List.remove_assoc tm warehouse) else (warehouse)) in
549 if (heurn > length heuristics) then ( warn true "Induction loop detected."; failwith "cannot prove" )
551 proof_print_string "Doing induction on:" (); bm_steps := hash ((+) 1) ((+) 1) !bm_steps ;
552 let void = proof_print_term tm ; proof_print_newline () in
553 let (tmil,proof) = induction (tm,false)
556 (map (FILTERED_WATERFALL heuristics induction ((tm,(length heuristics) + 1)::warehouse)) (inc_print_depth tmil)))
557 in let void = proof_print_newline ()
558 in let tree = filtered_waterfall heuristics [] (tm,ind)
559 (* in let void = proof_print_clausetree tree *)
560 in let tmil = fringe_of_clause_tree tree
561 in let thl = prove_pool conv (map fst tmil)
562 in prove_clause_tree tree thl;;
564 (*============================================================================*)
565 (* Some sample heuristics *)
566 (*============================================================================*)
568 (*----------------------------------------------------------------------------*)
569 (* conjuncts_heuristic : (term # bool) -> ((term # bool) list # proof) *)
571 (* `Heuristic' for splitting a conjunction into a list of conjuncts. *)
572 (* Right conjuncts are split recursively. *)
573 (* Fails if the argument term is not a conjunction. *)
574 (*----------------------------------------------------------------------------*)
576 let conjuncts_heuristic (tm,(i:bool)) =
577 let tms = conj_list tm
578 in if (length tms = 1)
579 then failwith "conjuncts_heuristic"
580 else (map (fun tm -> (tm,i)) tms,apply_proof LIST_CONJ tms);;
582 (*----------------------------------------------------------------------------*)
583 (* refl_heuristic : (term # bool) -> ((term # bool) list # proof) *)
585 (* `Heuristic' for proving that terms of the form "x = x" are true. Fails if *)
586 (* the argument term is not of this form. Otherwise it returns an empty list *)
587 (* of new clauses, and a proof of the original term. *)
588 (*----------------------------------------------------------------------------*)
590 let refl_heuristic (tm,(i:bool)) =
591 try(if (lhs tm = rhs tm)
592 then (([]:(term * bool) list),apply_proof (fun ths -> REFL (lhs tm)) [])
594 ) with Failure _ -> failwith "refl_heuristic";;
596 (*----------------------------------------------------------------------------*)
597 (* clausal_form_heuristic : (term # bool) -> ((term # bool) list # proof) *)
599 (* `Heuristic' that tests a term to see if it is in clausal form, and if not *)
600 (* converts it to clausal form and returns the resulting clauses as new *)
601 (* `goals'. It is critical for efficiency that the normalization is only done *)
602 (* if the term is not in clausal form. Note that the functions `conjuncts' *)
603 (* and `disjuncts' are not used for the testing because they split trees of *)
604 (* conjuncts (disjuncts) rather than simply `linear' con(dis)junctions. *)
605 (* If the term is in clausal form, but is not a single clause, it is split *)
606 (* into single clauses. If the term is in clausal form but contains Boolean *)
607 (* constants, the normalizer is applied to it. A single new goal will be *)
608 (* produced in this case unless the result of the normalization was true. *)
609 (*----------------------------------------------------------------------------*)
611 let clausal_form_heuristic (tm,(i:bool)) =
612 try (let is_atom tm =
613 (not (has_boolean_args_and_result tm)) or (is_var tm) or (is_const tm)
614 in let is_literal tm =
615 (is_atom tm) or ((is_neg tm) & (try (is_atom (rand tm)) with Failure _ -> false))
616 in let is_clause tm = forall is_literal (disj_list tm)
617 in let result_string = fun tms -> let s = length tms
618 in let plural = if (s=1) then "" else "s"
619 in ("-> Clausal Form Heuristic (" ^ string_of_int(s) ^ " clause" ^ plural ^ ")")
620 in if (forall is_clause (conj_list tm)) &
621 (not (free_in `T` tm)) & (not (free_in `F` tm))
623 then let tms = conj_list tm
624 in (proof_print_string_l (result_string tms) () ;
625 (map (fun tm -> (tm,i)) tms,apply_proof LIST_CONJ tms))
627 else let th = CLAUSAL_FORM_CONV tm
628 in let tm' = rhs (concl th)
630 then (proof_print_string_l "-> Clausal Form Heuristic" () ; ([],apply_proof (fun _ -> EQT_ELIM th) []))
631 else let tms = conj_list tm'
632 in (proof_print_string_l (result_string tms) () ;
633 (map (fun tm -> (tm,i)) tms,
634 apply_proof ((EQ_MP (SYM th)) o LIST_CONJ) tms))
635 ) with Failure _ -> failwith "clausal_form_heuristic";;
637 let meson_heuristic (tm,(i:bool)) =
638 try( let meth = MESON (rewrite_rules()) tm in
639 (([]:(term * bool) list),apply_proof (fun ths -> meth) [])
640 ) with Failure _ -> failwith "meson_heuristic";;
642 let taut_heuristic (tm,(i:bool)) =
643 try( let tautthm = TAUT tm in (proof_print_string_l "-> Tautology Heuristic" () ;
644 (([]:(term * bool) list),apply_proof (fun ths -> tautthm) []))
645 ) with Failure _ -> failwith "taut_heuristic";;
647 let setify_heuristic (tm,(i:bool)) =
649 if (not (is_disj tm)) then failwith ""
651 let tms = disj_list tm
652 in let tms' = setify tms
653 in let tm' = list_mk_disj tms'
654 in if ((length tms) = (length tms')) then failwith ""
655 else let th = TAUT (mk_imp (tm',tm))
656 in (proof_print_string_l "-> Setify Heuristic" () ;
657 ([tm',i],apply_proof ((MP th) o hd) [tm']))
659 with Failure _ -> failwith "setify_heuristic";;