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

Question

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

问候，弗洛里安

ps.：Scala 3.2 和 Z3 4.0 一起工作得很好:)

Answer 1

如果你还在寻找...

有两种设置选项的方法：

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

现在回答有关如何设置逻辑的特定问题，不幸的是 Z3 的 API 不支持该问题。您可以查看 Leo对 C# 的类似问题的回答。

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