简化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中的非对称行为简化
• z3中"简化"和"ctx-solver-simplified"之间的区别是什么

您的示例中的第一个查询可以使用策略进行简化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断言集,并显示生成的目标集.请注意,这种策略比命令更昂贵simplify.