告訴鬆弛變量和原始變量之間的差異Z3

我試圖創建一種新的切口，以取代在Z3實施的削減戈莫里。我設計了我的剪裁以使用用戶輸入的原始約束。不幸的是我發現約束的Z3預處理增加了鬆弛變量並改變了約束的結構。我可以使我的算法適應Z3約束結構和鬆弛變量，但算法的關鍵部分需要知道哪些變量是鬆弛變量，哪些變量是原始變量。我在Z3源代碼中找不到任何東西來幫助我做到這一點。我也嘗試在線搜索解決方案，但找不到任何東西。告訴鬆弛變量和原始變量之間的差異Z3

有誰知道這可以做到嗎？

由於

來源

2013-04-09 omerkatz

在調用Z3之前是否添加了切口？或者，你在修改theory_arith類嗎？你看了一下'src/smt/theory_arith_int.h'文件嗎？ – 2013-04-09 16:10:30

我正在嘗試修改thoery_arith類。我已經研究了'src/smt/theory_srith_int。h'文件和其中的代碼產生gomory削減，但我沒有找到我的問題在該文件中的答案 – omerkatz 2013-04-09 17:07:40

在該方法mk_gomory_cut(row const & r)文件src/smt/theory_arith_int.h中，r是單純形表的一行。而且，基本變量x_i是整數，但它被分配給一個非整數值。

該迭代it被用於遍歷行條目。每個條目基本上是一對a_ij和x_j，其中a_ij是數字和x_j是（理論）變量。

的theory_arith是文件src/smt/smt_context.h中定義的解算器的插件。這個求解器結合了許多理論插件，如theory_arith。它維護從表達式到理論變量的映射。該映射存儲在名爲enode的對象中。

方法get_enode(v)檢索與理論變量v相關聯的e節點。此外，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的方法。其實，每個理論插件都有這個方法。

來源

2013-04-09 17:38:27

感謝您的幫助！ – omerkatz 2013-04-09 18:10:48

告訴鬆弛變量和原始變量之間的差異Z3

回答

相關問題