module type S = sig .. end
module Env: Env.S
val given_clause_step : ?generating:bool -> int -> Saturate.szs_status
Perform one step of the given clause algorithm.
It performs generating inferences only if generating is true (default);
other parameters are the iteration number and the environment
val given_clause : ?generating:bool ->
?steps:int -> ?timeout:float -> unit -> Saturate.szs_status * int
run the given clause until a timeout occurs or a result
is found. It returns a tuple (new state, result, number of steps done).
It performs generating inferences only if generating is true (default)
val presaturate : unit -> Saturate.szs_status * int
Interreduction of the given state, without generating inferences. Returns
the number of steps done for presaturation, with status of the set.