Module AltErgoLib.Rel_utils

module X = Shostak.Combine
module MX = Shostak.MXH
module SX = Shostak.SXH
module HX = Shostak.HX
module L = Xliteral
module LR = AltErgoLib.Uf.LX
module HLR : sig ... end
val assume_nontrivial_eqs : X.r Sig_rel.input list -> X.r Sig_rel.input list -> X.r Sig_rel.fact list

assume_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) option
val delay1 : (Uf.r -> 'a) -> ('b -> 'c) -> ('d -> 'a -> 'b option) -> Uf.t -> 'd -> Expr.t list -> ('c * Explanation.t) option
val delay2 : (Uf.r -> 'a) -> ('b -> 'c) -> ('d -> 'a -> 'a -> 'b option) -> Uf.t -> 'd -> Expr.t list -> ('c * Explanation.t) option
module Delayed : sig ... end

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.

module XComparable : sig ... end

Implementation of the ComparableType interface for semantic values.