const-array

[LeventErkok]

In version 2.6 of the document (https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf), there's a reference to const-array on page 31.

I don't see any other reference to const-array anywhere else; and neither z3 nor cvc5 accept this as constant.

However, both z3 and cvc5 work fine with const

Is const-array really part of the language? If not, let's remove it from the text, replacing it with const. If so, I guess I'll have to file issues with at least z3 and cvc5 so they can support it to be compliant.

[Gbury]

As far as I'm aware, neither const nor const-array are part of the language, or rather, neither is present/mentioned in the ArraysEx theory (xsee https://smt-lib.org/theories-ArraysEx.shtml ) nor any logics that includes that theory, but I may have missed something, so one of the maintainers would probably know better.

I guess the array-const in the example is leftover from older versions where it may have been considered for inclusion ?

[fontainep]

Hi Levent and Guillaume, indeed, as pointed out by Guillaume, neither are part of the language, but they are used as illustration for the usage of the (as ...) construct, just like "cons" and "nil" in the line above. It is not a left-over. Future versions of the SMT-LIB array theory might include such an operator. We added a clarification in the upcoming reference document: https://smt-lib.org/papers/smt-lib-reference-v2.7-draft.pdf Thanks for your feedback! Can I close the issue?

[barrettcw]

Actually, let's leave the issue open as I have on my to-do list to do an initial draft of an array theory including the const-array operator. I've assigned myself.