限定モデル検査にはZ3を使用しています。我々は、各時間ステップに対して別々 表現を供給することによって、時間の経過（ステップ）をコードする、換言すればZ3による限定モデル検査 - 式の構築
state_A_1 && !state_B_1 && sometrigger => !state_A_2 & state_B_2
：この目的のために、我々は次の形式の式の全体 束を供給する。明らかに、これは数千の表現をもたらします。
Z3がそれらを解決するのにかかる時間は許容されますが（ステートマシンの複雑さのため）、Z3 JNI Java APIを通してこれらの式をすべて構築するにはかなりの時間（数秒）がかかります。
これは私の質問です：Z3にこれらのすべての特殊なAPIを使って時間展開された式をすべて作成するように伝える簡単な方法はありますか？
あなたの状況を改善するZ3の高速APIは認識していません。数秒で何千もの表現がそれほど先験的に悪くはありません。プロファイリングや並列処理のような伝統的なアトリビュートはまだあります。
また、ブール変数で作業するのではなく、ビットベクトルに分解してベクトルレベルで作業することも考えられます（つまり、すべての変数を1つずつ処理するのではなく、一度に変数のグループを処理します）あなたの問題が許せば、時間を節約することができます。
おそらくタイムステップをエンコードする関数を作成することができます（たとえば、TimeStep new = Next(old)）。
Z3には、未解釈関数と量子を拡張した式に変換できる「マクロファインダ」があります。おそらくZ3のすべての内部のため、この方法で拡張を作成する方が速いでしょう。
そうでなければ、表現作成のパフォーマンスが良いことがわかりました。あなたのコードが非常に非効率的であるかどうか疑問に思いますか？プロフィール。 Z3が遅いとあなたはどのように結論づけましたか？
ありがとうございます！私たちは関数ベースのアプローチを試みます。どのようにコードが非効率的であるかわかりません：私はforループでAPIを呼び出し、引用した時間はAPI呼び出しの裸の時間でした他の（回避可能な）処理をせずにZ3を遅らせていると非難するわけではありません。私たちがやるべきことをするためのより良い方法を探しています。 –
ビット "長時間"と多くの多くの表現を定量化してもよろしいですか？また、これらの式をどのように構築するのですか（テキストファイルからの読み込み、またはその場での計算方法） – Heyji
式は、Java/JNI APIを呼び出すことによって別のデータ構造から即座に構築されました。数秒以内 –