z3 - Z3 中的简化

Question

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(simplify (or (= s ON) (= s OFF) (= s BROKEN)))
(simplify (and (> a 0) (> a 1)))

结果是：

(or (= s ON) (= s OFF) (= s BROKEN))
(and (not (<= a 0)) (not (<= a 1)))

但预期的结果是：

1
> a 1

是否可以在 Z3 中简化此类表达式（此类表达式的组合）？谢谢！

Answer 1

该simplify命令只是一个自下而上的重写器。它很快，但无法简化表达式，例如您帖子中的表达式。Z3 允许用户使用策略定义自己的简化策略。它们在本文和 Z3 教程（Python和SMT 2.0）中进行了描述。以下帖子还有其他信息：

• t>=1 或 t>=2 => t>=1
• ctx-solver-simplify 中的不对称行为
• z3中的“简化”和“ctx-solver-simplify”有什么区别

您的示例中的第一个查询可以使用该策略进行简化ctx-solver-simplify（也可以在此处在线获得）。

(declare-datatypes () ((SE BROKEN ON OFF)))
(declare-const s SE)
(declare-const a Int)
(assert (or (= s ON) (= s OFF) (= s BROKEN)))
(assert (and (> a 0) (> a 1)))
(apply ctx-solver-simplify)

该命令apply将策略应用于ctx-solver-simplify断言集，并显示结果集。请注意，这种策略比 command 更昂贵simplify。