Z3 で実装された gomory カットを置き換える新しい種類のカットを作成しようとしています。ユーザーが入力した元の制約で動作するようにカットを設計しました。残念ながら、制約の Z3 前処理によってスラック変数が追加され、制約の構造が変更されることがわかりました。Z3 制約構造とスラック変数で動作するようにアルゴリズムを適応させることができますが、アルゴリズムの重要な部分では、どの変数がスラック変数で、どの変数が元の変数であるかを知る必要があります。Z3 のソース コードには、それを行うのに役立つものは何も見つかりませんでした。また、解決策をオンラインで検索しようとしましたが、何も見つかりませんでした。
これを行う方法を知っている人はいますか？
ありがとう
mk_gomory_cut(row const & r)ファイル内のメソッドではsrc/smt/theory_arith_int.h、Simplex rtableau の行です。さらに、基本変数x_iは整数ですが、整数以外の値に割り当てられています。
イテレータitは、行エントリをトラバースするために使用されます。各エントリは基本的に と のペアa_ijです。は数値で、x_jは(理論) 変数です。a_ijx_j
theory_arith は、ファイルで定義されたソルバーのプラグインですsrc/smt/smt_context.h。このソルバーは、theory_arith などの多くの理論プラグインを組み合わせています。式から理論変数へのマッピングを維持します。このマッピングは、 というオブジェクトに格納されますenode。
このメソッドget_enode(v)は、理論変数に関連付けられた e ノードを取得しますv。さらに、get_enode(v)->get_owner()理論変数 に関連付けられた式を返しますv。
ここで、理論変数vがスラックかどうかをテストしたいとします。まず、次を使用して関連する式を取得できます。
app * t = to_app(get_enode(v)->get_owner())
を使用しto_appたのは、理論プラグインが基底項のみを処理する (つまり、自由変数を含まない) ためです。またはなどの複合算術項の場合、変数vはスラックです。つまり、スラックは基本的に複合算術用語の「名前」です。以下を使用してこれをテストできます。t(+ a b)(* a b c)
t->get_family_id() == get_id()
この式が に評価される場合true、tは複合算術項であり、結果としてvスラックです。
備考：get_id()の方法ですtheory_arith。実際、すべての理論プラグインにはこのメソッドがあります。