sig
type t
type input
+ type state
type szsontology =
- | Unsatisfiable of (t Terms.bag * int * int list) list
+ | 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
val paramod :
+ useage:bool ->
max_steps:int ->
?timeout:float ->
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