在Scala设置逻辑/选项^ Z3

Question

我无法弄清楚，如何在Scala^Z3中设置逻辑和相应的选项。 猜它很简单，但我无法找到它..所以我真的很希望得到一些帮助那里;）

问候， 弗洛里安

PS：斯卡拉3.2和4.0 Z3工作真的没事在一起:)

Answer 1

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

有两种方法来设置选项：

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

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

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