Z3：如何最好地编码“switch 语句”？

Question

我想创建一个表达式来选择一组给定表达式中的一个。给定一个表达式数组

Expr[] availableExprs = ...;

在静态已知长度的情况下，我希望 Z3 选择其中任何一个（如 switch 语句）。如果问题是 SAT，我需要一种方法来找出模型中选择了哪些（它在数组中的索引）。

最快的编码方式是什么？

到目前为止，我考虑过这些方法：

1. 将 整数 限制为 [0, arrayLength) 并使用 ITE 选择其中一个表达式。该模型允许我提取这个整数。不幸的是，这将整数理论引入了模型（以前根本不使用整数）。
2. 每个可能的选择都有一个布尔值。使用 ITE 选择表达式。断言其中一个布尔值是真的。这种策略不需要任何特殊的理论（我认为），但编码可能过于冗长。
3. 将表达式存储到 数组 表达式中，并使用整数从该数组中读取。这节省了 ITE 链，但引入了数组理论。

显然，所有这些都有效，但它们似乎都有缺点。最好的策略是什么？

Answer 1

如果您只想编码元素 v 在有限集合 {e1, ..., en} 中（使用排序 U），则可以使用 smtlib2 执行此操作，如下所示：

(declare-fun v () U)
(declare-fun p1 () Bool)
...
(assert (= p1 (= v e1)))
(assert (= p2 (= v e2)))
...
(assert (= pn (= v en)))

(assert (or p1 ... pn))

变量 v 将等于 {e1 ... en} 的“数组”中的元素之一。如果选择变量 v 等于 ei，则 pi 必须为真。这基本上是对 Nikolaj 建议的重述，但可以随意改写。

请注意，可以将多个 pi 设置为 true，因为不能保证 ei != ej。如果你需要确保没有两个元素都被选中，你需要弄清楚你想要什么语义。如果 {e1... en} 已经被要求是不同的，你不需要添加任何东西。如果“数组”元素必须是不同的，但还没有必要是不同的，你可以断言

(assert (distinct e1 ... en))

（这可能会在内部扩展为 n 中的二次方。） 相反，您可以说没有 2 p 个变量可以同时为真。请注意，这是一个较弱的陈述。要看到这一点，假设 v = e1 = 1 和 e2 = e3 = 0。那么 p1 = true 和 p2 = p3 = false。这些约束的明显编码是二次的：

(assert (or (not pi) (not pj))) ; for all i < j

如果您需要更好的编码，请尝试在Translating Pseudo-Boolean Constraints into SAT 5.3 节中查看如何对“p1+ ... + pn

Answer 2

我认为您想确保每个表达式都没有量词，并且只使用公式中已经存在的函数和谓词。如果不是这种情况，则为每个索引引入一个新的命题变量 p_i 并向求解器断言 ctx.MkIff(p_i, availableExprs[i])。 Z3 生成模型时，使用 model.Eval(p_i) 并检查结果是否为表达式“True”。