Module Logtk.Unif_constr

Unification Constraint

A constraint is a pair of (scoped) terms that cannot be unified immediately (because they belong to some theory, for example).

We keep them in a separate constraint that will become a negative literal t ≠ u, on which the theory can then act.

type term = InnerTerm.t
type t = private {
  1. t1 : term;
  2. sc1 : Scoped.scope;
  3. t2 : term;
  4. sc2 : Scoped.scope;
  5. tags : Proof.tag list;
}

A constraint delayed because unification for this pair of terms is not syntactic

val make : tags:Proof.tag list -> term Scoped.t -> term Scoped.t -> t
val tags : t -> Proof.tag list
val apply_subst : Subst.Renaming.t -> Subst.t -> t -> term * term

Apply a substitution to a delayed constraint

val apply_subst_l : Subst.Renaming.t -> Subst.t -> t list -> (term * term) list

Apply a substitution to delayed constraints

module FO : sig ... end
include Interfaces.HASH with type t := t
include Interfaces.EQ with type t := t
val equal : t -> t -> bool
val hash : t -> int
include Interfaces.ORD with type t := t
val compare : t -> t -> int
include Interfaces.PRINT with type t := t
val to_string : t -> string