z3 c++ 接口中是否有一种位向量 concat 形式？答案

【问题标题】：Is there a form of bitvector concat in the z3 c++ interface?z3 c++ 接口中是否有一种位向量 concat 形式？
【发布时间】：2015-05-09 02:11:27
【问题描述】：

z3 python 接口中的 Concat() 函数允许您连接任意位向量。不过，我们的应用程序使用的是 C++ 接口。有没有一种简单的方法可以使用 C++ 接口获得相同的效果？我正在尝试从子表达式中构建输出位向量表达式。我可以通过 shift 和 or 操作来做到这一点，但如果它存在的话，我想要更简单的东西。

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

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++ 接口创建类似的东西，甚至只是简化上面的表达式？

【问题讨论】：

标签： c++ z3

【解决方案1】：

根据 Nikolaj Bjorner 的提示，我提出了以下包装函数，在提供正式版本之前似乎可以使用。

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);
}

使用这个，我的奇数示例可以写成：

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

【讨论】：