Module `Libzipperposition.Saturate`

Main saturation algorithm.

It uses inference rules and simplification rules from Superposition.

val check_timeout : float option -> bool: check whether we still have some time w.r.t timeout

type szs_status = | Unsat of Logtk.Proof.S.t | Sat | Unknown | Error of string | Timeout: The SZS status of a state

val k_abort_after_fragment_check : bool Logtk.Flex_state.key

module type S = sig ... end

module Make : functor (E : Env.S) -> S with module Env = E