module X = Shostak.Combinemodule MX = Shostak.MXHmodule SX = Shostak.SXHmodule HX = Shostak.HXmodule L = Xliteralmodule LR = AltErgoLib.Uf.LXmodule HLR : sig ... endval assume_nontrivial_eqs :
X.r Sig_rel.input list ->
X.r Sig_rel.input list ->
X.r Sig_rel.fact listassume_nontrivial_eqs eqs la can be used by theories to remove from the equations eqs both duplicates and those that are implied by the assumptions in la.
type delayed_fn =
Uf.t ->
Symbols.operator ->
Expr.t list ->
(X.r * Explanation.t) optionval delay1 :
(Uf.r -> 'a) ->
('b -> 'c) ->
('d -> 'a -> 'b option) ->
Uf.t ->
'd ->
Expr.t list ->
('c * Explanation.t) optionval delay2 :
(Uf.r -> 'a) ->
('b -> 'c) ->
('d -> 'a -> 'a -> 'b option) ->
Uf.t ->
'd ->
Expr.t list ->
('c * Explanation.t) optionmodule Delayed : sig ... endThe 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.
module XComparable : sig ... endImplementation of the ComparableType interface for semantic values.