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