Z3 .NET中的Set-Logic API

Question

使用Z3版本3.1時，如何在使用.NET API函數.parseSmtlib2String（String）時使用set-logic？

我總是以Z3Error異常結束。

在這種情況下不需要嗎？

Answer 1

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

由於技術原因，我們有這個限制。 在文本界面中，命令set-logic只能在上下文初始化之前使用。上下文根據選定的邏輯進行初始化。當使用API​​ parseSmtlib2String時，上下文已經由用戶初始化。因此，命令set-logic失敗，並生成解析錯誤。

我承認這不是理想的行爲。我會調查替代品。