我正在寻找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似乎更灵活，因为您可以通过optimize类为表达式分配权重。

目前，我不确定，因为Z3缺少文档，而gecode缺少开箱即用的变量类型。我想知道是否有人具有使用这两种工具实现SystemVerilog所能达到的任何经验。我也想听听在弹性许可下对任何其他API的任何建议。