type input
type state
type szsontology =
- | Unsatisfiable of
- (t Terms.bag * int * t Terms.substitution * int list) list
+ | Unsatisfiable of (t Terms.bag * int * 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 :
t Terms.unit_clause ->
int ->
state
- val goal_narrowing :
- int
- -> int
- -> float option
- -> state
- -> state
val paramod :
useage:bool ->
max_steps:int ->
bag ->
g_passives:t Terms.unit_clause list ->
passives:t Terms.unit_clause list -> szsontology
- val demod :
- state -> input* input -> szsontology
- val fast_eq_check :
- state -> input* input -> szsontology
- val nparamod :
- useage:bool ->
- max_steps:int ->
- ?timeout:float ->
- state ->
- input* input ->
- szsontology
end
module Paramod ( B : Orderings.Blob ) : Paramod