如何聲明常量以在Z3_mk_forall_const中用作約束變量？

假設我要普遍量化x和y滿足下述公式：如何聲明常量以在Z3_mk_forall_const中用作約束變量？

f(x,y) <=> x=y

使用Z3_mk_forall_const。我將不得不首先構造上面的公式，它需要Z3_ast類型的常量x和y。使用Z3_mk_const在全局聲明中創建x和y結果。我希望避免這種情況。有其他選擇嗎？

來源

2014-03-25 Gowtham Kaki

是的，有一種選擇;你可以使用Z3_mk_forall，它使用de-Brujin variable indexes。您可以使用 Z3_mk_bound創建索引變量，而不是常量，然後將它們的排序（排序）和名稱（decl_names）的數組傳遞給mk_forall或mk_exists。

來源

2014-03-26 11:46:37

謝謝，克里斯多弗。我瞭解_'Z3_mk_forall'_可用於創建具有de-Brujin索引作爲綁定變量的通用量化公式。但是，對於嵌套量詞來說，這種方法非常麻煩，因爲它需要「移動」索引。另一方面，具有唯一約束變量的量化公式可以平凡地組成。所以，我最好在不創建全局聲明的情況下使用_'Z3_mk_forall_const'_。 –

恐怕沒有直接的做法。然而，用於創建量詞的常量僅僅是爲了便於使用;內部任何東西無論如何都會被轉化爲de-Brujin指數。所以，一旦你創建了量詞，在其他地方重新使用常量應該是安全的。 –

如何聲明常量以在Z3_mk_forall_const中用作約束變量？

回答

相關問題