在z3 C++接口中是否存在一種bitvector concat形式？

Question

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++接口創建類似的東西，甚至只是爲了簡化上述表達式？

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