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

Question

我想知道当对表达式应用 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/ast/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 行代码来说，还不错!重点是，当您深入了解表达式的结构、识别关联性/交换性等，并对可编程 API 公开的 AST 进行任何您想要的转换时，您可以对其进行改进。

请记住，如果您在求解器上下文中使用它，则必须维护一堆不变量，如果您执行“不正确”的转换，则可以轻松地使求解器变得不健全。拥有权利的同时也被赋予了重大的责任!尽管如此，如果您愿意研究 API 并进行深入研究，则可以通过相对简单的编程实现很多目标。

祝你好运!