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
E-prover specific functions
module Eprover: sig
.. end