sig
module E : Env.S
module C = E.C
type lemma = C.t
type axiom = Libzipperposition.ID.t * MetaProverState_intf.term list
type theory = Libzipperposition.ID.t * MetaProverState_intf.term list
type rewrite =
(Libzipperposition.FOTerm.t * Libzipperposition.FOTerm.t) list
type pre_rewrite =
(MetaProverState_intf.term * MetaProverState_intf.term) list
module Result :
sig
type t
val lemmas :
MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.lemma list
val theories :
MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.theory list
val axioms :
MetaProverState_intf.S.Result.t -> MetaProverState_intf.S.axiom list
val rewrite :
MetaProverState_intf.S.Result.t ->
MetaProverState_intf.S.rewrite list
val pre_rewrite :
MetaProverState_intf.S.Result.t ->
MetaProverState_intf.S.pre_rewrite list
val print : Format.formatter -> MetaProverState_intf.S.Result.t -> unit
end
val results : unit -> MetaProverState_intf.S.Result.t
val pop_new_results : unit -> MetaProverState_intf.S.Result.t
val theories : MetaProverState_intf.S.theory Sequence.t
val reasoner : Libzipperposition_meta.Reasoner.t
val prover : Libzipperposition_meta.Prover.t
val on_theory : MetaProverState_intf.S.theory Signal.t
val on_lemma : MetaProverState_intf.S.lemma Signal.t
val on_axiom : MetaProverState_intf.S.axiom Signal.t
val on_rewrite : MetaProverState_intf.S.rewrite Signal.t
val on_pre_rewrite : MetaProverState_intf.S.pre_rewrite Signal.t
val parse_theory_file :
string -> MetaProverState_intf.S.Result.t MetaProverState_intf.or_error
val parse_theory_files :
string list ->
MetaProverState_intf.S.Result.t MetaProverState_intf.or_error
val scan_clause : C.t -> MetaProverState_intf.S.Result.t
val setup : unit -> unit
end