sig
type 'a or_error = [ `Error of string | `Ok of 'a ]
type t
type clause = Reasoner.clause
val empty : Prover.t
val reasoner : Prover.t -> Reasoner.t
val signature : Prover.t -> Reasoner.ty Libzipperposition.ID.Map.t
val add :
Prover.t -> Reasoner.clause -> Prover.t * Reasoner.consequence Sequence.t
val add_fact :
Prover.t -> Reasoner.fact -> Prover.t * Reasoner.consequence Sequence.t
val add_fo_clause :
Prover.t ->
Encoding.foclause -> Prover.t * Reasoner.consequence Sequence.t
module Seq :
sig
val to_seq : Prover.t -> Reasoner.clause Sequence.t
val of_seq :
Prover.t ->
Reasoner.clause Sequence.t ->
Prover.t * Reasoner.consequence Sequence.t
end
val of_ho_ast :
Prover.t ->
Libzipperposition_parsers.Ast_ho.t Sequence.t ->
(Prover.t * Reasoner.consequence Sequence.t) Prover.or_error
val parse_file :
Prover.t ->
string -> (Prover.t * Reasoner.consequence Sequence.t) Prover.or_error
end