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

Question

我想知道是否有可能让 z3 在输出表达式中不使用 Extract 和 Concat 时将 simplify 应用于带有位向量的表达式。

例如，而不是

>>> 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，但找不到这样的 "option"。

Answer 1

不容易。 z3 在重写器中相当早地将带有数字的 XOR 转换为掩码，并且似乎没有简单的方法来控制该行为。看这里：https://github.com/Z3Prover/z3/blob/master/src/ast/rewriter/bv_rewriter.cpp#L1817-L1823

话虽如此，可编程 API 的优势在于 z3 为您提供了自行编写此类转换代码的所有工具。这确实 not 意味着这样做很容易，但至少它公开了所有必要的点点滴滴。虽然完全按照您想要的方式进行重写可能是一项艰巨的任务，但您可以通过以下简单的方式逃脱：

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

这非常simple-minded；它实际上什至不能处理你提出的问题：

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

但它确实处理了这个问题：

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

不过8行代码，还不错！关键是您可以在沿着表达式的结构走下去时对其进行改进，识别 associativity/commutativity 等，并在可编程的 API.[=16 公开的 AST 上执行任何您想要的转换=]

请记住，如果您在求解器上下文中使用它，则必须维护一堆不变量，如果您进行 "incorrect" 转换，则很容易使求解器失效。拥有权利的同时也被赋予了重大的责任！尽管如此，如果您愿意研究 API 并深入研究，可以通过相对简单的编程实现很多。

祝你好运！

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

Simplify z3 bitvector expression, but avoid extract & concat

python

z3

xor

smt

bitvector