X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=b4a3118199d517266147b7712a976a54ce841e08;hb=65a9c286a765dd984bee251399b0d1e86d4db34c;hp=1ba1dd912495f63801c7ffbf90b0d785e93e883e;hpb=3b7bfb05e6fc1a2ac6864d8f7d959fcda0597d21;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 1ba1dd912..b4a311819 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -325,13 +325,18 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   (* argument parsing *)
   let depth = int "depth" params in
   let width = int "width" params in
+  let timeout = string "timeout" params in
   let paramodulation = bool "paramodulation" params in
   let full = bool "full" params in
   let superposition = bool "superposition" params in
-  let what = string "what" params in
-  let other = string "other" params in
+  let target = string "target" params in
+  let table = string "table" params in
   let subterms_only = bool "subterms_only" params in
-  let demodulate = bool "demodulate" params in
+  let caso_strano = bool "caso_strano" params in
+  let demod_table = string "demod_table" params in
+  let timeout = 
+    try Some (float_of_string timeout) with Failure _ -> None
+  in
   (* the real tactic *)
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
@@ -363,7 +368,8 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
       try
-        let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
+        let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full
+        ?timeout (proof, goal) in
         prerr_endline (Saturation.get_stats ());
         rc
       with exn ->
@@ -378,7 +384,7 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   match superposition with
   | true -> 
       ProofEngineTypes.mk_tactic
-       (Saturation.superposition_tac ~what ~other ~subterms_only ~demodulate)
+       (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table)
   | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd)
 ;;
 
@@ -412,7 +418,7 @@ let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term'
         [g1;g2] ->
           let proof'',goals =
            ProofEngineTypes.apply_tactic
-           (auto_tac ~params:["paramodulation","on"] ~dbd) (proof'',g2)
+           (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2)
           in
            let proof'',goals =
             ProofEngineTypes.apply_tactic
@@ -493,3 +499,5 @@ let applyS_tac ~dbd ~term =
     | CicUnification.UnificationFailure msg
     | CicTypeChecker.TypeCheckerFailure msg ->
         raise (ProofEngineTypes.Fail msg))
+
+let pp_proofterm = Equality.pp_proofterm;;