在 Scala^Z3 中设置逻辑/选项

Question

我不知道如何在 Scala^Z3 中设置逻辑和相应的选项。 猜猜它真的很简单，但我找不到它..所以我真的很感激那里的一些帮助;）

问候， 弗洛里安

ps.：Scala 3.2 和 Z3 4.0 可以很好地协同工作 :)

Answer 1

如果你还在寻找......

有两种设置选项的方法：

1. 在构造 Z3Config 实例时传递参数，例如new Z3Config("MODEL" -> true)。
2. 在Z3Config 实例上调用.setParamValue，例如myConf.setParamValue("MODEL", true)。

现在回答关于如何设置逻辑 的特定问题，遗憾的是 Z3 的 API 不支持该问题。你可以看看 Leo 对this similar question for C# 的回答。

请注意，严格来说，您在使用 API 时并不真正需要该选项：所有理论都可以使用，Z3 会神奇地弄清楚该怎么做。