AltErgoLib.Usemodule SA : Set.S with type elt = Expr.t * Explanation.ttype r = Shostak.Combine.rval src : Logs.srcval empty : tval find : r -> t -> Expr.Set.t * SA.tval add : r -> (Expr.Set.t * SA.t) -> t -> tval print : t -> unitval congr_add : t -> r list -> Expr.Set.tval congr_close_up : t -> r -> r list -> Expr.Set.t * SA.t