z3 - z3 のシンボリック変数

Question

z3ソルバーに「シンボリック」ソリューションを発行させる方法はありますか? たとえば、方程式の場合:

1+x=c

解は x=c-1 ですが、z3 は常に のような特定のモデルを出力し[c = 0, x = -1]ます。cをシンボリック変数として「定義」する方法は?

Answer 1

残念ながら、Z3 はこの種の機能を公開していません。内部ではソルバーを使用していますが、API では公開されていません。将来のバージョンでは、ソルバー、Grobner bases プロシージャなどの内部コンポーネントを公開したいと考えています。現在のバージョンでは、solve-eqs( http://rise4fun.com/Z3Py/tutorial/strategiesを参照) という戦術があります。ガウス消去法の一般化を使用して変数を消去します。ただし、これは前処理ステップであり、どの変数を削除するかを制御することはできません。