24 views

Skip to first unread message

Oct 9, 2021, 7:59:26 PM10/9/21

to SMT-LIB

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

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?

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu