Module CallProver

module CallProver: sig .. end

Call external provers with TSTP

type 'a or_error = [ `Error of string | `Ok of 'a ]

type untyped = Libzipperposition.STerm.t

module A: Ast_tptp

Description of provers

module Prover: sig .. end

val name : Prover.t -> string

Name of the prover

Run provers

type result =

`\|`	`Unsat`
`\|`	`Sat`
`\|`	`Unknown`
`\|`	`Error of string`

val call : ?timeout:int ->
       ?args:string list ->
       prover:Prover.t ->
       untyped A.t list -> result or_error

Call the prover (if present) on the given problem, and return a result. Default timeout is 30.

val call_proof : ?timeout:int ->
       ?args:string list ->
       prover:Prover.t ->
       untyped A.t list ->
       (result * Trace_tstp.t) or_error

Call the prover, and also tries to parse a TSTP derivation, if the prover succeeded

val call_with_out : ?timeout:int ->
       ?args:string list ->
       prover:Prover.t ->
       untyped A.t list ->
       (result * string) or_error

Same as CallProver.call, but also returns the raw output of the prover

E-prover specific functions

module Eprover: sig .. end