在 Z3 集的域上应用函数

Question

Z3有没有办法对集合中的每一个元素应用一个函数，从而得到一个新的集合？在通常的编程语言中，这样的函数如下所示： map :: (a -> b) -> Set a -> Set b

我知道 map 函数，但它将任意函数应用于数组范围。 map 我正在寻找与数组域一起工作的作品（考虑到 Z3 集的构建方式）。

Answer 1

这在 SMTLib 中是不可能的。注意你要的map函数是高阶函数，SMTLib不支持高阶逻辑。有一些提议的扩展来包含此类功能，但至少 z3 还不支持此类功能。一些参考资料：

话虽如此，您有时可以通过使用量化公理模拟高阶特征来逃脱。当然，引入量词会使逻辑成为半可判定的，因此证明者可以 return unknown （对于任何有趣的用例，它很可能会这样做），但这是处理此类问题的一种方法。这是一个例子：

; declare two Int sets
(declare-fun S1 () (Array Int Bool))
(declare-fun S2 () (Array Int Bool))

; Function to increment "domain" by 1
(define-fun f ((a Int)) Int (+ a 1))

; Relate S2 to S1 by "mapping" on the domain
; In a higher-order language, this would be:
;      S2 = map f S1
(assert (forall ((x Int)) (= (select S2 x)
                             (select S1 (f x))
                          )))

; some tests:
(assert (= (select S2 4) (select S1 3)))

(check-sat)
(get-model)

请注意我是如何使用 forall 断言来表达 S1 和 S2 之间的关系的。这在一般情况下可能是不可能的；在一般情况下，您可能还必须指定 f 的倒数，但它可以解决基本用途。请注意，您将无法 "pass" 一个函数到其中任何一个：就像上面示例中的 f 一样，所有在 "higher-order" 位置使用的函数都必须明确命名.比较有限，但在简单的情况下可以完成工作。

此外，虽然 Z3 快速解决了这个特定的基准，但我不希望它处理任意量化的案例。对于高阶函数的推理，Z3（或任何其他 SMT 求解器）不是合适的工具。如果那是你的目标，请研究 Isabelle、HOL、Coq、Agda、Lean 等定理证明器；它们是从头开始设计的，用于处理高阶特征。他们还拥有强大的联系（即预言机和证明重播机制），因此他们可以在完成证明时使用 SMT 求解器作为后台引擎。当然，缺点是它们不是按钮，因此需要手动引导。（虽然近年来自动化变得非常好。）

在 Z3 集的域上应用函数

Applying a function on the domain of a Z3 set

set

z3