Z3 (z3py) "simplify()" 函数的 "elim_and" 选项总是为位向量启用

Question

我想使用 z3py 的 simple() 函数，但不将按位和 '&' 更改为按位或 '|'。

简化函数似乎存在一个名为“elim_and”的选项，但我无法让它用于按位运算。函数 help_simplify() 状态：

elim_and (bool) 连词使用否定和析取进行重写（默认值：false）

>>> from z3 import *
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> z = x & y
>>> z
x & y
>>> simplify(z)
~(~x | ~y)
>>> simplify(z, elim_and=False)
~(~x | ~y)

我希望结果是“x & y”。 有什么办法吗？

Answer 1

目前这是不可能的。请注意，elim_and 针对的是布尔值，而不是位向量：

>>> from z3 import *
>>> a = Bool("a")
>>> b = Bool("b")
>>> simplify(And(a, b))
And(a, b)
>>> simplify(And(a, b), elim_and=True)
Not(Or(Not(a), Not(b)))

没有与simplify 等效的选项来控制位向量。实际上，甚至在您调用简化器之前就已经发生了析取的转换，请参见此处：https://github.com/Z3Prover/z3/blob/master/src/ast/rewriter/bv_rewriter.cpp#L1980-L1988

Answer 2

elim_and 用于布尔表达式，而不用于位向量。恐怕Z3没有禁用特定重写规则的选项。