有沒有在某些Z3綁定中支持declare-sort的解決方法？

Question

我對Z3不太熟悉，但必須用它來做一些項目。

我使用Z3 racket binding，它具有像SMT-LIB v2這樣的文本接口，能夠消除通用量詞，但它尚不支持declare-sort，而我的模型需要某種自定義類型定義（我不能怎麼會想到只用在我的模型Int尚未..）

在這種情況下，如果我想使用綁定，我如何可以解決得到的declare-sort 在我的模型的功能？ Z3中有類似的東西嗎？

什麼是在Z3中不支持的某些類型的常用提示？

Answer 1

我相信你得到答案的最佳方法就是直接郵寄Siddharth Agarwal。