[SMT-LIB] [SMT-COMP] Draft of SMT-LIB 2.5: request for feedback

[Florian Lapschies]

On 01/15/2015 01:40 PM, Delcypher wrote:
> * Calling get-value on arrays. I remember a few years ago using
> (get-value) to retrieve the values of arrays of bitvectors. I remember
> running into a few issues. Let's say I declare the following
>
> ```
> (declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
> ```
>
> If I later did
>
> ```
> (get-value unnamed_1)
> ```
>
> the response I got was not consistent between solvers. IIRC correctly
> SONOLAR gave a list of relevant assignments
>
> ```
> (select  unnamed #b00000000000000000000000000000000) #b00011011)
> (select  unnamed #b00000000000000000000000000000001) #b00011011)
> ...
> ```
>
> where as other solvers outputted things relating to their model. For
> example Z3 would output something like
>
> ```
> ((unnamed_1 (_ as-array k!0)))
> ```
>
> which isn't very useful. Is there any intent to standardise what
> calling (get-value) on an array type should do?
>
>
Dear SMTLIB community,

as a member of the sonolar team I must say that our solver's output

(((select a #b00000001) #b00101010)
((select a #b00000010) #b00000001))

in response to

(declare-fun a () (Array (_ BitVec 8) (_ BitVec 8)))
(assert (= (_ bv1 8) (select a (_ bv2 8))))
(assert (= (_ bv42 8) (select a (_ bv1 8))))
(check-sat)
(get-value (a))

is not strictly correct wrt. the standard, since the sort of the 
returned value must be the same as the sort of the corresponding term in 
the get-value command.
We simply found it easier to use and implement than introducing new 
auxiliary functions.

Best regards,
Florian