Inspecting uninterpreted sorts

[erk...@gmail.com]

I'm looking for a uniform way to access the details of an uninterpreted sort in a model. Let's say I have the script:

(set-logic ALL)
(declare-sort A 0)
(declare-fun a () A)
(declare-fun b () A)
(assert (distinct a b))
(check-sat)
(get-model)

I'm interested in finding out what kind of a model A has. z3 says:

sat
(
  ;; universe for A:
  ;;   A!val!1 A!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun A!val!1 () A)
  (declare-fun A!val!0 () A)
  ;; cardinality constraint:
  (forall ((x A)) (or (= x A!val!1) (= x A!val!0)))
  ;; -----------
  (define-fun b () A
    A!val!1)
  (define-fun a () A
    A!val!0)
)

cvc5 says:

sat
(
; cardinality of A is 2
; rep: (as @A_0 A)
; rep: (as @A_1 A)
(define-fun a () A (as @A_0 A))
(define-fun b () A (as @A_1 A))
)

So, if I "squint" right, they are both telling me:

(declare-datatype A ((A0) (A1)))

But there does not seem to be a command in SMTLib just to receive the description of A (get-value doesn't take sorts), to have a standard interface for upstream tools to utilize.

Is this an oversight in SMTLib? Is there a command I missed? Or, is the problem more complicated: Perhaps I'm overlooking some detail that makes designing a standard interface for accessing uninterpreted-sorts in a model impossible?

It might even be sufficient if there was a way to extract the info that A is an enumeration of some cardinality. Something like, after getting sat, we might be allowed to say:

(get_cardinality A)

--> 2

would this be useful if formalized?

Cheers,

-Levent.