Datatype declarations: Trying to get cvc4 and z3 to agree

[LeventErkok]

@ajreynol

I'm having issues generating code that is good for both z3 and cvc4. I raised this in the cvc4 repo, and it seems perhaps this is a z3 problem:

cvc5/cvc5#2832

The crux of the issue seems to be the following:

(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes ((SBVEither 2)) ((par (T1 T2)
                                    ((left_SBVEither  (get_left_SBVEither  T1))
                                     (right_SBVEither (get_right_SBVEither T2))))))

(declare-fun s0 () (_ BitVec 8))
(define-fun s1 () (SBVEither (_ BitVec 8) (_ BitVec 8)) (as (left_SBVEither s0) (SBVEither (_ BitVec 8) (_ BitVec 8))))
(check-sat)
(get-model)

CVC4 is OK with this, but z3 says:

(error "line 8 column 61: invalid indexed identifier, '_' expected")

I think CVC4 is right here; but I've been bitten by these syntax problems before so would appreciate some feedback.

[NikolajBjorner]

SMTLIB 2.6 spec says on page 95/96:

    <identifier> ::= <symbol> | ( _ <symbol> <index>+ )
   <qual_identifier> ::= <identifier> | ( as <identifier> <sort> )

that, is, whatever comes after "as" is expected to be a symbol or something that is of the form ( _ ...).
Z3's parser is pedantic about this.

[ajreynol]

Nikolaj is right, as should only be applied to identifiers according to the standard.

I believe the right syntax for your example is (somewhat strangely):

(set-logic ALL)
(declare-datatypes ((SBVEither 2)) ((par (T1 T2)
                                    ((left_SBVEither  (get_left_SBVEither  T1))
                                     (right_SBVEither (get_right_SBVEither T2))))))

(declare-fun s0 () (_ BitVec 8))
(define-fun s1 () (SBVEither (_ BitVec 8) (_ BitVec 8)) ((as left_SBVEither (SBVEither (_ BitVec 8) (_ BitVec 8))) s0))
(check-sat)

In other words, the function symbol left_SBVEither should be annotated with its result sort (SBVEither (_ BitVec 8) (_ BitVec 8)). This is mentioned on page 27 of SMTLIB 2.6:

To simplify sort checking, a function symbol in a term can be annotated with one of its result sorts σ.

where the key word is "result" here.

Interestingly, both CVC4 and Z3 do not correctly parse the version above. Z3 gives the errors:

(error "line 3 column 20: invalid sort parameter, symbol or ')' expected")
(error "line 8 column 19: unknown sort 'SBVEither'")

[NikolajBjorner]

I am willing to believe that there are legal cases that Z3 doesn't parse,
but this particular example works with the current main branch.

[ajreynol]

You're right, I was using an older version.

[LeventErkok]

Thanks @ajreynol

It is indeed bizarre that you get to annotate "with one of its result sorts σ." I'm not sure what "one of" refers to in this sentence. The standard seems to be quite vague about this; but I trust I can use the translation you described and hopefully CVC4 and z3 will both accept the input.

I'm closing this ticket as there doesn't seem to be a z3 actionable item left for it. Thanks!