如何使用z3pythonapi对bvredand进行编码？

Question

假设我希望使用Z3 python API对以下表达式进行编码：

(bv-redand
    (bv-or
        (bv-xnor symbolic_bit_0 
            (bv-concat src_ip dst_ip src_port dst_port))
        symbolic_dc_0)))))

我该怎么做？你知道吗

看来我必须这样做：

And(~(symbolic_bit_0 ^ Concat(src_ip dst_ip src_port dst_port)) | symbolic_dc_0)

但最外层的似乎不起作用。我能想到的一个方法是避免使用And，而是与所有的1进行比较，但是有没有更好的方法呢？你知道吗

作为旁注，有没有办法直接指定一个Xnor b而不是~（a^b）？你知道吗

Answer 1

Reduction和Reduction或还没有添加到pythonapi中。请注意，减少和是非常不同的'正常和'。我现在已经把它们添加到不稳定的分支中。为了便于参考和将来使用，我们可以从外部添加存在于C-API中但不存在于pythonapi中的函数。例如，在这种情况下，我们可以定义

def BVRedAnd(a):
    return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)

其他的布尔运算符有Python的等价物，但是XNor没有，所以没有添加相应的函数。但是，如果我们想：

def BVXNor(a, b):
    return BitVecRef(Z3_mk_bvxnor(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)

但是，性能上的差异可以忽略不计。你知道吗