z3 - 告诉Z3中松弛变量和原始变量之间的区别

Question

我正在尝试创建一种新的剪辑来替代 Z3 中实施的 gomory 剪辑。我设计了我的剪辑以使用用户输入的原始约束。不幸的是，我发现约束的 Z3 预处理添加了松弛变量并改变了约束的结构。我可以调整我的算法以使用 Z3 约束结构和松弛变量，但算法的关键部分需要知道哪些变量是松弛变量，哪些是原始变量。我在 Z3 源代码中找不到任何东西来帮助我做到这一点。我也尝试在网上搜索解决方案，但找不到任何东西。

有谁知道如何做到这一点？

谢谢

Answer 1

mk_gomory_cut(row const & r)在文件中的方法中src/smt/theory_arith_int.h，r是Simplex 表的一行。此外，基变量x_i是整数，但它被分配了一个非整数值。

迭代器it用于遍历行条目。每个条目本质上是一对a_ij和x_j，其中a_ij是数字并且x_j是（理论）变量。

Theory_arith 是文件中定义的求解器的插件src/smt/smt_context.h。该求解器结合了许多理论插件，例如 theory_arith。它维护从表达式到理论变量的映射。此映射存储在一个名为 的对象中enode。

该方法get_enode(v)检索与理论变量关联的 enode v。此外，get_enode(v)->get_owner()返回与理论变量关联的表达式v。

现在，假设我们要测试一个理论变量v是否是松弛的。首先，我们可以使用以下方法检索关联的表达式：

   app * t = to_app(get_enode(v)->get_owner())

我使用了，to_app因为理论插件只处理基本术语（即它们不包含自由变量）。如果一个复合算术项（例如或），则该变量v是一个松弛变量。也就是说，slack本质上是复合算术项的“名称”。我们可以使用以下方法进行测试：t(+ a b)(* a b c)

  t->get_family_id() == get_id()

如果此表达式的计算结果为true，则t是一个复合算术项，因此v是一个松弛项。

备注：get_id()是一种方法theory_arith。实际上，每个理论插件都有这个方法。