Is there a compliant way to let z3 recognize a term with a polymorphic datatype's tester well sorted in general?

Question

As pointed out in this issue, Z3 cannot handle the following code correctly, meaning that Z3 reports the error (error "line 6 column 15: ambiguous function declaration reference, provide full signature to disambiguate (<symbol> (<sort>*) <sort>) X").

(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes ((S 1)) ((par (T) ((X (getX T))))))
(declare-fun x () (S Int))
(define-fun  y () (S (S Int)) (X x))
(assert ((_ is X) y))
(check-sat)
(get-model)

Regarding the comments on the issue, the following alternatives for line 6 solve the situation.

• (assert (is-X y))
• (assert ((_ is (X ((S Int)) (S (S Int)))) y))

However, neither is compliant with the SMT-Lib standard. The second alternative is said to be the SMT-Lib syntax in the comments, but actually not. It doesn't follow the syntax of SMT-Lib 2.6, and other SMT solver, e.g., cvc5, doesn't accept the form.

Now, the question is the title. Is there an SMT-Lib compliant alternative? Fortunately, cvc5 accepts the first alternative. So, as far as we use Z3 or cvc5, it would suffice. However, it isn't SMT-Lib compliant, and I'm curious about other solvers.

Answer 1

Unfortunately I don't think the state of affairs has changed since that issue was discussed. The "most portable" way is to do what Nikolaj suggested:

(define-sort S1I () (S Int))
(define-sort S2I () (S (S Int)))

but that introduces extra declarations that shouldn't be needed. Note that with upcoming SMTLib3, all of this will become (possibly?) easier since the language itself will allow for much better types and polymorphism.

When faced with this problem, I ended up using the SMTLib syntax for CVC, and the extended version for z3. I don't think there's a solution that can handle everything out of the box.