z3 - Z3 的simple() 方法是否支持吸收定律？

Question

假设我有一个 BoolExpr 的形式

a & (a | b) or a | (a & b) 

我想把它简化为

a 

通过调用simple()。它不起作用。

此外，对于像这样的约束

(a | b) & (b | a) 

简化()不能把它变成最简单的形式

(a|b) or (b|a).

有解决方法吗？

@Nikolaj Bjorner:感谢您的帮助，我还有一个问题:

这是我的原始约束:

Goal: (goal
  (or (> (type o) 2) (= (type o) 1))
  (or (= (type o) 1) (> (type o) 2)))

这是简化版本(通过 ctx-solver-simplify):

(or (= (type o) 1) (not (<= (type o) 2)))

我期望的实际约束是:

(or (= (type o) 1) (> (type o) 2))

我不想介绍任何否定。我该怎么办？

Answer 1

默认的简化器只寻找廉价的重写。
您可以调用一个不同的简化器作为策略。
它简化了您描述的目标。
例如:

(declare-const a Bool)
(declare-const b Bool)
(assert (or a (and a b)))
(apply ctx-solver-simplify)

它可能会返回几个需要重新组合成公式的子目标。
rise4fun.com 上的 Z3 教程描述了策略。

ctx-solver-simplify 进行有限的上下文相关重写。它仍然不完整。
它不产生规范的范式(两个等价的公式可以简化为
两个不同的公式)。