sig
type 'a or_error = [ `Error of string | `Ok of 'a ]
type untyped = Libzipperposition.STerm.t
module A = Ast_tptp
module Prover :
sig
type t = {
name : string;
command : string;
unsat : string list;
sat : string list;
}
val lookup : string -> CallProver.Prover.t
val list_provers : unit -> string list
val register : string -> CallProver.Prover.t -> unit
val p_E : CallProver.Prover.t
val p_Eproof : CallProver.Prover.t
val p_SPASS : CallProver.Prover.t
val p_Zenon : CallProver.Prover.t
val default : CallProver.Prover.t list
end
val name : CallProver.Prover.t -> string
type result = Unsat | Sat | Unknown | Error of string
val call :
?timeout:int ->
?args:string list ->
prover:CallProver.Prover.t ->
CallProver.untyped A.t list -> CallProver.result CallProver.or_error
val call_proof :
?timeout:int ->
?args:string list ->
prover:CallProver.Prover.t ->
CallProver.untyped A.t list ->
(CallProver.result * Trace_tstp.t) CallProver.or_error
val call_with_out :
?timeout:int ->
?args:string list ->
prover:CallProver.Prover.t ->
CallProver.untyped A.t list ->
(CallProver.result * string) CallProver.or_error
module Eprover :
sig
type result = {
answer : CallProver.Eprover.szs_answer;
output : string;
decls : CallProver.untyped A.t Sequence.t option;
proof : Trace_tstp.t option;
}
and szs_answer = Theorem | CounterSatisfiable | Unknown
val string_of_answer : CallProver.Eprover.szs_answer -> string
val run_eproof :
steps:int ->
input:string -> CallProver.Eprover.result CallProver.or_error
val run_eprover :
?opts:string list ->
?level:int ->
steps:int ->
input:string -> unit -> CallProver.Eprover.result CallProver.or_error
val discover :
?opts:string list ->
steps:int ->
CallProver.untyped A.t Sequence.t ->
CallProver.untyped A.t Sequence.t CallProver.or_error
val cnf :
?opts:string list ->
CallProver.untyped A.t Sequence.t ->
CallProver.untyped A.t Sequence.t CallProver.or_error
end
end