Previous  Up  

Module Prover

module Prover: sig .. end

Meta-Prover


type 'a or_error = [ `Error of string | `Ok of 'a ] 
type t
Meta-prover
type clause = Reasoner.clause 
val empty : t
Fresh meta-prover (using default plugins' signature)
val reasoner : t -> Reasoner.t
The inner reasoner, holding a set of clauses and facts
val signature : t -> Reasoner.ty Libzipperposition.ID.Map.t
Current signature
val add : t -> Reasoner.clause -> t * Reasoner.consequence Sequence.t
Add a clause
val add_fact : t -> Reasoner.fact -> t * Reasoner.consequence Sequence.t
val add_fo_clause : t -> Encoding.foclause -> t * Reasoner.consequence Sequence.t
Add a first-order clause (as "holds" predicate)
module Seq: sig .. end

IO

val of_ho_ast : t ->
       Libzipperposition_parsers.Ast_ho.t Sequence.t ->
       (t * Reasoner.consequence Sequence.t) or_error
Add the given declarations to the meta-prover. In case of type inference failure, or other mismatch, an error is returned.
val parse_file : t ->
       string -> (t * Reasoner.consequence Sequence.t) or_error
Attempt to parse file using Libzipperposition_parsers.Parse_ho and add the parsed content to the prover