5

QFBV フォーミュラで Z3 を使用しています。SATソルバーがブール句でできるように、Z3がそのような式で段階的に機能できるかどうか疑問に思っていました。基本的に、次のループを実装する方法が必要です。

F = initial QFBV formula
while(F is unsat) {
    F := F Union {some additional QFBV formula based on unsat core}
}

Z3 は学習した情報を維持しますか? z3 を段階的に使用できますか?

ありがとう。

4

1 に答える 1

6

はい、Z3 を使用すればそれが可能ですassumptions。これについては、ここで説明します: Z3 のソフト/ハード制約

于 2012-02-03T00:34:18.117 に答える