package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module CallProver.ProverSource

Sourcetype 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
Sourceval lookup : string -> t

Lookup a prover by its name.

  • raises Not_found

    if the prover is not registered.

Sourceval list_provers : unit -> string list

List of registered provers

Sourceval register : string -> t -> unit

Register the prover with the given name.

Sourceval p_E : t
Sourceval p_Eproof : t
Sourceval p_SPASS : t
Sourceval p_Zenon : t
Sourceval 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