racket - 在某些 Z3 绑定中是否有不支持声明排序的解决方法？

Question

我对Z3不太熟悉，但必须用它来做一些项目。

我使用的是Z3球拍绑定，它有像SMT-LIB v2一样的文本界面，可以消除通用量词，但它还不支持declare-sort，而我的模型需要某种自定义类型定义（我想不出如何只Int在我的模型中使用..)

在这种情况下，如果我想使用绑定，我该如何解决declare-sort 在我的模型中获取的功能？Z3有类似的东西吗？

或者在 Z3 不支持的某些类型上工作的常用技巧是什么？

Answer 1

我相信你最好的办法是直接给 Siddharth Agarwal 发邮件。