简化 Z3 表达式答案

【问题标题】：Simplifying Z3 expressions简化 Z3 表达式
【发布时间】：2015-06-09 15:45:14
【问题描述】：

我在 Python 中使用 z3 来简化一些逻辑表达式，但我有疑问。当我执行以下代码时

x = BitVec('x', 8)
e = ULT(x - 5, 10)
Then('simplify', 'propagate-values', 'ctx-solver-simplify')(e).as_expr()

我得到了结果：

Not(ULE(10, 251 + x))

但是，这等价于

And(UGE(x, 5), ULT(x, 15))

有没有办法将第一个表达式（Not）转换（简化）为第二个表达式（And）？更具体地说，是否可以向 z3 询问特定变量的取值范围（在本例中为 x >= 5 && x

【问题讨论】：

标签： z3 z3py

【解决方案1】：

您可以在 Z3 之上通过在一组模板中合成更简单的表达式来构建一个简化器。但 Z3 并没有尝试在许多其他方面进行这种特殊的简化。

【讨论】：