是否可以訪問與Z3中的de Bruijn索引關聯的名稱？

因此，我可以使用Z3_get_quantifier_bound_name在表示量詞的表達式上調用，獲得與量詞邊界相關的名稱。但假設我正在穿越量化子公式的AST。在這一點上可以訪問索引的名稱嗎？謝謝。是否可以訪問與Z3中的de Bruijn索引關聯的名稱？

if (z3_expr.is_var()) 
{ 
    // is it possible at this point to get the name of the quantified variable, 
    // which was associated with it at quantifier creation? 
}

來源

2012-11-13 Egbert

作爲變量的表達式沒有直接與它們關聯的名稱。我們訪問這些名稱的方式是保留一堆名爲的量詞，這些量詞在下路時被遍歷。因此，維護一個符號向量（堆棧/列表），並且每當您遍歷一個量詞時，都會將量詞的綁定名稱推送到該向量上。完成遍歷量詞後，您將不得不彈出名稱。

可以使用下列API來訪問綁定變量的名稱：

unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a); 

Z3_symbol Z3_API Z3_get_quantifier_bound_name(__in Z3_context c, __in Z3_ast a, unsigned i);

需要注意的是量化的變量的指標進行排序從右到左。所以如果Z3_get_quantifier_num_bound（上下文中，表達式）返回圖2，和 X = Z3_get_quantifier_bound_name（上下文，EXPR，0） Y = Z3_get_quantifier_bound_name（上下文，EXPR，1）然後Y具有索引0和x具有索引1

來源

2012-11-13 08:44:23

謝謝，我明白了，我期待這一點。當我們嵌套量詞時會發生什麼？索引的計數是否繼續？我假設，我應該使用Z3_get_index_value來獲取給定變量表達式的索引號。 – Egbert

是X2，枚舉繼續，'Z3_get_index_value'檢索變量的de Bruijn索引。查看更多代碼示例的答案：http://stackoverflow.com/questions/11816626/understanding-the-indexing-of-bound-variables-in-z3 –

是否可以訪問與Z3中的de Bruijn索引關聯的名稱？

回答

相關問題