z3:作为阵列的袋子

Question

以下片段来自z3的教程：https://rise4fun.com/z3/tutorialcontent/guide

(define-sort A () (Array Int Int Int))
(define-fun bag-union ((x A) (y A)) A
((_ map (+ (Int Int) Int)) x y))
(declare-const s1 A)
(declare-const s2 A)
(declare-const s3 A)
(assert (= s3 (bag-union s1 s2)))
(assert (= (select s1 0 0) 5))
(assert (= (select s2 0 0) 3))
(assert (= (select s2 1 2) 4))
(check-sat)
(get-model)

我无法理解这条线路是如何工作的——((_ map (+ (Int Int) Int)) x y))

此外，我不明白，为什么在下面给定的输出中，数组s2被从索引[1，2]指定为常数值4，而不是从索引[0，0]指定为常值：

sat
(model 
(define-fun s2 () (Array Int Int Int)
(store ((as const (Array Int Int Int)) 4) 0 0 3))
(define-fun s1 () (Array Int Int Int)
((as const (Array Int Int Int)) 5))
(define-fun s3 () (Array Int Int Int)
(store ((as const (Array Int Int Int)) 9) 0 0 8))
)

我甚至尝试向s2的其他索引添加更多的值，但z3只选择[1，2]索引处的值作为数组的常数值。有人能解释一下发生了什么吗？提前谢谢。

Answer 1

在z3中，map是一个将逐点运算符扩展到数组的函数。

假设你有两个符号int。你可以这样添加它们：

(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 4))

如果有两个数组，会发生什么？SMTLib没有指定"；添加"；两个数组，也就是说，没有办法说给我一个新的数组，它是两个数组的逐点求和。这就是z3的map扩展的用武之地

(declare-const arr1 (Array Int Int))
(declare-const arr2 (Array Int Int))
(declare-const arr3 (Array Int Int))
(assert (= arr3 ((_ map (+ (Int Int) Int)) arr1 arr2)))

再次注意，这是一个z3扩展，不适用于其他SMT解算器。上面发生的事情是，z3将按元素添加arr1和arr2，并且由于arr3，将要求其等效于arr3。

(此外：在教程的例子中，它们是对袋子进行建模；也就是说，它们在地图中存储了两个整数；所以它有点复杂。但除此之外，想法是一样的。(

类型消歧需要+上的滑稽归属。您可以将其视为：(map + arr1 arr2)。不幸的是，SMTLib的类型系统不够强大，无法确定您想要哪个+，因为它是一个重载运算符。因此，您必须通过编写(_ map (+ (Int Int) Int))来显式地给出一个类型注释。这是一个相当令人困惑的语法，但这就是你所说的"我想要"；地图"；正在处理"+"在这种情况下。你基本上可以忽略它。

我不明白你问题的第二部分。求解器可以自由选择任何令人满意的模型。此外，请记住SMTLib数组不具有边界。即任何Int都是有效索引。(这与许多编程语言中的数组形成了鲜明对比。(如果您有进一步的问题，请随时启动另一个线程。(当每个线程只问一个问题时，堆栈溢出效果最好。(