The Delayed module can be used by relations that deal with partially interpreted functions. It will introduce the equalities between a function and its interpreted value as soon as the value of its arguments become known.
To avoid issues with eager splitting, functions are not computed on case splits unless model generation is enabled.
val create :
is_ready:(X.r -> bool) ->
(Symbols.operator -> delayed_fn option) ->
tcreate ~is_ready dispatch creates a new delayed structure for the symbols handled by dispatch.
The predicate is_ready is used to prevent from computing the functions of dispatch before we actually know their arguments.
dispatch must be pure.
add env uf r t checks whether the term t is a delayed function and if so either adds it to the structure or evaluates it immediately if possible, in which case a new equality with corresponding explanation is returned.
r must be the semantic value associated with t.
add can be called directly with the arguments passed to a relation's add function.
val update :
t ->
Uf.t ->
X.r ->
X.r ->
Th_util.lit_origin ->
X.r Sig_rel.input list ->
X.r Sig_rel.input listupdate env uf r orig eqs checks whether r is an argument of a registered delayed function and, if so, tries to compute the corresponding delayed function. If all the function's arguments are constants, the resulting equality is accumulated into eqs.
update should be called with the left-hand side of Eq literals that are assumed by a relation.
val assume : t -> Uf.t -> X.r Sig_rel.input list -> t * X.r Sig_rel.resultassume is a simple wrapper for update that is compatible with the assume signature of a relation.
val iter_delayed : (X.r -> Symbols.operator -> Expr.t -> unit) -> t -> unititer_delayed f t iterates on the delayed applications of t.