integration with paramodulation

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 568e12ca40c4b303bd182ea3688efba78070ea0f..d46aa6949c9f074526ca0ab312f96e6f8f90db22 100644 (file)
--- 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 90f958e7ba0e0fa07ba4d6913ec074239df6a11d..c91e92e3f03e6c181148b47ed381101e9cfad79e 100644 (file)
--- 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