scala - 在 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 会神奇地找出要做什么。