Z3可以调用外部定义的函数吗？答案

【问题标题】：Can Z3 call an externally defined function?Z3可以调用外部定义的函数吗？
【发布时间】：2016-07-08 18:03:28
【问题描述】：

我正在使用 Z3opt。我的大部分模型可以用标准 SMTLIB 表示，但其中一部分需要用通用编程语言实现，具有字符串处理、关联数组等结构。

是否可以在 Z3 模型中使用外部定义的函数？我知道这会影响求解器的性能，但它只是模型的一小部分。

-- 编辑澄清--

我希望提供约束的实现（作为函数指针或等效项）以支持 Z3 不支持的函数（例如三角函数）。在使用这样的黑盒约束时，我会接受 Z3 无法应用任何启发式的折衷。

【问题讨论】：

标签： z3

【解决方案1】：

您可以从 Z3 公开的二进制接口加载 SMTLIB 断言，然后使用来自 python、Java、.NET、C++、Ocaml 的 Z3 执行其他操作，然后调用检查可行性或优化目标的代码。 http://rise4fun.com/z3opt 上的 z3opt 教程包含指向 Phan 的 F# 代码的指针，该代码举例说明了使用二进制 API（在本例中来自 F#/.NET）。源代码中的示例目录包含使用各种 API 的示例。如果您需要未公开的更高级的东西，那么默认的回退基于 Z3 是开源的，因此您可以添加您想要的任何特殊功能。如果您觉得有一个普遍感兴趣的有用功能，那么在 https://github.com/z3prover/z3.git 上跟踪问题会很有用，如果您实现了它，您可以添加拉取请求。

【讨论】：

我认为您建议在调用 Z3 之前进行预处理步骤，但这还不够。我正在寻找的是一种编写自定义断言的方法，该断言在测试排列时由求解器调用。
我觉得你应该看看 Nikolaj 提到的 API。
我不是在询问有关使用 API 零碎构建 z3 SMTLIB 表达式的问题。我希望提供约束的实现（作为函数指针或等效项）以支持 Z3 不支持的函数（例如三角函数）。我认为实际的答案是做不到。
您可以通过为 Z3 编写自定义理论扩展（类似于插件）来实现您想要的。不过，由于缺乏这方面的个人经验，很遗憾我不能给你任何进一步的指示。
感谢 Malte - 这听起来很有希望，但我还没有找到任何与自定义理论相关的文档、示例或 API 调用。唯一提到的是其他堆栈溢出问题，表明它们可能已被弃用。