Module `Ctx.Make`

Create a new context

Parameters

X : PARAMETERS

Signature

val sk_ctx : unit -> Logtk.Skolem.ctx
val ord : unit -> Logtk.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 : Logtk.Ordering.t -> unit
val signature : unit -> Logtk.Signature.t: Current signature

val renaming : Logtk.Subst.Renaming.t

Utils

val compare : Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t: Compare two terms

val select : Selection.t
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 : Logtk.Signature.t -> unit: Merge the given signature with the context's one

val find_signature : Logtk.ID.t -> Logtk.Type.t option: Find the type of the given symbol

val find_signature_exn : Logtk.ID.t -> Logtk.Type.t

Unsafe version of find_signature.

raises Not_found: for unknown symbols

val declare : Logtk.ID.t -> Logtk.Type.t -> unit: Declare the type of a symbol (updates signature)

val declare_syms : (Logtk.ID.t * Logtk.Type.t) list -> unit: Declare multiple symbols (more efficient that calling declare function incrementally)

val on_new_symbol : (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
val on_signature_update : Logtk.Signature.t Logtk.Signal.t
val set_injective_for_arg : Logtk.ID.t -> int -> unit
val is_injective_for_arg : Logtk.ID.t -> int -> bool

Literals

module Lit : sig ... end