Z3 for Javaを使用した現在のプロジェクトで、いくつかのパフォーマンスの問題が発生しています。基本的に、現在の制約のほとんどは非常に単純です。例： (f(x) = 2 && f(y) <= 3) || f(x) <=5
プロジェクト全体で共有される静的コンテキストとソルバーインスタンスを使用しています。
public class ConstraintManager {
static Context ctx;
static Solver solver;
...
}
ctxの同じインスタンスで数十億回exprを生成した場合、それは問題になりますか？呼び出すのに最適な時期はいつctx.Dispose()ですか、またはctxを管理するための最良の方法は何ですか？
次のexpr.Simplify()ようないくつかの制約を単純化するために呼び出しましたf(x)=3 && f(x)<=2。しかし、このAPIは非常に遅いことが判明しました。特に制約の長さが増加しました。これは既知の問題ですか、それとも間違って使用したためですか？
を使用しexpr.substitute(expr1, expr2)ていますが、z3が置換後にexprをlet-binding形式に変換することに気付きました。これは数式をよりコンパクトにするためですか？
.NETおよびJavaAPIは、ガベージコレクターを使用して用語の有効期間を管理します。それらはGCの裁量でリサイクルされます。最高のパフォーマンスを得るには、参照カウントを自分で管理できますが、サポートされているAPIをバイパスする必要があります。リリースされたソースコードには、これに関連するJNI / pinvokeが含まれています。独自の低レベルAPIをローリングするのは大変な作業であり、低レベルの参照カウントもサポートされているAPIほど簡単にプログラミングできないことに注意してください。
この記事はインターネットから収集されたものであり、転載の際にはソースを示してください。
侵害の場合は、連絡してください[email protected]
コメントを追加