我正在寻找SystemVerilog语言的基于C ++的替代方法。尽管我怀疑那里是否有任何东西可以与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的任何建议。
尽管z3（或任何SMT求解器）可以处理所有这些问题，但是要获得令人满意的分配的良好采样将非常难以控制。 SMT求解器已经过优化，仅能为您提供模型，而且在您要如何求解解决方案空间方面，它们没有多少。
顺便说一下，这是SMT解决中的活跃研究领域。这是一篇仅在6周前就此主题发表的论文：https://ieeexplore.ieee.org/document/8894251
因此，如果支持“良好采样”是您的主要动机，那么使用SMT求解器可能不是最佳选择。如果您的目标是找到方便表达的位向量的令人满意的假设（这些天您可以想象使用任何语言的高级API），那么z3将是一个非常好的选择。
根据您的描述，良好的采样听起来像是主要动机，而对于SMT求解器来说可能并不是那么好。至少暂时还没有。