z3：将袋作为数组

编程问答 2022-08-15

问题描述

下面的摘录来自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))

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

    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]索引处的值作为数组的常数。谁能解释发生了什么事？预先感谢。

解决方法

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

假设您有两个符号整数。您可以像这样添加它们：

(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))来明确给出类型注释。这是相当令人困惑的语法，但是这就是您说我希望“ map”在这种情况下在“ +”上工作的方式。您几乎可以忽略它。

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

arraysarraysarraysfirst-order-logicz3