Module ClauseContext

module ClauseContext: sig .. end

Clause context

A clause with a "hole" in it. Filling the whole with a term t is called "applying the context to t".

The point is to relate different applications of the same context.

type term = Logtk.Term.t

type subst = Logtk.Subst.t

type t

A context is represented as a regular array of literals, containing at least one specific variable x, paired with this variable x. Applying the context is a mere substitution

val compare : t -> t -> int

val equal : t -> t -> bool

val hash : t -> int

val make : Logtk.Literals.t -> var:Logtk.Term.var -> t

Make a context from a var and literals containing this var.
Raises Assert_failure if the variable isn't present in any literal

val extract : Logtk.Literals.t -> term -> t option

extract lits t returns None if t doesn't occur in lits. Otherwise, it creates a fresh var x, replaces t with x within lits, and returns the corresponding context. Basically, if extract lits t = Some c then apply c t = lits

val extract_exn : Logtk.Literals.t -> term -> t

Unsafe version of ClauseContext.extract.
Raises Invalid_argument if the term is not to be found within the lits

val trivial : Logtk.Literals.t -> term -> t

Trivial context, that contains 0 holes.

val apply : t -> term -> Logtk.Literals.t

apply c t fills the hole of c with the given term t. t and c share no free variables.

val apply_same_scope : t -> term -> Logtk.Literals.t

Same as ClauseContext.apply, but now variables from the context and variables from the term live in the same scope

val raw_lits : t -> Logtk.Literals.t

give access to the underlying literals. Careful not to depend on the variable's actual name.

val pp : t CCFormat.printer

Sets of contexts

module Set: CCSet.S  with type elt = t