(* $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 ->
+ Equality_retrieval.auto_type option ->
+ 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 *)
+ Equality_retrieval.auto_type option ->
+ AutoCache.cache ->
+ Equality.equality_bag *
+ Equality.equality list * AutoCache.cache * int
+
+val close_more:
+ Equality.equality_bag ->
+ active_table ->
+ int -> (* maxmeta *)
+ ProofEngineTypes.status ->
+ bool -> (* smart flag *)
+ Equality_retrieval.auto_type option ->
+ 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
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 *)