package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t = {
  1. name : string;
    (*

    name of the prover

    *)
  2. command : string;
    (*

    command to call prover

    *)
  3. unsat : string list;
    (*

    prover returned unsat (possible outputs)

    *)
  4. sat : string list;
    (*

    prover returned sat (possible outputs)

    *)
}

data useful to invoke a prover. The prover must read from stdin. The command is interpolated using Buffer.add_substitude, with the given patterns:

  • "timeout" is the timeout in seconds
val lookup : string -> t

Lookup a prover by its name.

  • raises Not_found

    if the prover is not registered.

val list_provers : unit -> string list

List of registered provers

val register : string -> t -> unit

Register the prover with the given name.

  • raises Invalid_argument

    if the name is already used.

val p_E : t
val p_Eproof : t
val p_SPASS : t
val p_Zenon : t
val default : t list
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