z3 - Z3 ソルバーのコピー

Question

私は投稿で見ました: Z3_context を複製することは可能ですか? バックトラッキング動作を容易にするために、ソルバーをコピー/クローンする機能が Z3 に追加される予定でした。C API ドキュメントを調べましたが、現在これを行う方法を見つけることができませんでした。

C API を介してソルバーをコピーできるようになりましたか?

Answer 1

API には Solver オブジェクトをコピーするメソッドはありませんが、 と を使用してシミュレートできZ3_solver_get_assertionsますZ3_solver_assert。アイデアは、新しい Solver オブジェクトを作成し、アサーションを古いものから新しいものにコピーすることです。