module ClauseContext:`sig`

..`end`

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

**Raises**

`ClauseContext.extract`

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

module Set:`CCSet.S`

`with type elt = t`