如何在 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 中正确定义分段函数？

Answer 1

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

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

转向你的例子：

使用 Z3 4.8.7 x64，我立即得到 sat 您提供的 SMT-LIB 片段。您使用的是哪个 Z3 版本？
如果我通过 (set-option :smt.mbqi true) 禁用 MBQI（Z3 有不同的 subsolvers for quantifiers），那么我会立即得到 unknown。这并不奇怪，因为 MBQI 非常适合为（非递归）函数查找模型，例如 f.
为什么设置:weigh 0？它用于防止无限量词实例化链 (matching loops)，因此明确设置权重为 0 似乎有风险。尽管您的量词无论如何都不会产生匹配循环。

Answer 2

Malte 描述了处理量词时经常出现的一些问题。使用量词来定义这样的函数几乎总是一个坏主意：它不必要地调用很容易导致求解器进入永无止境的电子匹配循环的过程。定义此类函数的经典（和“官方”）方法是简单地使用 define-fun 结构：

(declare-fun x () Int)
(define-fun f ((x Int)) Int (ite (<= x 2) x (+ x 1)))
(assert (= (f x) 2))
(check-sat)

有了这个输入，我得到：

sat

马上。

关于 SMT 求解中的量词有很多要说的，这里有一组很好的幻灯片供您浏览：http://homepage.divms.uiowa.edu/~ajreynol/pres-dagstuhl15.pdf

但是，长话短说，除非绝对需要，否则请避免使用量词。对于您遇到的常规一阶问题，您不需要量词。

（请注意，当您使用 C++ 或任何其他更高级别 API 进行编程时，您通常不会定义这些类型的函数。相反，您只需在宿主语言中定义一个函数，并且用“符号”变量调用它，它为每个实例化生成右侧。从某种意义上说，您在每个调用站点“内联”定义。这避免了不必要的复杂性并且通常足以解决大多数建模问题。）

如何在 z3 中定义分段函数

How to define a piecewise function in z3

c++

z3