Z3 可以调用外部定义的函数吗? [英] Can Z3 call an externally defined function?

问题描述

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

I am using Z3opt. The majority of my model can be expressed in standard SMTLIB but part of it needs to be implemented in a general purpose programming language with constructs like string processing, associative arrays etc.

是否可以在 Z3 模型中使用外部定义的函数?我知道这会降低求解器的性能，但这只是模型的一小部分.

Is it possible to use an externally defined function in a Z3 model? I know this would kill solver performance but it would only be a small part of the model.

-- 编辑澄清--

我希望提供约束的实现(作为函数指针或等效函数)，以支持 Z3 不支持的函数(例如触发函数).当使用像这样的黑盒约束时，我会接受 Z3 不能应用任何启发式的权衡.

I wish to supply the implementation of a constraint (as a function pointer or equivalent) in order to support functions not supported by Z3 (e.g. trig functions). I would accept the tradeoff that Z3 cannot apply any heuristics when using a blackbox constraint like this.

推荐答案

您可以从 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，如果你实现了它，你可以添加一个拉取请求.

You can load SMTLIB assertions from the binary interfaces that Z3 exposes, and then use Z3 from python, Java, .NET, C++, Ocaml to perform other operations before calling into the code that checks feasibility or optimizes objectives. The z3opt tutorial on http://rise4fun.com/z3opt contains pointers to Phan's F# code that exemplifies using the binary API (in this case from F#/.NET). The examples directory in the source code contains examples of using the various APIs. If you need something fancier that isn't exposed, then the default fallback is based on Z3 being open source so you can add any special feature you desire. If you feel there is a useful feature of general interest it would be useful to track an issue on https://github.com/z3prover/z3.git, and if you have it implemented you can add a pull request.

这篇关于Z3 可以调用外部定义的函数吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！