Question on Arrays (with extensionality)

[aman-goel]

What types of domain/range are arrays with extensionality supported by Yices?

Does Yices support arrays with extensionality for Array type domain/range? For example, consider a custom sorts as follows:

(define-sort 2darray_int_type () (Array Int (Array Int Bool))) (define-sort 2darray_bv_type () (Array (_ BitVec 3) (Array (_ BitVec 2) Bool)))

Thanks

-- Aman

[BrunoDutertre]

Hi Aman,

The solver should be able to handle arbitrary arrays so that should work. Just remember that SMT-LIB 2 does not allow symbols (including sort names) to start with a digit.

[aman-goel]

Thanks Bruno.

I have another related question: Is there a way to specify constant arrays (arrays with all indices mapped to a default value) using Yices C API? This is especially useful when the domain of the array is infinite.

Thank you.

[ekiwi]

Is there a way to specify constant arrays (arrays with all indices mapped to a default value) using Yices C API?

I am wondering the same thing. I was trying to emulate constant arrays by declaring a lambda that always returns the default value. However I get an error that the context (I am using the default context) does not support lambdas.

My approach is something like:

term_t[] args = // create  a yices_new_variable for each index
term_t default = // this is the default expression which should be returned for any index
term_t const_array = yices_lambda(length(args), args, default) // this call results in an error about lambdas not being supported

Do you have any pointers as to which context configuration would support lambdas? Does my approach make sense for the problem at hand?

Note: The error message I am seeing is the same as the one described in this issue: https://github.com/SRI-CSL/yices2/issues/138