X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.mli;h=0c9a75e62478dff464ea8ee5b5451b662939a1a4;hb=f809c7537eda20a275b17bc1407f0ee446f70356;hp=7a16895a77a8abe67d9f1eb4eeadfcc33ae39590;hpb=942023d1f147318b7869f40fb1556c2d69f3d731;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 7a16895a7..0c9a75e62 100644
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -25,31 +25,50 @@
 
 (* $Id$ *)
 
+type passive_table
+type active_table = Equality.equality list * Indexing.Index.t
 
-val saturate :
-  HMysql.dbd ->
-  ?full:bool ->
-  ?depth:int ->
-  ?width:int ->
-  ProofEngineTypes.proof * ProofEngineTypes.goal ->
-  (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) *
-  ProofEngineTypes.goal list
+val reset_refs : unit -> unit
+
+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 list_of_passive: passive_table -> Equality.equality list
+
+val simplify_equalities : 
+  Equality.equality_bag ->
+  UriManager.uri ->
+  Utils.environment -> 
+  Equality.equality list -> 
+  Equality.equality list
+val pump_actives :
+  Cic.context ->
+  Equality.equality_bag ->
+  int ->
+  active_table ->
+  passive_table -> 
+  int -> 
+  float -> 
+  active_table * passive_table * int
+val all_subsumed :
+  Equality.equality_bag ->
+  int ->
+  ProofEngineTypes.status ->
+  active_table ->
+  passive_table -> 
+  (Cic.substitution * 
+     ProofEngineTypes.proof * 
+     ProofEngineTypes.goal list) list * 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 weight_age_ratio : int ref
-val weight_age_counter: int ref
-val symbols_ratio: int ref
-val symbols_counter: int ref
-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 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 ->  
-  pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
 
-val get_stats: unit -> string