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