Previous  Up  Next

Module CallProver.Prover

module Prover: sig .. end
type t = {
   name : string; (*
name of the prover
*)
   command : string; (*
command to call prover
*)
   unsat : string list; (*
prover returned unsat (possible outputs)
*)
   sat : string list; (*
prover returned sat (possible outputs)
*)
}
data useful to invoke a prover. The prover must read from stdin. The command is interpolated using Buffer.add_substitude, with the given patterns: 


val lookup : string -> t
Lookup a prover by its name.
Raises Not_found if the prover is not registered.
val list_provers : unit -> string list
List of registered provers
val register : string -> t -> unit
Register the prover with the given name.
Raises Invalid_argument if the name is already used.
val p_E : t
val p_Eproof : t
val p_SPASS : t
val p_Zenon : t
val default : t list