使用Z3 :: expr作爲映射值

我在使用Z3 :: expr作爲映射值類型時遇到了困難。編譯器抱怨沒有默認的構造函數可以使用。玩具示例如下所示。使用Z3 :: expr作爲映射值

#include <z3++.h> 
#include <map> 
//#include <vector> 

using namespace std; 
using namespace z3; 

int main() { 
    map <int, expr> m; 
    context c; 
    m[1] = c.bool_const("x"); 
    return 0; 
}

的編譯器（鏘++）抱怨

no matching constructor for initialization of 'mapped_type' (aka 'z3::expr') 
     __i = insert(__i, value_type(__k, mapped_type())); 

in instantiation of member function 'std::map<int, z3::expr, std::less<int>, 
std::allocator<std::pair<const int, z3::expr> > >::operator[]' requested here 
m[1] = c.bool_const("x"); 

/usr/include/z3++.h:562:9: note: candidate constructor not viable: requires single argument 'c', but no arguments were provided 
    expr(context & c):ast(c) {} 
    ^
/usr/include/z3++.h:564:9: note: candidate constructor not viable: requires single argument 'n', but no arguments were provided 
    expr(expr const & n):ast(n) {} 
    ^
/usr/include/z3++.h:563:9: note: candidate constructor not viable: requires 2 arguments, but 0 were provided 
    expr(context & c, Z3_ast n):ast(c, reinterpret_cast<Z3_ast>(n)) {}

使用矢量來包裝EXPR或在地圖中找到的方法的替代品似乎是細。有沒有辦法直接使用expr作爲map值類型+ []運算符？

來源

2016-11-17 Min Gao

這是一個有關地圖的常見問題：[]需要一個空的構造函數用於實例類型，請參閱this和this。

（Ugly）Tweak。 您可能想要派生子類map，將本地引用添加到z3 context，並通過構造函數map_subclass或方法提供此參數。然後，您應該覆蓋[]，以便它使用此引用創建一個新的expr實例與構造函數expr(context &c)，而不是嘗試使用expr()。

我的Z3的內部知識是有限的，但作爲據我所知這應該不破壞任何東西。

來源

2016-11-18 13:54:56

表達式被內化爲唯一的指針。您可以從無符號或指針創建一個映射作爲鍵。 Z3_get_ast_id將AST的標識符作爲無符號進行檢索，並且expr類中的運算符將檢索也是唯一的AST指針。 YOu也希望使用一些輔助方法（例如expr_vector）將表達式固定在地圖上。 –

使用Z3 :: expr作爲映射值

回答

相關問題