sig
type term = Libzipperposition.TypedSTerm.t
type ty = Reasoner.term
type property = Reasoner.term
type fact = Reasoner.term
val property_ty : Libzipperposition.TypedSTerm.t
val property_id : Libzipperposition.ID.t
exception Error of string
module Clause :
sig
type t = { head : Reasoner.term; body : Reasoner.term list; }
val rule : Reasoner.term -> Reasoner.term list -> Reasoner.Clause.t
val fact : Reasoner.term -> Reasoner.Clause.t
val is_fact : Reasoner.Clause.t -> bool
val pp : t CCFormat.printer
val to_string : t -> string
val equal : t -> t -> bool
val hash_fun : t -> CCHash.state -> CCHash.state
val hash : t -> int
val compare : t -> t -> int
module Seq :
sig
val terms : Reasoner.Clause.t -> Reasoner.term Sequence.t
val vars :
Reasoner.Clause.t ->
Reasoner.ty Libzipperposition.Var.t Sequence.t
end
end
type clause = Reasoner.Clause.t
module Proof :
sig
type t =
Axiom
| Resolved of Reasoner.fact Reasoner.Proof.with_proof *
Reasoner.clause Reasoner.Proof.with_proof
and 'a with_proof = { conclusion : 'a; proof : Reasoner.Proof.t; }
val facts : Reasoner.Proof.t -> Reasoner.fact Sequence.t
val rules : Reasoner.Proof.t -> Reasoner.clause Sequence.t
end
type proof = Reasoner.Proof.t
type consequence = Reasoner.fact * Reasoner.proof
type t
val empty : Reasoner.t
val add :
Reasoner.t ->
Reasoner.clause -> Reasoner.t * Reasoner.consequence Sequence.t
val add_fact :
Reasoner.t ->
Reasoner.fact -> Reasoner.t * Reasoner.consequence Sequence.t
module Seq :
sig
val of_seq :
Reasoner.t ->
Reasoner.clause Sequence.t ->
Reasoner.t * Reasoner.consequence Sequence.t
val to_seq : Reasoner.t -> Reasoner.clause Sequence.t
val facts : Reasoner.t -> Reasoner.fact Sequence.t
end
end