用于约束随机化的 Gecode 与 Z3答案

【问题标题】：Gecode vs. Z3 for Constrained Randomization用于约束随机化的 Gecode 与 Z3
【发布时间】：2020-01-27 17:36:09
【问题描述】：

我正在寻找基于 C++ 的 SystemVerilog 语言替代方案。虽然我怀疑任何东西都无法与 SystemVerilog 约束语言的简单性和灵活性相媲美，但我决定使用 Z3 或 Gecode 来完成我的工作，主要是因为它们都在 MIT 许可下。

我正在寻找的是：

支持可变大小的位向量和位向量算术逻辑运算。例如：

bit_vector a<30>;
bit_vector b<30>;
constraint { 
    a == (b << 2);
    a == (b * 2);
    b < a;
}

据我所知，Gecode 的问题在于它没有提供开箱即用的位向量。然而，它的编程模型似乎有点简单，它确实提供了一种方法来创建自己的变量类型。因此，我或许可以围绕 C++ 位集创建某种包装器，类似于 IntVar 包装 32 位整数的方式。但是，这将缺乏执行基于乘法的约束的能力，因为 C++ 位集不支持此类操作。

Z3 确实提供了开箱即用的位向量，但我不确定它会如何处理尝试设置约束，例如 128 位向量。我也不确定如何指定我想尽可能生成满足约束的各种随机变量。使用 Gecode，鉴于其文档的详尽程度，它会更加清晰。

一个简单的约束规划模型，接近或类似于 SystemVerilog。例如，我只需要输入 (x == y + z) 而不是 EQ(x, y + z) 之类的语言。据我所知，这两个 API 都提供了如此简单的编程模型。
一种执行约束随机化的方法，以产生随机刺激。如，我可以提供一些随机种子，根据约束条件，产生的答案可能与之前的答案不同。类似于 SystemVerilog 随机调用可能会产生新的随机结果。 Gecode 似乎支持使用随机种子。 Z3，就不太清楚了。
支持加权分布。 Gecode 似乎通过加权集支持这一点。我想我可以在某些条件和布尔变量之间建立关系，然后为这些变量添加权重。 Z3 似乎更灵活，您可以通过优化类为表达式分配权重。

目前，我还没有决定，因为 Z3 缺乏 Gecode 在开箱即用的变量类型中所缺乏的文档。我想知道是否有人有任何使用这两种工具的经验来实现 SystemVerilog 的功能。我也想听听对灵活许可下的任何其他 API 的任何建议。

【问题讨论】：

标签： c++ constraints z3 constraint-programming gecode

【解决方案1】：

虽然 z3（或任何 SMT 求解器）可以处理所有这些问题，但要获得令人满意的分配的良好采样将很难控制。 SMT 求解器经过优化，只为您提供一个模型，并且在您希望如何对解决方案空间进行采样方面没有太多内容。

顺便说一下，这是 SMT 求解的一个活跃研究领域。这是一篇仅在 6 周前就该主题发表的论文：https://ieeexplore.ieee.org/document/8894251

所以，如果支持“良好采样”是您的主要动机，那么使用 SMT 求解器可能不是最佳选择。如果您的目标是为方便地表达的位向量找到令人满意的假设（如今您可以想象的任何语言都有高级 API），那么 z3 将是一个非常好的选择。

根据您的描述，良好的采样听起来像是主要动机，因此 SMT 求解器可能不是那么好。至少暂时不会。

【讨论】：

这实际上是您链接到的一篇很棒的论文。事实上，作者专门开发了 Z3 本身的补丁版本！也许有一天我们会在 Z3 中看到它。