c++ - 如何在z3中定义分​​段函数

Question

我正在尝试使用以下 C++ 代码在 Z3 中定义一个非常简单的分段线性函数：

context c;
sort I = c.int_sort();
expr x = c.int_const("x");
func_decl f = function("f", I, I);
solver s(c);
s.add(forall(x, f(x) == ite(x <= 2, x, x + 1)));
s.add(f(x) == 2);
std::cout << s.check() << std::endl;

这会生成以下 SMTLib 格式的代码：

(declare-fun f (Int) Int)
(declare-fun x () Int)
(assert (forall ((x Int)) (! (= (f x) (ite (<= x 2) x (+ x 1))) :weight 0)))
(assert (= (f x) 2))
(check-sat)

显而易见的答案是 x=2。然而，在执行过程中，Z3 似乎进入了无限循环，完全停止响应。

为什么会发生这种情况，我应该如何在 Z3 中正确定义分段函数？

标签： c++z3

Answer 1

由于 SMT 问题通常是无法确定的（取决于问题涉及的理论），因此通常可以预期 Z3 不会因某些问题而终止（在合理的时间内）。量词和非线性整数算术是常见的原因。

默认情况下，Z3 分析它给出的问题并相应地配置（例如选择子求解器）。如果您想禁用它，例如因为您想自己配置 Z3。使用(set-option :auto_config false).

转向你的例子：

• 使用 Z3 4.8.7 x64，我立即获得sat了您提供的 SMT-LIB 片段。您使用的是哪个 Z3 版本？

• 如果我通过 禁用 MBQI（Z3 有不同的量词子求解器）(set-option :smt.mbqi true)，那么我会立即得到unknown. 这并不奇怪，因为 MBQI 非常适合寻找（非递归）函数的模型，比如你的f.

• 你为什么设置:weigh 0？它用于防止无限量词实例化链（匹配循环），因此显式设置权重 0 似乎有风险。尽管您的量词无论如何都不会产生匹配循环。