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.
typeterm =
Logtk.Term.t
typesubst =
Logtk.Subst.t
type
t
x
, paired with this variable x
.
Applying the context is a mere substitutionval compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val make : Logtk.Literals.t -> var:Logtk.Term.var -> t
Assert_failure
if the variable isn't present in any literalval 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
ClauseContext.extract
.Invalid_argument
if the term is not to be found within the litsval trivial : Logtk.Literals.t -> term -> t
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
ClauseContext.apply
, but now variables from the context and variables
from the term live in the same scopeval raw_lits : t -> Logtk.Literals.t
val pp : t CCFormat.printer
module Set:CCSet.S
with type elt = t