Z3Contextを複製する

Question

Z3Contextインスタンスを複製して、新しい定義を1つのインスタンスに追加して他のインスタンスに影響を与えることができないようにする必要があります。

これは可能ですか？

私はどのAPIを調べるべきですか？

私はJava APIを使用していると言います。

ありがとうございました

Answer 1

コンテキストをクローニングする方法はありません。また、コンテキストをクローンした後、新しいコンテキストの用語や数式に対応するポインタは何でしょうか？代わりに、用語、式、ソルバー、および目標をコンテキスト間でインポートできるようにするさまざまな翻訳方法があります。たとえば、2つのコンテキスト間に用語/式をコピーするには、

 Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target); 

を使用します。

 Z3_solver Z3_API Z3_solver_translate(Z3_context source, Z3_solver s, Z3_context target); 

方法は、あなたがソルバーのクローンを作成することができます。 2つの異なるコンテキストまたは同じコンテキストの間でソルバをクローンすることができます。特に、さまざまなアサーションのバリエーションを探索するためにクローニングを使用する場合は特にそうです。