z3中给数组赋值的三种方式

Question

据我所知，在 z3 中有三种方法可以将值分配给数组。

使用 assert 将值分配给某些单元格：

(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))

(assert (= 1 (select a1 0)))
(assert (= 2 (select a2 0)))

z3 returns unsat 当添加约束 (assert (= a1 a2)) 时。

首先使用as const初始化数组，然后将值分配给特定的单元格：

(declare-const a3 (Array Int Int))
(assert
    (=
        (store ((as const (Array Int Int)) 64) 0 3)
        a3
    )
)
(declare-const a4 (Array Int Int))
(assert
    (=
        (store ((as const (Array Int Int)) 64) 0 4)
        a4
    )
)

加上(assert (= a3 a4))又得到unsat

通过函数定义数组：

(define-const a5 (Array Int Int)
    (lambda ((i Int))
    (ite (= i 0) 5 64)))
(define-const a6 (Array Int Int)
    (lambda ((i Int))
    (ite (= i 0) 6 64)))

但是如果我们加上(assert (= a5 a6))，z3returnssat。为什么？

顺便问一下，有没有（更好的）方法可以为 z3 中的数组赋值？

Answer 1

这是一个错误。看看这个 issue.

z3中给数组赋值的三种方式

Three ways to assgin values to an array in z3

smt

z3