【发布时间】：2016-03-08 20:43:55
【问题描述】：
我正在尝试使用 Z3 的 OCaml API 来表达以下函数声明：
(declare-fun ctrl_p ((Int)) String)
但是，我在 documentation 中找不到合适的 mk_sort 函数。有什么建议的解决方法吗？
谢谢。
【问题讨论】：
【发布时间】：2016-03-08 20:43:55
【问题描述】：
您是否已经需要此功能？字符串功能是全新的，仅可用于其他 API。对于 OCaml，我们也在处理修复 GC 交互。当然欢迎您提供拉取请求。
【讨论】：
-
确实，OCaml API 目前正在恢复中，但是一旦完成，添加字符串就很容易了，所以暂时先忍耐一下。
-
感谢您的快速回答。出于好奇：除了
src/api/ml/z3.ml和src/api/ml/z3.mli，我应该在哪些文件中添加对字符串的支持？我看到scripts/update_api.py用于生成 C 存根，但我并不完全清楚它是如何工作的。