在z3 c ++接口中是否有一种形式的bitvector concat？ [英] Is there a form of bitvector concat in the z3 c++ interface?

问题描述

z3 python接口中的Concat（）函数允许连接任意位向量。我们的应用程序使用的是C ++接口。有一个简单的方法来获得与C ++接口相同的效果？我试图建立一个输出位向量表达式从子表达式。我可以使用shift和or操作，但我想要更简单，如果它存在。

The Concat() function in the z3 python interface allows you to concatenate arbitrary bit vectors. Our application is using the C++ interface, though. Is there an easy way to get the same effect with the C++ interface? I'm trying to build up an output bitvector expression out of sub-expressions. I can do it with shift and or operations, but I'd like something simpler if it exists.

例如，我想做的事情之一是创建一个4位位向量表示输入8位位向量表达式的奇数位。以下工作：

For example, one of the things I want to do is create a 4-bit bitvector representing the odd bits of an input 8-bit bitvector expression. The following works:

expr getOddBits8to4(context &c, expr &in) {
    expr result = ite(in.extract(1, 1) == c.bv_val(1, 1), c.bv_val(1, 4), c.bv_val(0, 4)) |
        ite(in.extract(3, 3) == c.bv_val(1, 1), c.bv_val(2, 4), c.bv_val(0, 4)) |
        ite(in.extract(5, 5) == c.bv_val(1, 1), c.bv_val(4, 4), c.bv_val(0, 4)) |
        ite(in.extract(7, 7) == c.bv_val(1, 1), c.bv_val(8, 4), c.bv_val(0, 4));
        return result;
}

但我宁愿能写如下：

expr result = Concat(in.extract(1,1), in.extract(3,3), in.extract(5,5), in.extract(7,7));

据我所知，这只能在Python接口中使用。有没有办法从C ++界面创建类似的东西，甚至只是简化上面的表达式？

As far as I can tell, this is only available in the Python interface. Is there a way to create something similar from the C++ interface, or even just to simplify the above expression?

推荐答案

提示Nikolaj Bjorner，我想出了以下包装函数似乎工作，直到可以提供正式版本。

Based on the hint by Nikolaj Bjorner, I've come up with the following wrapper function that seems to work until an official version can be supplied.

inline expr concat(expr const & a, expr const & b) {
    check_context(a, b);
    assert(a.is_bv() && b.is_bv());
    Z3_ast r = Z3_mk_concat(a.ctx(), a, b);
    a.check_error();
    return expr(a.ctx(), r);
}

$ b b
$ b

Using this, my odd bit example can be written:

expr result = concat(in.extract(1, 1), concat(in.extract(3, 3), concat(in.extract(5, 5), in.extract(7, 7))));

这篇关于在z3 c ++接口中是否有一种形式的bitvector concat？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！