(******************************************************************************) (* FILE : waterfall.ml *) (* DESCRIPTION : `Waterfall' of heuristics. Clauses pour over. *) (* Some evaporate. Others collect in a pool to be cleaned up. *) (* Heuristics that act on a clause send the new clauses to *) (* the top of the waterfall. *) (* *) (* READS FILES : *) (* WRITES FILES : *) (* *) (* AUTHOR : R.J.Boulton *) (* DATE : 9th May 1991 *) (* *) (* LAST MODIFIED : R.J.Boulton *) (* DATE : 12th August 1992 *) (* *) (* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *) (* DATE : July 2009 *) (******************************************************************************) (*============================================================================*) (* Some auxiliary functions *) (*============================================================================*) (*----------------------------------------------------------------------------*) (* proves : thm -> term -> bool *) (* *) (* Returns true if and only if the theorem proves the term without making any *) (* assumptions. *) (*----------------------------------------------------------------------------*) let proves th tm = (let (hyp,concl) = dest_thm th in (hyp = []) & (concl = tm));; (*----------------------------------------------------------------------------*) (* apply_proof : proof -> term list -> proof *) (* *) (* Converts a proof into a new proof that checks that the theorems it is *) (* given have no hypotheses and have conclusions equal to the specified *) (* terms. Used to make a proof robust. *) (*----------------------------------------------------------------------------*) let apply_proof f tms ths = try (if (itlist (fun (tm,th) b -> (proves th tm) & b) (List.combine tms ths) true) then (f ths) else failwith "" ) with Failure _ -> failwith "apply_proof";; (*============================================================================*) (* The `waterfall' for heuristics *) (*============================================================================*) (*----------------------------------------------------------------------------*) (* proof_printing : bool *) (* *) (* Assignable variable. If true, clauses are printed as they are `poured' *) (* over the waterfall. *) (*----------------------------------------------------------------------------*) let proof_printing = ref false;; (*----------------------------------------------------------------------------*) (* proof_printer : bool -> bool *) (* *) (* Function for setting the flag that controls the printing of clauses as *) (* are `poured' over the waterfall. *) (*----------------------------------------------------------------------------*) let proof_printer state = let old_state = !proof_printing in proof_printing := state; old_state;; (*----------------------------------------------------------------------------*) (* proof_print_depth : int *) (* *) (* Assignable variable. A number indicating the `depth' of the proof and more *) (* practically the number of spaces printed before a term. *) (*----------------------------------------------------------------------------*) let proof_print_depth = ref 0;; (*----------------------------------------------------------------------------*) (* inc_print_depth : * -> * *) (* *) (* Identity function that has the side-effect of incrementing the *) (* print_proof_depth. *) (*----------------------------------------------------------------------------*) let inc_print_depth x = (proof_print_depth := !proof_print_depth + 1; x);; (*----------------------------------------------------------------------------*) (* dec_print_depth : * -> * *) (* *) (* Identity function that has the side-effect of decrementing the *) (* print_proof_depth. *) (*----------------------------------------------------------------------------*) let dec_print_depth x = if (!proof_print_depth < 1) then (proof_print_depth := 0; x) else (proof_print_depth := !proof_print_depth - 1; x);; (*----------------------------------------------------------------------------*) (* proof_print_term : term -> term *) (* *) (* Identity function on terms that has the side effect of printing the term *) (* if the `proof_printing' flag is set to true. *) (*----------------------------------------------------------------------------*) let proof_print_term tm = if !proof_printing then (print_string (implode (replicate " " !proof_print_depth)); print_term tm; print_newline () ; tm) else tm;; let proof_print_thm thm = if !proof_printing then ( print_thm thm; print_newline (); print_newline());; let proof_print_tmi (tm,i) = if !proof_printing then ( proof_print_term tm; print_string " ("; print_bool i; print_string ")"; (tm,i) ) else (tm,i);; (* let proof_print_clause cl = if !proof_printing then ( match cl with | Clause_proved thm -> (print_thm thm; print_newline (); cl) | _ -> cl ) else cl;; *) (*----------------------------------------------------------------------------*) (* proof_print_newline : * -> * *) (* *) (* Identity function that has the side effect of printing a newline if the *) (* `proof_printing' flag is set to true. *) (*----------------------------------------------------------------------------*) let proof_print_newline x = if !proof_printing then (print_newline (); x) else x;; let proof_print_string s x = if !proof_printing then (print_string s; x) else x;; let proof_print_string_l s x = if !proof_printing then (print_string s; print_newline (); x) else x;; (*----------------------------------------------------------------------------*) (* Recursive type for holding partly processed clauses. *) (* *) (* A clause is either still to be proved, has been proved, or can be proved *) (* once sub-clauses have been. A clause that is still to be proved carries a *) (* flag indicating whether or not it is an induction step. *) (*----------------------------------------------------------------------------*) type clause_tree = Clause of (term * bool) | Clause_proved of thm | Clause_split of clause_tree list * (thm list -> thm);; let rec proof_print_clausetree cl = if !proof_printing then ( proof_print_string_l "Clause tree:" (); match cl with | Clause (tm,bool) -> (print_term tm; print_newline ()) | Clause_proved thm -> (print_thm thm; print_newline()) | Clause_split (tlist,proof) -> (print_string "Split -> "; print_int (length tlist); print_newline () ; let void = map proof_print_clausetree tlist in () ));; (*----------------------------------------------------------------------------*) (* waterfall : ((term # bool) -> ((term # bool) list # proof)) list -> *) (* (term # bool) -> *) (* clause_tree *) (* *) (* `Waterfall' of heuristics. Takes a list of heuristics and a term as *) (* arguments. Each heuristic should fail if it can do nothing with its input. *) (* Otherwise the heuristic should return a list of new clauses to be proved *) (* together with a proof of the original clause from these new clauses. *) (* *) (* Clauses that are not processed by any of the heuristics are placed in a *) (* leaf node of the tree, to be proved later. The heuristics are attempted in *) (* turn. If a heuristic returns an empty list of new clauses, the proof is *) (* applied to an empty list, and the resultant theorem is placed in the tree *) (* as a leaf node. Otherwise, the tree is split, and each of the new clauses *) (* is passed to ALL of the heuristics. *) (*----------------------------------------------------------------------------*) let nth_tail n l = if (n > length l) then [] else let rec repeattl l i = if ( i = 0 ) then l else tl (repeattl l (i-1)) in repeattl l n;; let rec waterfall heuristics tmi = bm_steps := hashI ((+) 1) !bm_steps; let rec flow_on_down rest_of_heuristics tmi = if (is_F (fst tmi)) then (failwith "cannot prove") else if (rest_of_heuristics = []) then (Clause tmi) else try ((let (tms,f) = hd rest_of_heuristics tmi in if (tms = []) then (proof_print_string "Proven:" (); proof_print_thm (f []) ; Clause_proved (f [])) else if ((tl tms) = []) then (Clause_split ([waterfall heuristics (hd tms)],f)) else Clause_split ((dec_print_depth o map (waterfall heuristics o proof_print_newline) o inc_print_depth) tms, f)) )with Failure s -> (if (s = "cannot prove") then failwith s else (flow_on_down (tl rest_of_heuristics) tmi) ) in flow_on_down heuristics (proof_print_tmi tmi);; let rec filtered_waterfall heuristics warehouse tmi = bm_steps := hashI ((+) 1) !bm_steps; if (max_var_depth (fst tmi) > 12) then let void = (warn true "Reached maximum depth!") in failwith "cannot prove" else let heurn = try (assoc (fst tmi) warehouse) with Failure _ -> 0 in let warehouse = (if (heurn > 0) then let void = proof_print_string ("Warehouse kicking in! Skipping " ^ string_of_int(heurn) ^ " heuristic(s)") () ; in let void = proof_print_newline () in (List.remove_assoc (fst tmi) warehouse) else (warehouse)) in let rec flow_on_down rest_of_heuristics tmi it = if (is_F (fst tmi)) then (failwith "cannot prove") else let rest_of_heuristics = nth_tail heurn rest_of_heuristics in if (rest_of_heuristics = []) then (Clause tmi) else try (let (tms,f) = hd rest_of_heuristics tmi in if (tms = []) then (proof_print_string "Proven:" (); proof_print_thm (f []) ; Clause_proved (f [])) else if ((tl tms) = []) then Clause_split ([filtered_waterfall heuristics (((fst tmi),it)::warehouse) (hd tms)],f) else Clause_split ((dec_print_depth o map (filtered_waterfall heuristics (((fst tmi),it)::warehouse) o proof_print_newline) o inc_print_depth) tms, f) )with Failure s -> ( if (s = "cannot prove") then failwith s else (flow_on_down (tl rest_of_heuristics) tmi (it+1)) ) in flow_on_down heuristics ((hashI proof_print_term) tmi) 1;; (* in let fringe = fringe_of_clause_tree restree in if (fringe = []) then restree else ( waterfall_warehouse := ((fst tmi),it)::(!waterfall_warehouse) ; restree ) *) (*----------------------------------------------------------------------------*) (* fringe_of_clause_tree : clause_tree -> (term # bool) list *) (* *) (* Computes the fringe of a clause_tree, including in the resultant list only *) (* those clauses that remain to be proved. *) (*----------------------------------------------------------------------------*) let rec fringe_of_clause_tree tree = match tree with | (Clause tmi) -> [tmi] | (Clause_proved _) -> [] | (Clause_split (trees,_)) -> (flat (map fringe_of_clause_tree trees));; (*----------------------------------------------------------------------------*) (* prove_clause_tree : clause_tree -> proof *) (* *) (* Given a clause_tree, returns a proof that if given theorems for the *) (* unproved clauses in the tree, returns a theorem for the clause at the root *) (* of the tree. The list of theorems must be in the same order as the clauses *) (* appear in the fringe of the tree. *) (*----------------------------------------------------------------------------*) let prove_clause_tree tree ths = try( let rec prove_clause_trees trees ths = if (trees = []) then ([],ths) else let (th,ths') = prove_clause_tree' (hd trees) ths in let (thl,ths'') = prove_clause_trees (tl trees) ths' in (th::thl,ths'') and prove_clause_tree' tree ths = match tree with | (Clause (tm,_)) -> (let th = hd ths in if (proves th tm) then (th,tl ths) else failwith "prove_clause_tree") | (Clause_proved th) -> (th,ths) | (Clause_split (trees,f)) -> (let (thl,ths') = prove_clause_trees trees ths in (f thl,ths')) in (let (th,[]) = (prove_clause_tree' tree ths) in th) ) with Failure _ -> failwith "prove_clause_tree";; (*============================================================================*) (* Eliminating instances in the `pool' of clauses remaining to be proved *) (* *) (* Constructing partial orderings is probably overkill. It may only be *) (* necessary to split the clauses into two sets, one of most general clauses *) (* and the rest. This would still be computationally intensive, but it would *) (* avoid comparing two clauses that are both instances of some other clause. *) (*============================================================================*) (*----------------------------------------------------------------------------*) (* inst_of : term -> term -> thm -> thm *) (* *) (* Takes two terms and computes whether the first is an instance of the *) (* second. If this is the case, a proof of the first term from the second *) (* (assuming they are formulae) is returned. Otherwise the function fails. *) (*----------------------------------------------------------------------------*) let inst_of tm patt = try( (let (_,tm_bind,ty_bind) = term_match [] patt tm in let (insts,vars) = List.split tm_bind in let f = (SPECL insts) o (GENL vars) o (INST_TYPE ty_bind) in fun th -> apply_proof (f o hd) [patt] [th] )) with Failure _ -> failwith "inst_of";; (*----------------------------------------------------------------------------*) (* Recursive datatype for a partial ordering of terms using the *) (* `is an instance of' relation. *)let proof_print_thm thm = if !proof_printing then ( print_thm thm; print_newline (); print_newline());; (* *) (* The leaf nodes of the tree are terms that have no instances. The other *) (* nodes have a list of instance trees and proofs of each instance from the *) (* term at that node. *) (* *) (* Each term carries a number along with it. This is used to keep track of *) (* where the term came from in a list. The idea is to take the fringe of a *) (* clause tree, number the elements, then form partial orderings so that *) (* only the most general theorems have to be proved. *) (*----------------------------------------------------------------------------*) type inst_tree = No_insts of (term * int) | Insts of (term * int * (inst_tree * (thm -> thm)) list);; (*----------------------------------------------------------------------------*) (* insert_into_inst_tree : (term # int) -> inst_tree -> inst_tree *) (* insert_into_inst_trees : (term # int # (thm -> thm)) -> *) (* (inst_tree # (thm -> thm)) list -> *) (* (inst_tree # (thm -> thm)) list *) (* *) (* Mutually recursive functions for constructing partial orderings, ordered *) (* by `is an instance of' relation. The algorithm is grossly inefficient. *) (* Structures are repeatedly destroyed and rebuilt. Reference variables *) (* should be used for efficiency. *) (* *) (* Inserting into a single tree: *) (* *) (* If tm' is an instance of tm, tm is put in the root node, with the old tree *) (* as its single child. If tm is not an instance of tm', the function fails. *) (* Assume now that tm is an instance of tm'. If the tree is a leaf, it is *) (* made into a branch and tm is inserted as the one and only child. If the *) (* tree is a branch, an attempt is made to insert tm in the list of *) (* sub-trees. If this fails, tm is added as a leaf to the list of instances. *) (* Note that if tm is not an instance of tm', then it cannot be an instance *) (* of the instances of tm'. *) (* *) (* Inserting into a list of trees: *) (* *) (* The list of trees carry proofs with them. The list is split into those *) (* whose root is an instance of tm, and those whose root is not. The proof *) (* associated with a tree that is an instance is replaced by a proof of the *) (* term from tm. If the list of trees that are instances is non-empty, they *) (* are made children of a node containing tm, and this new tree is added to *) (* the list of trees that are n't instances. If tm has instances in the list, *) (* it cannot be the case that tm is an instance of one of the other trees in *) (* the list, for the trees in a list must be unrelated. *) (* *) (* If there are no instances of tm in the list of trees, an attempt is made *) (* to insert tm into the list. If it is unrelated to all of the trees, this *) (* attempt fails, in which case tm is made into a leaf and added to the list. *) (*----------------------------------------------------------------------------*) let rec insert_into_inst_tree (tm,n) tree = match tree with | (No_insts (tm',n')) -> (try ( (let f = inst_of tm' tm in Insts (tm,n,[No_insts (tm',n'),f])) ) with Failure _ -> try( let f = inst_of tm tm' in Insts (tm',n',[No_insts (tm,n),f])) with Failure _ -> failwith "insert_into_inst_tree" ) | (Insts (tm',n',insts)) -> (try (let f = inst_of tm' tm in Insts (tm,n,[Insts (tm',n',insts),f])) with Failure _ -> try(let f = inst_of tm tm' in try( Insts (tm',n',insert_into_inst_trees (tm,n,f) insts)) with Failure _ -> (Insts (tm',n',(No_insts (tm,n),f)::insts)) ) with Failure _ -> failwith "insert_into_inst_tree" ) and insert_into_inst_trees (tm,n,f) insts = let rec instances (tm,n) insts = if (insts = []) then ([],[]) else let (not_instl,instl) = instances (tm,n) (tl insts) and (h,f) = hd insts in let (tm',n') = match h with | (No_insts (tm',n')) -> (tm',n') | (Insts (tm',n',_)) -> (tm',n') in (try( (let f' = inst_of tm' tm in (not_instl,(h,f')::instl)) ) with Failure _ -> ((h,f)::not_instl,instl) ) and insert_into_inst_trees' (tm,n) trees = if (trees = []) then failwith "insert_into_inst_trees'" else (try( ((insert_into_inst_tree (tm,n) (hd trees))::(tl trees)) ) with Failure _ -> ((hd trees)::(insert_into_inst_trees' (tm,n) (tl trees))) ) in let (not_instl,instl) = instances (tm,n) insts in if (instl = []) then try( (lcombinep o (hashI (insert_into_inst_trees' (tm,n)))) (List.split insts) ) with Failure _ -> ((No_insts (tm,n),f)::insts) else (Insts (tm,n,instl),f)::not_instl;; (*----------------------------------------------------------------------------*) (* mk_inst_trees : (term # int) list -> inst_tree list *) (* *) (* Constructs a partial ordering of terms under the `is an instance of' *) (* relation from a list of numbered terms. *) (* *) (* A dummy proof is passed to the call of insert_into_inst_trees. The result *) (* of the call has a proof associated with the root of each tree. These *) (* proofs are dummies and so are discarded before the final result is *) (* returned. *) (*----------------------------------------------------------------------------*) let mk_inst_trees tmnl = let rec mk_inst_trees' insts tmnl = if (tmnl = []) then insts else let (tm,n) = hd tmnl in mk_inst_trees' (insert_into_inst_trees (tm,n,I) insts) (tl tmnl) in map fst (mk_inst_trees' [] tmnl);; (*----------------------------------------------------------------------------*) (* roots_of_inst_trees : inst_tree list -> term list *) (* *) (* Computes the terms at the roots of a list of partial orderings. *) (*----------------------------------------------------------------------------*) let rec roots_of_inst_trees trees = if (trees = []) then [] else let tm = match (hd trees) with | (No_insts (tm,_)) -> tm | (Insts (tm,_,_)) -> tm in tm::(roots_of_inst_trees (tl trees));; (*----------------------------------------------------------------------------*) (* prove_inst_tree : inst_tree -> thm -> (thm # int) list *) (* *) (* Given a partial ordering of terms and a theorem for its root, returns a *) (* list of theorems for the terms in the tree. *) (*----------------------------------------------------------------------------*) let rec prove_inst_tree tree th = match tree with | (No_insts (tm,n)) -> (if (proves th tm) then [(th,n)] else failwith "prove_inst_tree") | (Insts (tm,n,insts)) -> (if (proves th tm) then (th,n)::(flat (map (fun (tr,f) -> prove_inst_tree tr (f th)) insts)) else failwith "prove_inst_tree");; (*----------------------------------------------------------------------------*) (* prove_inst_trees : inst_tree list -> thm list -> thm list *) (* *) (* Given a list of partial orderings of terms and a list of theorems for *) (* their roots, returns a sorted list of theorems for the terms in the trees. *) (* The sorting is done based on the integer labels attached to each term in *) (* the trees. *) (*----------------------------------------------------------------------------*) let prove_inst_trees trees ths = try ( map fst (sort_on_snd (flat (map (uncurry prove_inst_tree) (lcombinep (trees,ths))))) ) with Failure _ -> failwith "prove_inst_trees";; (*----------------------------------------------------------------------------*) (* prove_pool : conv -> term list -> thm list *) (* *) (* Attempts to prove the pool of clauses left over from the waterfall, by *) (* applying the conversion, conv, to the most general clauses. *) (*----------------------------------------------------------------------------*) let prove_pool conv tml = let tmnl = number_list tml in let trees = mk_inst_trees tmnl in let most_gen_terms = roots_of_inst_trees trees in let ths = map conv most_gen_terms in prove_inst_trees trees ths;; (*============================================================================*) (* Boyer-Moore prover *) (*============================================================================*) (*----------------------------------------------------------------------------*) (* WATERFALL : ((term # bool) -> ((term # bool) list # proof)) list -> *) (* ((term # bool) -> ((term # bool) list # proof)) -> *) (* (term # bool) -> *) (* thm *) (* *) (* Boyer-Moore style automatic proof procedure. Takes a list of heuristics, *) (* and a single heuristic that does induction, as arguments. The result is a *) (* function that, given a term and a Boolean, attempts to prove the term. The *) (* Boolean is used to indicate whether the term is the step of an induction. *) (* It will normally be set to false for an external call. *) (*----------------------------------------------------------------------------*) let rec WATERFALL heuristics induction (tm,(ind:bool)) = let conv tm = proof_print_string "Doing induction on:" () ; bm_steps := hash ((+) 1) ((+) 1) !bm_steps ; let void = proof_print_term tm ; proof_print_newline () in let (tmil,proof) = induction (tm,false) in dec_print_depth (proof (map (WATERFALL heuristics induction) (inc_print_depth tmil))) in let void = proof_print_newline () in let tree = waterfall heuristics (tm,ind) in let tmil = fringe_of_clause_tree tree in let thl = prove_pool conv (map fst tmil) in prove_clause_tree tree thl;; let rec FILTERED_WATERFALL heuristics induction warehouse (tm,(ind:bool)) = let conv tm = (* let constr_check = ind && not((find_bm_terms (fun t -> count_constructors t > 5) tm) = []) in *) let constr_check = (max_var_depth tm > 12) in if (constr_check) then let void = (warn true "Reached maximum depth!") in failwith "cannot prove" else let heurn = try (assoc tm warehouse) with Failure _ -> 0 in let warehouse = (if (heurn > 0) then (List.remove_assoc tm warehouse) else (warehouse)) in if (heurn > length heuristics) then ( warn true "Induction loop detected."; failwith "cannot prove" ) else proof_print_string "Doing induction on:" (); bm_steps := hash ((+) 1) ((+) 1) !bm_steps ; let void = proof_print_term tm ; proof_print_newline () in let (tmil,proof) = induction (tm,false) in dec_print_depth (proof (map (FILTERED_WATERFALL heuristics induction ((tm,(length heuristics) + 1)::warehouse)) (inc_print_depth tmil))) in let void = proof_print_newline () in let tree = filtered_waterfall heuristics [] (tm,ind) (* in let void = proof_print_clausetree tree *) in let tmil = fringe_of_clause_tree tree in let thl = prove_pool conv (map fst tmil) in prove_clause_tree tree thl;; (*============================================================================*) (* Some sample heuristics *) (*============================================================================*) (*----------------------------------------------------------------------------*) (* conjuncts_heuristic : (term # bool) -> ((term # bool) list # proof) *) (* *) (* `Heuristic' for splitting a conjunction into a list of conjuncts. *) (* Right conjuncts are split recursively. *) (* Fails if the argument term is not a conjunction. *) (*----------------------------------------------------------------------------*) let conjuncts_heuristic (tm,(i:bool)) = let tms = conj_list tm in if (length tms = 1) then failwith "conjuncts_heuristic" else (map (fun tm -> (tm,i)) tms,apply_proof LIST_CONJ tms);; (*----------------------------------------------------------------------------*) (* refl_heuristic : (term # bool) -> ((term # bool) list # proof) *) (* *) (* `Heuristic' for proving that terms of the form "x = x" are true. Fails if *) (* the argument term is not of this form. Otherwise it returns an empty list *) (* of new clauses, and a proof of the original term. *) (*----------------------------------------------------------------------------*) let refl_heuristic (tm,(i:bool)) = try(if (lhs tm = rhs tm) then (([]:(term * bool) list),apply_proof (fun ths -> REFL (lhs tm)) []) else failwith "" ) with Failure _ -> failwith "refl_heuristic";; (*----------------------------------------------------------------------------*) (* clausal_form_heuristic : (term # bool) -> ((term # bool) list # proof) *) (* *) (* `Heuristic' that tests a term to see if it is in clausal form, and if not *) (* converts it to clausal form and returns the resulting clauses as new *) (* `goals'. It is critical for efficiency that the normalization is only done *) (* if the term is not in clausal form. Note that the functions `conjuncts' *) (* and `disjuncts' are not used for the testing because they split trees of *) (* conjuncts (disjuncts) rather than simply `linear' con(dis)junctions. *) (* If the term is in clausal form, but is not a single clause, it is split *) (* into single clauses. If the term is in clausal form but contains Boolean *) (* constants, the normalizer is applied to it. A single new goal will be *) (* produced in this case unless the result of the normalization was true. *) (*----------------------------------------------------------------------------*) let clausal_form_heuristic (tm,(i:bool)) = try (let is_atom tm = (not (has_boolean_args_and_result tm)) or (is_var tm) or (is_const tm) in let is_literal tm = (is_atom tm) or ((is_neg tm) & (try (is_atom (rand tm)) with Failure _ -> false)) in let is_clause tm = forall is_literal (disj_list tm) in let result_string = fun tms -> let s = length tms in let plural = if (s=1) then "" else "s" in ("-> Clausal Form Heuristic (" ^ string_of_int(s) ^ " clause" ^ plural ^ ")") in if (forall is_clause (conj_list tm)) & (not (free_in `T` tm)) & (not (free_in `F` tm)) then if (is_conj tm) then let tms = conj_list tm in (proof_print_string_l (result_string tms) () ; (map (fun tm -> (tm,i)) tms,apply_proof LIST_CONJ tms)) else failwith "" else let th = CLAUSAL_FORM_CONV tm in let tm' = rhs (concl th) in if (is_T tm') then (proof_print_string_l "-> Clausal Form Heuristic" () ; ([],apply_proof (fun _ -> EQT_ELIM th) [])) else let tms = conj_list tm' in (proof_print_string_l (result_string tms) () ; (map (fun tm -> (tm,i)) tms, apply_proof ((EQ_MP (SYM th)) o LIST_CONJ) tms)) ) with Failure _ -> failwith "clausal_form_heuristic";; let meson_heuristic (tm,(i:bool)) = try( let meth = MESON (rewrite_rules()) tm in (([]:(term * bool) list),apply_proof (fun ths -> meth) []) ) with Failure _ -> failwith "meson_heuristic";; let taut_heuristic (tm,(i:bool)) = try( let tautthm = TAUT tm in (proof_print_string_l "-> Tautology Heuristic" () ; (([]:(term * bool) list),apply_proof (fun ths -> tautthm) [])) ) with Failure _ -> failwith "taut_heuristic";; let setify_heuristic (tm,(i:bool)) = try ( if (not (is_disj tm)) then failwith "" else let tms = disj_list tm in let tms' = setify tms in let tm' = list_mk_disj tms' in if ((length tms) = (length tms')) then failwith "" else let th = TAUT (mk_imp (tm',tm)) in (proof_print_string_l "-> Setify Heuristic" () ; ([tm',i],apply_proof ((MP th) o hd) [tm'])) ) with Failure _ -> failwith "setify_heuristic";;