Module Libzipperposition.ClauseContextSource

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.

Sourcetype term = Logtk.Term.t
Sourcetype subst = Logtk.Subst.t
Sourcetype 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

Sourceval compare : t -> t -> int
Sourceval equal : t -> t -> bool
Sourceval hash : t -> int

Make a context from a var and literals containing this var.

Sourceval 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

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

Unsafe version of extract.

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

Trivial context, that contains 0 holes.

Sourceval 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.

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

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

Sourceval raw_lits : t -> Logtk.Literals.t

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

Sets of contexts

Sourcemodule Set : CCSet.S with type elt = t