境界モデルのチェックに Z3 を使用しています。この目的のために、次の形式の式を多数提供します。
state_A_1 && !state_B_1 && sometrigger => !state_A_2 & state_B_2
つまり、時間ステップごとに個別の式を提供することで、時間の経過 (ステップ) をエンコードします。明らかに、これは数千の式になります。
Z3 がそれらを解決するのにかかる時間は (私たちが持っているステート マシンの複雑さのために) 許容範囲ですが、Z3 JNI Java API を介してこれらすべての式を構築するには非常に長い時間 (数秒) がかかります。
では、私の質問は次のとおりです。特殊な API を使用して、これらすべてのタイム アンロール式を作成するように Z3 に指示する簡単な方法はありますか?
おそらく、タイムステップをエンコードする関数を作成できます（例：TimeStep new = Next(old)）。
Z3 には、解釈されていない関数と量指定子を拡張式に変換できる「マクロ ファインダー」があります。すべてZ3内部なので、この方法で拡張を作成する方が速いかもしれません。
それ以外は、式作成のパフォーマンスが優れていることがわかりました。あなたのコードは非常に非効率的ではないでしょうか? プロファイリングします。Z3 が遅いとどのように結論付けましたか?
あなたの状況を改善する Z3 の高速 API については知りません。数秒で数千の表現はアプリオリにそれほど悪くはありません。プロファイリングや並列処理などの従来のアプローチも引き続き使用できます。
また、問題が許せば、ブール変数で作業するのではなく、それらをビットベクトルに因数分解してベクトルレベルで作業することを考えることができます (つまり、すべての変数を 1 つずつ処理するのではなく、変数のグループを一度に処理します)。あなたの問題はそれを可能にします）時間を節約します。