Allow `const` arrays with symbolic elements

[yav]

Consider the following specification fragment:

(declare-const x Int)                                                            
(assert (= (select ((as const (Array Int Int)) x) 0) 0)) 

This results in:

(error "Parse Error: test.cvc5:2.49: invalid argument 'x' for 'val', expected a value")

It would appear that CVC5 wants the values of the constant arrays to be a value, but x is not one. This works as expected in Z3.

This happens with version 1.2.0 of CVC5.

[benjaminfjones]

Const array support has baffled me in the past. It seems not to be part of the SMT-LIB standard, although there is an oblique reference to it one example in the standards doc https://smt-lib.org/papers/smt-lib-reference-v2.6-r2024-09-20.pdf section 3.6.4.

Here's a different formulation that is at least accepted by both z3 and cvc5, but in my testing only z3 can solve it. cvc5 1.1.2 (and some other previous versions) returns unknown immediately. @ajreynol probably has a good idea what cvc5 options would help with the quantified assertion.

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

(declare-const x Int)
(declare-const const-array-x (Array Int Int))

(assert (forall ((i Int)) (= (select const-array-x i) x)))
(assert (= (select const-array-x 0) 0))

(check-sat)
(get-value (const-array-x x))

ps. Hi Yavor!

[barrettcw]

Constant arrays are not part of the SMT-LIB standard, but it is something we intend to add soon, as many solvers do indeed support them. Unfortunately, cvc5 supports only a narrow case. The constants must be values, and the user is not allowed to create write-chains between constant arrays. This is also something we hope to address in the future.