z3 - 从模型中获取具体的数组值

Question

我正在使用 Z3 检查数组属性片段中公式的可满足性。Z3 返回的数组变量模型通常使用其他 if 表达式、if-then-else 案例分析等来表示。我想以某种方式解析 Z3 输出的模型并创建满足输入 SMT-LIB 公式的数组，明确的。

例如，我希望能够以某种方式始终将 Z3 输出的模型简化为以下形式：

A -> {
  1 -> 3
  2 -> 4
  else -> 6
}

是否有一些简单的方法来遍历模型（使用 C API？）并创建一个表示模型的显式数组？

Answer 1

不幸的是，您的消息中描述的输出格式不足以描述数组属性片段中每个可满足公式的模型。例如，考虑以下简单示例。

(declare-fun f (Int) Int)
(declare-const a Int)
(declare-const b Int)

(assert (forall ((i Int) (j Int)) (=> (<= i j) (<= (f i) (f j)))))
(assert (< (f a) (f b)))

(check-sat)
(get-model)

该公式f是非递减的，它有两个点a和bst f(a) < f(b)。在任何模型中，我们必须对所有值i <= a,f(i) <= f(a)和所有值j >= b,都具有该值f(b) <= f(j)。那是，

f(i) <= f(a) < f(b) <= f(j).

单行else不行。Z3 产生了一种解释，f它本质上是一个“阶梯函数”。您可以在此处尝试上面的示例。