module Make:
Create a new context
val ord : unit -> Libzipperposition.Ordering.t
current ordering on terms
val selection_fun : unit -> Selection.t
selection function for clauses
val set_selection_fun : Selection.t -> unit
val set_ord : Libzipperposition.Ordering.t -> unit
val signature : unit -> Libzipperposition.Signature.t
Current signature
val renaming : Libzipperposition.Substs.Renaming.t
Utils
val compare : Libzipperposition.FOTerm.t ->
Libzipperposition.FOTerm.t -> Libzipperposition.Comparison.t
Compare two terms
val select : Selection.t
val renaming_clear : unit -> Libzipperposition.Substs.Renaming.t
Obtain the global renaming. The renaming is cleared before
it is returned.
val lost_completeness : unit -> unit
To be called when completeness is not preserved
val is_completeness_preserved : unit -> bool
Check whether completeness was preserved so far
val add_signature : Libzipperposition.Signature.t -> unit
Merge the given signature with the context's one
val find_signature : Libzipperposition.ID.t -> Libzipperposition.Type.t option
Find the type of the given symbol
val find_signature_exn : Libzipperposition.ID.t -> Libzipperposition.Type.t
val declare : Libzipperposition.ID.t -> Libzipperposition.Type.t -> unit
Declare the type of a symbol (updates signature)
val on_new_symbol : (Libzipperposition.ID.t * Libzipperposition.Type.t) Signal.t
val on_signature_update : Libzipperposition.Signature.t Signal.t
Literals
module Lit: sig .. end