Understanding solver-generated function symbols other than abstract values.

[Siyuan Chen]

Dear SMT community,

I have a question about solver-generated symbols.

There is an example of solver-generated constant and function symbols in p.31.

```
; const - array takes a value v and
; returns an array storing v at all positions
(= a (( as const - array ( Array Int Real )) 0.0))

(select (as @a1 ( Array Int Int )) 3)
```

In my understanding,

`@a1` is a solver-generated constant (and it is also an abstract value),

 `const-array` is a solver-generated function symbol other than abstract values (because abstract values must be constant symbols, see p.83)


However, in p.65, the `(get-value (t1...tn))` section, it says that

> The values are returned as a sequence of pairs of the form ((t1 v1) . . .  (tn vn)).
> The terms v1, . . . , vn are allowed to contain symbols not in the current signature only if
> they are abstract values, i.e., constant symbols starting with the special character @.

The question is that can `v1` contain solver-generated function symbols? like the `const-array`?

For example, in z3 or cvc4

```
$ z3 -in
(set-info :smt-lib-version 2.6)
(set-logic QF_AX)
(set-option :produce-models true)
(declare-const a (Array Bool Bool))
(check-sat)
sat
(get-value (a))
((a ((as const (Array Bool Bool)) false)))
```

As you see, the result of `get-value` contains  `const`, which is a solver-generated function symbol other than abstract values.

Should we think it violates the SMT-LIB standard?

The other question is that does the SMT-LIB standard allow those solver-generated function symbols be used in the input formulas? (The program in p.31 seems to allow.)  

However,

```
$ z3 -in
(set-info :smt-lib-version 2.6)
(set-logic QF_AX)
(set-option :produce-models true)
(define-fun array_0 () (Array Bool Bool) ((as const (Array Bool Bool)) false))
(error "line 3 column 76: unknown constant const (Bool) (Array Bool Bool) ")
```

```
$ z3 -in
(set-info :smt-lib-version 2.6)
(set-logic ALL)
(set-option :produce-models true)
(define-fun array_0 () (Array Bool Bool) ((as const (Array Bool Bool)) false))
(check-sat)
sat
(get-model)
(
  (define-fun array_0 () (Array Bool Bool)
    ((as const (Array Bool Bool)) false))
)
```

In other words, if the sub-logic is QF_AX, it can only appear in the resulting model; if the sub-logic is ALL, it can appear in both the input formulas and result model. This makes the behavior unpredictable...

PS. `const` is not a function symbol in the theory signature (e.g. `ArraysEx`), so it is a solver-generated function symbol (I don't know what is `ALL` is though).

I admit that it may be a solver-specific question, but could the SMT-LIB standard give more strict restrictions for those solver-generated symbols?

Thanks.

Best regards,
Siyuan Chen