z3 - 如何在 Z3 中获得“更强”的连词简化？

Question

使用 Z3 2.18 版，我试图简化公式，例如：

• (和 (> (- (- x 1) 1) 0) (> x 0))
• (或 (> (- (- x 1) 1) 0) (> x 0))

希望得到类似的东西：（> x 2）和（> x 0）。

我正在使用以下输入文件运行 Z3，其中 F 是上述公式之一：

(set-option set-param "STRONG_CONTEXT_SIMPLIFIER" "true")
(declare-const x Int)
(simplify F)

它适用于我得到以下输出的析取：

(let (($x35 (<= x 0)))
(not $x35))

但是，通过结合，我得到：

(not (or (<= x 0) (<= x 2)))

有没有办法强制 Z3 进一步简化上述公式？我希望能够得到(not (<= x 2))。

PS：有没有办法强制 Z3 内联其输出（即有(not (<= x 0))而不是(let (($x35 (<= x 0))) (not $x35))）

谢谢，格斯

Answer 1

不，你不能在 Z3 2.x 上这样做。

Z3 3.x 有一个新的（完全兼容的）SMT 2.0 前端。Z3 3.x 有几个新特性，例如基于战术和战术的“策略规范语言”。我还没有“做广告”，因为它正在进行中。此幻灯片中描述了基本思想。这种语言可以用来做你想做的事。你只需要写：

(declare-const x Int)
(assert (not (or (<= x 0) (<= x 2))))
(apply (and-then simplify propagate-bounds))

您可以使用以下命令找到所有可用的策略：

(help-strategy)
(help apply)
(help check-sat-using)