c# - Z3 .NET API 中的设置逻辑

Question

使用 Z3 版本 3.1 时如何使用 .NET API 函数 .parseSmtlib2String(String) 时使用 set-logic？

我总是以 Z3Error-Exception 告终。

这种情况下不需要吗？

Answer 1

不幸的是，(set-logic <symbol>)使用 API 时不支持该命令parseSmtlib2String。

由于技术原因，我们有此限制。在文本界面中，该命令set-logic只能在上下文初始化之前使用。基于所选逻辑初始化上下文。当使用 API 时parseSmtlib2String，上下文已经被用户初始化。因此，该命令set-logic失败，并生成解析错误。

我承认这不是理想的行为。我将研究替代方案。