Module Logtk_parsers.CallProver

Call external provers with TSTP (Old)

type 'a or_error = ('a, string) CCResult.t
type untyped = Logtk.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 call, but also returns the raw output of the prover

E-prover specific functions

module Eprover : sig ... end