Up  

Module type MetaProverState_intf.S

module type S = sig .. end
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
Rewrite system
type pre_rewrite = (MetaProverState_intf.term * MetaProverState_intf.term) list

Result: Feedback from the meta-prover


module Result: sig .. end

Interface to the Meta-prover


val results : unit -> Result.t
Sum of all results obtained so far
val pop_new_results : unit -> Result.t
Obtain the difference between last call to pop_new_results p and results p, and pop this difference. ignore (pop_new_results p); pop_new_results p always returns the empty results
val theories : theory Sequence.t
List of theories detected so far
val reasoner : Libzipperposition_meta.Reasoner.t
Meta-level reasoner (inference system)
val prover : Libzipperposition_meta.Prover.t
meta-prover
val on_theory : theory Signal.t
val on_lemma : lemma Signal.t
val on_axiom : axiom Signal.t
val on_rewrite : rewrite Signal.t
val on_pre_rewrite : pre_rewrite Signal.t
val parse_theory_file : string -> Result.t MetaProverState_intf.or_error
Update prover with the content of this file, returns the new results or an error
val parse_theory_files : string list -> Result.t MetaProverState_intf.or_error
Parse several files
val scan_clause : C.t -> Result.t
Scan a clause for axiom patterns, and save it

Inference System


val setup : unit -> unit
setup () registers some inference rules to E