据我所知,有三种方法可以在z3中为数组赋值。
assert
为某些单元格赋值:(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(assert (= 1 (select a1 0)))
(assert (= 2 (select a2 0)))
当添加约束unsat
时,z3返回(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))
,z3将返回sat
。为什么?
顺便说一下,有没有(更好的)方法为z3中的数组赋值?
这是一个错误。看看这个issue。