sig
type t
type input
+ type state
type szsontology =
| 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 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 paramod :
useage:bool ->
max_steps:int ->