Z3 中的简化 [英] simplification in Z3

问题描述

(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中简化此类表达式(此类表达式的组合)?谢谢！

Is it possible to simplify such expressions (the combinations of such expressions) in Z3? Thank you!

推荐答案

simplify 命令只是一个自底向上的重写器.它很快，但无法简化您帖子中的表达方式.Z3 允许用户使用策略定义自己的简化策略.本文 和 Z3教程(Python 和 SMT 2.0).以下帖子还包含其他信息:

The simplify command is just a bottom-up rewriter. It is fast, but will fail to simplify expressions such as the ones in your post. Z3 allows users to define their own simplification strategies using tactics. They are described in this article, and the Z3 tutorials (Python and SMT 2.0). The following posts also have additional information:

• t>=1 或 t>=2 =>t>=1
• ctx-solver-simplify 中的非对称行为
• 简化"有什么区别;和ctx-solver-simplify"在 z3

您示例中的第一个查询可以使用策略 ctx-solver-simplify(也可在线获得此处).

The first query in your example can be simplified using the tactic ctx-solver-simplify (also available online here).

(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 应用于断言集，并显示生成的目标集.请注意，此策略比命令 simplify 的成本要高得多.

The command apply applies the tactic ctx-solver-simplify over the set of assertions, and displays the resulting set of goals. Note that, this tactic is way more expensive than the command simplify.

这篇关于Z3 中的简化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！