scala - Scala^Z3 でロジック/オプションを設定する

Question

Scala ^ Z3でロジックとそれに応じたオプションを設定する方法がわかりません。それは本当に簡単だと思いますが、私はそれを見つけることができません..だから私はそこにいくつかの助けを本当に感謝します;)

よろしく、フロリアン

ps .: Scala 3.2 と Z3 4.0 は非常にうまく連携します :)

Answer 1

あなたがまだ探している場合...

オプションを設定するには、次の2つの方法があります。

1. Z3Configインスタンスを作成するときにパラメータを渡します。例： new Z3Config("MODEL" -> true)。
2. インスタンスを.setParamValue呼び出します。例： 。Z3ConfigmyConf.setParamValue("MODEL", true)

ここで、ロジックの設定方法に関する特定の質問に答えます。これは、残念ながらZ3のAPIではサポートされていません。C＃に関するこの同様の質問に対するLeoの回答を見ることができます。

ただし、厳密に言えば、APIを使用する場合は、このオプションは実際には必要ありません。すべての理論を使用でき、Z3は魔法のように何をすべきかを理解します。