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)检索与理论变量 v 关联的 enode .
此外，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的方法.实际上，每个理论插件都有这种方法。