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
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