package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 =
  1. | Unsat of Logtk.Proof.S.t
  2. | Sat
  3. | Unknown
  4. | Error of string
  5. | Timeout

The SZS status of a state

module type S = sig ... end
module Make (E : Env.S) : S with module Env = E