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

[Delcypher]

Sorry forwarding to smt-lib and smt-comp using the right e-mail
address this time...

Hi All,

I thought I'd mention a few issues I've had in the past with SMT-LIBv2
and I was wondering if they were resolved in the draft 2.5 spec.

* Sometimes I've found it necessary to use a mixture of logics. For example I
wanted to use Ints and arrays of bitvectors. (I might do conversions
using the int2bv
and bv2int functions although I think these might be Z3 extensions). There is
no logic I can specific in this case. For Z3 I just don't specify the
logic and for CVC4 I just use

(set-logic: ALL_SUPPORTED)

Is there any plan to add something like "ALL_SUPPORTED" to the
standard? I couldn't see anything obvious about it in the draft.

* Non standard (get-model) output. I seem to remember that the output
of (get-model) was not standardised so different solvers can give
completely different outputs making it difficult to parse.
Glancing at the spec I see for (get-model) to draft says (declare-fun)
or (declare-fun-rec) is now emitted so I take it this is the
standardisation of the model syntax?

* 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?

* Representation of bitvector constants in models.
There are three different ways to represent bitvector constants in
SMTLIBv2. I recall trying to write code to parse the response from
calling something like...

```
(get-value ( (select unnamed_1 (_ bv0 32) ) ) )
```

being complicated by the fact that different solvers use different
representations for constant bitvectors. In fact in some cases the
representation is mixed (e.g. this output from Z3)

```
(((select unnamed_1 (_ bv0 32) ) #x20))
```

Is there any interest in standardising the representation of bitvector
constants used in outputted models?


Thanks,
Dan.