Disambiguating sorts with "as"

26 views
Skip to first unread message

Calvin Loncaric

unread,
Feb 27, 2021, 11:23:29 PM2/27/21
to smt...@googlegroups.com
The SMT-LIB 2.6 standard requires clients and solvers to disambiguate function symbols that have ambiguous sorts (section 3.6.4 "Well-sortedness requirements").

However, the standard contradicts itself about how to do this, and different solvers seem to have interpreted it in different ways. The text states "every occurrence of an ambiguous function symbol f in a term must occur as a qualified identifier of the form (as f \sigma) where \sigma is the intended output sort of that occurrence". Then, in the example immediately below, it shows the term (as (const-array 0.0) (Array Int Real)). I believe the text implies that the term should have been written ((as const-array (Array Int Real)) 0.0) instead.

In practice, the solvers CVC4 and Z3 seem to have interpreted this section in different ways. Consider these definitions, which both solvers accept:

(declare-datatypes ((Either 2)) (
    (par (L R) (
        (Left (get-left L))
        (Right (get-right R))))))

(declare-const x (Either Int Int))

CVC4 accepts this assertion, and Z3 does not:

(assert (distinct x (as (Right 10) (Either Int Int))))

By contrast, Z3 accepts this assertion, and CVC4 does not:

(assert (distinct x ((as Right (Either Int Int)) 10)))

So CVC4 is consistent with the example and Z3 is consistent with the text. Which solver is in the right?

(I am working on a tool that sometimes generates assertions like the ones above. I would like to be able to use either solver, but right now CVC4 rejects the tool's output because the tool takes Z3's approach to disambiguation. For now I can work around it by blasting away all the parametric datatype declarations into uniquely-named sorts and constructors, but it's frustrating to have to re-implement functionality that I know both solvers are capable of.)

Calvin Loncaric

unread,
May 4, 2021, 4:15:41 PM5/4/21
to smt...@googlegroups.com
A quick note for anyone following along at home:

CVC4 1.8 accepts only the second syntax, the same as Z3:

(assert (distinct x ((as Right (Either Int Int)) 10)))

It took some digging to find, but I think this is the pull request that fixed it: https://github.com/CVC4/CVC4/pull/3111

I had been using CVC4 1.7 when I wrote my original email, even though CVC4 1.8 was released months earlier in June 2020. I installed CVC4 through Homebrew, and the Homebrew package wasn't updated to 1.8 until recently.

Also, there is now a new release of the SMT-LIB standard. Section 3.6.4 hasn't been revised, so it seems to me that the disambiguation ambiguity remains.

Cesare Tinelli

unread,
May 12, 2021, 1:59:36 PM5/12/21
to smt...@googlegroups.com

Calvin,

Thanks for pointing out the problem in the document. The example in Section 3.6.4 explaining the use of 'as' is indeed incorrect.

Not fixing the example in release 2021-04-02 was an oversight which we have now fixed with a new release: 2021-05-12.

To recap, 'as' takes two arguments: an ambiguous function symbol f (not a term) and the intended return type for f.

Both Z3 and CVC4 1.8 are compliant with respect to this specification. Older versions of CVC4 were not.

Best,

Cesare, also for Clark and Pascal

On 4 May 2021, at 13:16, Calvin Loncaric wrote:

A quick note for anyone following along at home:

CVC4 1.8 accepts only the second syntax, the same as Z3:

(assert (distinct x ((as Right (Either Int Int)) 10)))

It took some digging to find, but I think this is the pull request that
fixed it: https://github.com/CVC4/CVC4/pull/3111

I had been using CVC4 1.7 when I wrote my original email, even though CVC4
1.8 was released months earlier in June 2020. I installed CVC4 through
Homebrew, and the Homebrew package wasn't updated to 1.8 until recently


.

Also, there is now a new release of the SMT-LIB standard

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CABf5HMg8c5PVqN5jjEE2oTEnymAzU%3DW%3D3P8wKU0hSBpeOa-B1g%40mail.gmail.com.

Calvin Loncaric

unread,
May 14, 2021, 4:38:32 AM5/14/21
to smt...@googlegroups.com
Fantastic, thank you for the clarification. :)

--
Calvin


Reply all
Reply to author
Forward
0 new messages