告诉松弛变量和原始变量之间的差异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

回答

相关问题