Z3的simplify()方法是否支持吸收定律？

Question

假设我有一个BoolExpr的形式

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

我想简化它

a 

通过调用simplify().它不起作用.

另外,对于像这样的约束

(a | b) & (b | a) 

simplify()无法将其转换为最简单的形式

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

(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-simplified确实限制了依赖于上下文的重写.它仍然不完整.它不产生规范的正规形式(两个等价的公式可以简化为两个不同的公式).