Parametric ADT

[mgudemann]

For these constraints

(set-logic ALL)
(set-option :produce-models true)

(declare-datatypes ((Ptr 1)) ((par (T) ((null_ptr)))))

( declare-datatypes
    (
        ( L
            0
        )
    )
    (
        (
            ( mk-L
                ( val
                    ( _
                        BitVec
                        8
                    )
                )
                ( e
                    ( Ptr
                        L
                    )
                )
            )
        )
    )
)
(declare-const l L)

(assert (= l (mk-L (_ bv0 8) (as null_ptr (Ptr L)))))

(check-sat)
(get-value (l))

Princess reports (error "Sort L not declared") while both Z3 and CVC5 correctly report sat.
What are the restrictions of using ADTs?

[pruemmer]

Although Z3 and cvc5 might accept this input, I don't think that the second declare-datatypes command is a valid declaration in SMT-LIB 2.7. The standard says on page 65 for declare-datatypes: [...] (iv) τj is a sort term that contains no occurrences of δ1, . . . , δn below its top symbol [...]

https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-02-05.pdf

So (Ptr L) cannot be used as the sort of a field.

I will add a proper error message for this.

We are planning to eventually support declarations of this kind; for instance, it would be convenient to be able to declare infinitely-branching trees using arrays, but currently this does not work yet.

[mgudemann]

I see your point, thanks for the explication, the error message was indeed not too helpful in this case. CVC5 reads the file even with --strict-parsing, so I did not think that it was not SMT-LIB2 compliant.

[xywang18]

Is there any plan to support this recursive ADT case? I meet this issue too. Thank you very much