(* $Id$ *)
+type passive_table
+type active_table = Equality.equality list * Indexing.Index.t
-val saturate :
- bool ->
- HMysql.dbd ->
- ?full:bool ->
- ?depth:int ->
- ?width:int ->
- ?timeout:float ->
- ProofEngineTypes.proof * ProofEngineTypes.goal ->
- ProofEngineTypes.proof * ProofEngineTypes.goal list
+val reset_refs : unit -> unit
-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 -> ProofEngineTypes.tactic
+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 add_to_active:
+ Equality.equality_bag ->
+ active_table -> passive_table ->
+ Utils.environment -> Cic.term (* ty *) -> Cic.term -> Cic.metasenv ->
+ active_table * passive_table * Equality.equality_bag
+val list_of_passive: passive_table -> Equality.equality list
+val list_of_active: active_table -> Equality.equality list
-val superposition_tac:
- target:string -> table:string -> subterms_only:bool ->
- demod_table:string -> ProofEngineTypes.proof * ProofEngineTypes.goal ->
- ProofEngineTypes.proof * ProofEngineTypes.goal list
+val simplify_equalities :
+ Equality.equality_bag ->
+ UriManager.uri ->
+ Utils.environment ->
+ Equality.equality list ->
+ Equality.equality_bag * Equality.equality list
+val pump_actives :
+ Cic.context ->
+ Equality.equality_bag ->
+ active_table ->
+ passive_table ->
+ int ->
+ float ->
+ active_table * passive_table * Equality.equality_bag
+val all_subsumed :
+ Equality.equality_bag ->
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) list
+val given_clause:
+ Equality.equality_bag ->
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ int -> int -> float ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) option *
+ active_table * passive_table * Equality.equality_bag
-val get_stats: unit -> string
+val solve_narrowing:
+ Equality.equality_bag ->
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ int ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) option *
+ active_table * passive_table * Equality.equality_bag