简化 z3 位向量表达式，但避免提取和连接

Question

我想知道，当一个与BitVectors在表达式上应用simplify时，是否有可能在输出表达式中使用Z3不使用Extract和Concat。

例如，而不是

>>> x = BitVector("x", 32)
>>> simplify(x ^ 7 ^ 6)
Concat(Extract(31, 1, x), ~Extract(0, 0, x))

我想拥有

>>> x = BitVector("x", 32)
>>> simplify(x ^ 7 ^ 6)
x ^ 1

我看了help_simplify，但是找不到这样的"选项"。

Answer 1

不容易。z3在重写者的早期将带有数字的XOR转换为掩码，并且似乎没有简单的方法来控制该行为。请参阅此处：https：//github.com/z3prover/z3/blob/master/src/src/rewriter/bv_rewriter.cpp#l1817-l1823

话虽如此，可编程API的优点是Z3为您提供了自己编码此类转换的所有工具。这确实不是意味着这样做很容易，但是至少它会暴露出所有必要的碎屑。在做完整的工作时，您想要的重写可能是一项艰巨的任务，您可以逃脱这样的简单的东西：

def constFold(e):
    try:
       if is_app(e) and all([is_bv_value(c) for c in e.children()]):
          return simplify(e)
       else:
          return e
    except:
        return e

这是非常简单的；实际上，它甚至无法处理您提出的问题：

>>> constFold(x^6^7)
x ^ 6 ^ 7

但确实处理了这一点：

>>> constFold(x^(6^7))
x ^ 1

但是，对于8行代码，还不错！关键是，当您走下表达式的结构，识别关联/通勤等级时，您可以改善它，并执行您想要在AST上进行的任何转换，以使可编程API暴露。

请记住，如果您在求解器上下文中使用它，则必须维护一堆不变性，如果进行"不正确"的转换，则可以轻松使求解器不符合。拥有权利的同时也被赋予了重大的责任！但是，如果您愿意学习API并深入研究，可以通过相对简单的编程实现很多。

。

祝你好运！