From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 21 Jul 2005 11:48:42 +0000 (+0000)
Subject: integration with paramodulation
X-Git-Tag: V_0_7_2~128
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cb790b3f03194d3155841431d17cfea1245fea9d;p=helm.git

integration with paramodulation
---

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