Make (p.libzipperposition.2.0.doc.libzipperposition.Libzipperposition.Saturate.Make)

Parameters

module E : Env.S

Signature

module Env = E

val given_clause_step : ?generating:bool -> int -> 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 ->
  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 -> szs_status * int

Interreduction of the given state, without generating inferences. Returns the number of steps done for presaturation, with status of the set.