Z3檢查兩個表達式是否相同

Question

在我的代碼中添加約束時，我發現我必須將相同的約束添加到表達式向量中多次。是否有任何API來檢測兩個表達式是否完全相同，以便我可以刪除多餘的表達式？

Answer 1

表達式總是內化爲唯一的指針。因此，如果使用相同的子表達式構建兩個表達式，則指向它們的指針將相同。你可以簡單地使用指針相等。

表達式也有所謂的「標識符」。獲取標識符的C調用稱爲Z3_ast_get_id，其他編程語言中有相應的調用 （來自C++，您仍然需要使用來自C＃和Java的Z3_ast_get_id，它被稱爲「Id」/「id」）。