From cb790b3f03194d3155841431d17cfea1245fea9d Mon Sep 17 00:00:00 2001 From: Alberto Griggio Date: Thu, 21 Jul 2005 11:48:42 +0000 Subject: [PATCH] integration with paramodulation --- helm/ocaml/tactics/autoTactic.ml | 50 +++++++++++++++++++++++++++++-- helm/ocaml/tactics/autoTactic.mli | 7 +++++ 2 files changed, 55 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 568e12ca4..d46aa6949 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) - let debug_print = ignore (*prerr_endline *) + let debug_print = (* ignore *) prerr_endline (* let debug_print = fun _ -> () *) @@ -275,6 +275,7 @@ and auto_new_aux dbd width already_seen_goals universe = function let default_depth = 5 let default_width = 3 +(* let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () = @@ -283,17 +284,62 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) Hashtbl.clear inspected_goals; debug_print "Entro in Auto"; let id t = t in + let t1 = Unix.gettimeofday () in match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with [] -> debug_print("Auto failed"); raise (ProofEngineTypes.Fail "No Applicable theorem") - | (_,(proof,[],_))::_ -> + | (_,(proof,[],_))::_ -> + let t2 = Unix.gettimeofday () in debug_print "AUTO_TAC HA FINITO"; let _,_,p,_ = proof in debug_print (CicPp.ppterm p); + Printf.printf "tempo: %.9f\n" (t2 -. t1); (proof,[]) | _ -> assert false in ProofEngineTypes.mk_tactic (auto_tac dbd) ;; +*) + +let paramodulation_tactic = ref + (fun dbd status -> raise (ProofEngineTypes.Fail "Not Ready yet..."));; + +let term_is_equality = ref + (fun term -> debug_print "term_is_equality E` DUMMY!!!!"; false);; +let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () = + let auto_tac dbd (proof, goal) = + let paramodulation_ok = + let _, metasenv, _, _ = proof in + let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in + !term_is_equality meta_goal + in + if paramodulation_ok then ( + debug_print "USO PARAMODULATION..."; + try + !paramodulation_tactic dbd (proof, goal) + with e -> + raise (ProofEngineTypes.Fail "paramodulation failure") + ) else + let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in + Hashtbl.clear inspected_goals; + debug_print "Entro in Auto"; + let id t = t in + let t1 = Unix.gettimeofday () in + match + auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] + with + [] -> debug_print("Auto failed"); + raise (ProofEngineTypes.Fail "No Applicable theorem") + | (_,(proof,[],_))::_ -> + let t2 = Unix.gettimeofday () in + debug_print "AUTO_TAC HA FINITO"; + let _,_,p,_ = proof in + debug_print (CicPp.ppterm p); + debug_print (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)); + (proof,[]) + | _ -> assert false + in + ProofEngineTypes.mk_tactic (auto_tac dbd) +;; diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli index 90f958e7b..c91e92e3f 100644 --- a/helm/ocaml/tactics/autoTactic.mli +++ b/helm/ocaml/tactics/autoTactic.mli @@ -27,3 +27,10 @@ val auto_tac: ?depth:int -> ?width:int -> dbd:Mysql.dbd -> unit -> ProofEngineTypes.tactic + +val paramodulation_tactic: + (Mysql.dbd -> ProofEngineTypes.status -> + ProofEngineTypes.proof * ProofEngineTypes.goal list) ref + +val term_is_equality: + (Cic.term -> bool) ref -- 2.39.2