在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會神奇地找出要做什麼。