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

【问题标题】：How to get "stronger" simplifications of conjunctions in Z3?如何在 Z3 中获得“更强”的连词简化？
【发布时间】：2011-09-26 13:39:44
【问题描述】：

使用 Z3 版本 2.18，我正在尝试简化公式，例如：

希望得到类似：(> 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))）

谢谢，格斯

【问题讨论】：

标签： z3

【解决方案1】：

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

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

(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)

【讨论】：