时间戳

首页 > 解决方案 > 用于约束随机化的 Gecode 与 Z3

c++ - 用于约束随机化的 Gecode 与 Z3

问题描述

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

我正在寻找的是：

  1. 支持可变大小的位向量和位向量算术逻辑运算。例如：
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，鉴于其文档的详尽程度，它会更加清晰。

  1. 一个简单的约束规划模型，接近或类似于 SystemVerilog。例如，我只需要输入 (x == y + z) 而不是 EQ(x, y + z) 之类的语言。据我所知，这两个 API 都提供了如此简单的编程模型。

  2. 为了产生随机刺激而执行约束随机化的一种方法。如，我可以提供一些随机种子，根据约束条件，产生的答案可能与之前的答案不同。类似于 SystemVerilog 随机调用可能会产生新的随机结果。Gecode 似乎支持使用随机种子。Z3，不太清楚。

  3. 支持加权分布。Gecode 似乎通过加权集支持这一点。我想我可以在某些条件和布尔变量之间建立关系，然后为这些变量添加权重。Z3 似乎更灵活，因为您可以通过优化类为表达式分配权重。

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

标签： c++constraintsz3constraint-programminggecode

解决方案

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

顺便说一句，这是 SMT 求解的一个活跃研究领域。这是一篇仅在 6 周前出现的关于这个主题的论文：https ://ieeexplore.ieee.org/document/8894251

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

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

推荐阅读