Major changes to auto, documented on the helm mailing list.

[helm.git] / components / tactics / paramodulation / saturation.mli

diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli
index aa8f24ec3f0a842b011d95ba6fc14634ba13a791..0c9a75e62478dff464ea8ee5b5451b662939a1a4 100644 (file)
--- a/components/tactics/paramodulation/saturation.mli
+++ b/components/tactics/paramodulation/saturation.mli
@@ -25,42 +25,40 @@
 
 (* $Id$ *)
 
-val saturate : (* FIXME: should be exported a a tactic *)
-  bool ->
-  HMysql.dbd ->
-  ?full:bool ->
-  ?depth:int ->
-  ?width:int ->
-  ?timeout:float ->
-  Equality_retrieval.auto_type option ->
-  ProofEngineTypes.status ->
-  ProofEngineTypes.proof * ProofEngineTypes.goal list
+type passive_table
+type active_table = Equality.equality list * Indexing.Index.t
+
+val reset_refs : unit -> unit
 
-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 list_of_passive: passive_table -> Equality.equality list
 
-val find_equalities:
-  HMysql.dbd ->
-  ProofEngineTypes.status ->
-  bool -> (* smart_flag *)
-  Equality_retrieval.auto_type option -> 
-  AutoCache.cache -> 
-  Equality.equality_bag *
-    Equality.equality list * AutoCache.cache * int
-
-val close_more: 
+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 ->
-  int -> (* maxmeta *)
+  passive_table -> 
+  int -> 
+  float -> 
+  active_table * passive_table * int
+val all_subsumed :
+  Equality.equality_bag ->
+  int ->
   ProofEngineTypes.status ->
-  bool -> (* smart flag *)
-  Equality_retrieval.auto_type option ->
-  AutoCache.cache ->
-    Equality.equality_bag * Equality.equality list * AutoCache.cache * int
-
+  active_table ->
+  passive_table -> 
+  (Cic.substitution * 
+     ProofEngineTypes.proof * 
+     ProofEngineTypes.goal list) list * int
 val given_clause: 
   Equality.equality_bag ->
   int -> (* maxmeta *)
@@ -73,28 +71,4 @@ val given_clause:
      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
-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
-(* eof *)