- type bag = B.t Terms.bag * int
- val mk_passive : bag -> B.input * B.input -> bag * B.t Terms.unit_clause
- val mk_goal : bag -> B.input * B.input -> bag * B.t Terms.unit_clause
+ type t
+ type input
+ type state
+ type szsontology =
+ | Unsatisfiable of
+ (t Terms.bag * int * t Terms.substitution * int list) list
+ | GaveUp
+ | Error of string
+ | Timeout of int * t Terms.bag
+ type bag = t Terms.bag * int
+ val empty_state : state
+ val bag_of_state :state -> bag
+ val replace_bag : state -> bag -> state
+ val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
+ val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
+ val forward_infer_step :
+ state ->
+ t Terms.unit_clause ->
+ int ->
+ state
+ val goal_narrowing :
+ int
+ -> int
+ -> float option
+ -> state
+ -> state