package libzipperposition

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

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct