私はZ3optを使用しています。私のモデルの大部分は標準SMTLIBで表現することができますが、その一部は文字列処理、連想配列などの構造を持つ汎用プログラミング言語で実装する必要があります。Z3が外部定義された関数を呼び出すことはできますか？
外部定義関数をZ3モデル？私はこれがソルバーのパフォーマンスを殺すだろうが、モデルのほんの一部に過ぎないことを知っています。
- 明確化のために編集 -
IはZ3（例えば三角関数）によってサポートされない機能をサポートするために（関数ポインタまたは同等品など）の制約の実装を提供することを望みます。私はZ3がこのようなブラックボックスの制約を使うとき、ヒューリスティックを適用できないというトレードオフを受け入れるだろう。
Z3が公開するバイナリインターフェイスからSMTLIBアサーションを読み込み、Python、Java、.NET、C++、OcamlからZ3を使用して、実現可能性をチェックしたり目的を最適化するコードを呼び出す前に他の操作を実行できます。 http://rise4fun.com/z3optのz3optチュートリアルには、バイナリAPI（この場合はF＃/ .NET）を使用する例を示すPhanのF＃コードへのポインタが含まれています。ソースコード内のexamplesディレクトリには、さまざまなAPIの使用例が含まれています。 公開されていない好きなものが必要な場合、デフォルトのフォールバックはZ3がオープンソースであることに基づいているため、必要な特別な機能を追加できます。有用な一般的な機能があると感じたら、https://github.com/z3prover/z3.gitの問題を追跡すると便利です。実装している場合はプルリクエストを追加できます。
私はZ3を呼び出す前に前処理ステップを提案していると思いますが、それでは不十分です。私が探しているのは、順列をテストするときにソルバによって呼び出されるカスタムアサーションを書く方法です。 – daw
Nikolajが言及しているAPIを見てください。 – Heyji
私は、APIを使用して小分けのz3 SMTLIB式を構築することについて質問していません。 Z3でサポートされていない関数（trig関数など）をサポートするために、（関数ポインタまたは同等のものとして）制約の実装を提供したいと思います。私は実際の答えはそれができないことだと思います。 – daw