我在 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 < 15)?
最佳答案
您可以通过在一组模板中合成更简单的表达式来在 Z3 之上构建一个简化器。但是 Z3 并没有尝试在许多其他方面执行这种特定的简化。
关于z3 - 简化 Z3 表达式,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/30736834/