more work for the generic auto parameters

diff --git a/helm/software/components/binaries/tptp2grafite/main.ml b/helm/software/components/binaries/tptp2grafite/main.ml
index 871ff7b56a6299f0a497f913dfed177e9b978f68..786ff7e75abc7a00d2f94d9498210601cb7b6308 100644 (file)
--- a/helm/software/components/binaries/tptp2grafite/main.ml
+++ b/helm/software/components/binaries/tptp2grafite/main.ml
@@ -201,7 +201,7 @@ let convert_ast statements context = function
                 fv)) 
            else [])@
             [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
-              GA.Auto (floc,None,None,Some "paramodulation",None)),
+            GA.Auto (floc,["paramodulation",""])),
                 Some (GA.Dot(floc))))]@
           (if fv <> [] then     
             (List.flatten

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 1ba1dd912495f63801c7ffbf90b0d785e93e883e..63dc8631dbc8b4b564fded81c72ea44fcffe204c 100644 (file)
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -328,10 +328,10 @@ let auto_tac ~params ~(dbd:HMysql.dbd) =
   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 demod_table = string "demod_table" params in
   (* the real tactic *)
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
@@ -378,7 +378,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)
 ;;
 

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index f81556c8f997e7088fbfe006b3552fdec48c8132..bb1b3a853515d22c49fecc0e9b43e944e0b55d17 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1888,8 +1888,19 @@ let rec position_of i x = function
   | _ -> i
 ;;
 
-let superposition_tac ~what ~other ~subterms_only ~demodulate status = 
+(* Syntax: 
+ *   auto superposition target = NAME 
+ *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
+ *
+ *  - if table is omitted no superposition will be performed
+ *  - if demod_table is omitted no demodulation will be prformed
+ *  - subterms_only is passed to Indexing.superposition_right
+ *
+ *  lists are coded using _ (example: H_H1_H2)
+ *)
+let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   reset_refs();
+  Indexing.init_index ();
   let proof,goalno = status in 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
@@ -1897,18 +1908,32 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status =
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let names = names_of_context context in
   let eq_index, equalities, maxm = find_equalities context proof in
-  let what = find_in_ctx 1 what context in
-  let other = find_in_ctx 1 other context in
-  let eq_what = List.nth equalities (position_of 0 what eq_index) in
-  let eq_other = List.nth equalities (position_of 0 other eq_index) in
-  let index = Indexing.index Indexing.empty eq_other in
+  let eq_what = 
+    let what = find_in_ctx 1 target context in
+    List.nth equalities (position_of 0 what eq_index)
+  in
+  let eq_other = 
+    if table <> "" then
+      let other = 
+        let others = Str.split (Str.regexp "_") table in 
+        List.map (fun other -> find_in_ctx 1 other context) others 
+      in
+      List.map 
+        (fun other -> List.nth equalities (position_of 0 other eq_index)) 
+        other 
+    else
+      []
+  in
+  let index = List.fold_left Indexing.index Indexing.empty eq_other in
   let maxm, eql = 
+    if table = "" then maxm,[eq_what] else 
     Indexing.superposition_right 
       ~subterms_only eq_uri maxm env index eq_what
   in
   prerr_endline ("Superposition right:");
   prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
-  prerr_endline ("\n table: " ^ Equality.string_of_equality eq_other ~env);
+  prerr_endline ("\n table: ");
+  List.iter (fun e -> prerr_endline ("  " ^ Equality.string_of_equality e ~env)) eq_other;
   prerr_endline ("\n result: ");
   List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
   prerr_endline ("\n result (cut&paste): ");
@@ -1917,9 +1942,18 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status =
       let t = Equality.term_of_equality eq_uri e in
       prerr_endline (CicPp.pp t names)) 
   eql;
-  if demodulate then
+  if demod_table <> "" then
     begin
-      let table = List.fold_left Indexing.index Indexing.empty equalities in
+      let demod = 
+        let demod = Str.split (Str.regexp "_") demod_table in 
+        List.map (fun other -> find_in_ctx 1 other context) demod 
+      in
+      let eq_demod = 
+        List.map 
+          (fun demod -> List.nth equalities (position_of 0 demod eq_index)) 
+          demod 
+      in
+      let table = List.fold_left Indexing.index Indexing.empty eq_demod in
       let maxm,eql = 
         List.fold_left 
           (fun (maxm,acc) e -> 
@@ -1946,5 +1980,6 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status =
 
 let get_stats () = 
   <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
-  Equality.get_stats ();;
+  Equality.get_stats ()
+;;
 

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 6a46887113343e2bf436729494a9ab97de61d584..9f1ad293d97cfa1563df07112ed52a4bf6b3b642 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -52,9 +52,8 @@ val demodulate_tac:
   pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 
 val superposition_tac: 
-  what:string -> other:string -> subterms_only:bool ->
-  demodulate:bool ->  
-  ProofEngineTypes.proof * ProofEngineTypes.goal ->
+  target:string -> table:string -> subterms_only:bool ->
+  demod_table:string ->  ProofEngineTypes.proof * ProofEngineTypes.goal ->
    ProofEngineTypes.proof * ProofEngineTypes.goal list
 
 val get_stats: unit -> string