X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.mli;h=d16c9e28a8aa9f8653b149c82b8c03fd025f5e5c;hb=bd4a73c6f758bd39254178dd7b313af321a5cd4b;hp=d48dfc349ba77d007b9da65e564b618981b68028;hpb=8752fac73a864c821b6954f0572bce2052924183;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index d48dfc349..d16c9e28a 100644
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -25,16 +25,63 @@
 
 (* $Id$ *)
 
-
-val saturate :
+val saturate : (* FIXME: should be exported a a tactic *)
   bool ->
   HMysql.dbd ->
   ?full:bool ->
   ?depth:int ->
   ?width:int ->
-  ProofEngineTypes.proof * ProofEngineTypes.goal ->
+  ?timeout:float ->
+  ?auto:Equality_retrieval.auto_type ->
+  ProofEngineTypes.status ->
   ProofEngineTypes.proof * ProofEngineTypes.goal list
 
+type active_table 
+type passive_table 
+val make_active: Equality.equality list -> active_table
+val make_passive: Equality.equality list -> passive_table
+val add_to_passive: Equality.equality list -> passive_table -> passive_table
+
+val find_equalities:
+  HMysql.dbd ->
+  ProofEngineTypes.status ->
+  bool -> (* smart_flag *)
+  ?auto:Equality_retrieval.auto_type -> 
+  AutoCache.cache ->
+  Equality.equality_bag *
+    Equality.equality list * AutoCache.cache * int
+val saturate_more: 
+  Equality.equality_bag ->
+  active_table ->
+  int -> (* maxmeta *)
+  ProofEngineTypes.status ->
+  bool -> (* smart flag *)
+  ?auto:Equality_retrieval.auto_type ->
+  AutoCache.cache ->
+    Equality.equality_bag * Equality.equality list * AutoCache.cache * int
+
+val given_clause: 
+  Equality.equality_bag ->
+  int -> (* maxmeta *)
+  ProofEngineTypes.status ->
+  active_table ->
+  passive_table -> 
+  int -> int -> float -> 
+    (Cic.substitution * 
+     ProofEngineTypes.proof * 
+     ProofEngineTypes.goal list) option * 
+    active_table * passive_table * int
+
+val demodulate_tac: dbd:HMysql.dbd ->  ProofEngineTypes.tactic
+
+val superposition_tac: 
+  target:string -> table:string -> subterms_only:bool ->
+  demod_table:string ->  ProofEngineTypes.proof * ProofEngineTypes.goal ->
+   ProofEngineTypes.proof * ProofEngineTypes.goal list
+
+val get_stats: unit -> string
+  
+(* this is used only in saturate_main: MUST BE REMOVED!  *)
 val weight_age_ratio : int ref
 val weight_age_counter: int ref
 val symbols_ratio: int ref
@@ -43,16 +90,10 @@ val use_fullred: bool ref
 val time_limit: float ref
 val maxwidth: int ref
 val maxdepth: int ref
-val retrieve_and_print: HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit
+val retrieve_and_print: 
+  HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit
 val main_demod_equalities: HMysql.dbd ->
     Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
 val main: HMysql.dbd ->
     bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
-val demodulate_tac: dbd:HMysql.dbd ->  ProofEngineTypes.tactic
-
-val superposition_tac: 
-  target:string -> table:string -> subterms_only:bool ->
-  demod_table:string ->  ProofEngineTypes.proof * ProofEngineTypes.goal ->
-   ProofEngineTypes.proof * ProofEngineTypes.goal list
-
-val get_stats: unit -> string
+(* eof *)