Module CallProver.Eprover

module Eprover: sig .. end

type result = {

	`answer : szs_answer;`
	`output : string;`
	`decls : CallProver.untyped A.t Sequence.t option;`
	`proof : Trace_tstp.t option;`

}

type szs_answer =

`\|`	`Theorem`
`\|`	`CounterSatisfiable`
`\|`	`Unknown`

val string_of_answer : szs_answer -> string

val run_eproof : steps:int -> input:string -> result CallProver.or_error

Run Eproof_ram, and tries to read a proof back.

val run_eprover : ?opts:string list ->
       ?level:int ->
       steps:int ->
       input:string -> unit -> result CallProver.or_error

Runs E with the given input (optional verbosity level). The returned result will not contain a proof. opts is an additional list of command line options that will be given to E.

val discover : ?opts:string list ->
       steps:int ->
       CallProver.untyped A.t Sequence.t ->
       CallProver.untyped A.t Sequence.t CallProver.or_error

explore the surrounding of this list of declarations, returning the TPTP output of E

val cnf : ?opts:string list ->
       CallProver.untyped A.t Sequence.t ->
       CallProver.untyped A.t Sequence.t CallProver.or_error

Use E to convert a set of statements into CNF