用于约束随机化的Gecode与Z3

Question

我正在寻找一种基于C++的替代SystemVerilog语言。虽然我对SystemVerilog约束语言的简单性和灵活性有任何怀疑，但我已经决定使用Z3或Gecode来完成我正在做的工作，主要是因为它们都处于麻省理工学院的许可之下。

我要找的是：

1. 支持可变大小的位向量和位向量算术逻辑操作.例如：

bit_vector a<30>；bit_vector b<30>；约束{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随机调用可能会产生新的随机结果。壁虎似乎支持随机种子的使用。对于加权分布来说，clear.
3. Support要小得多。Gecode似乎通过加权集来支持这一点。我设想我可以在一定的条件和布尔变量之间建立一个关系，然后给这些变量增加权重。Z3似乎更灵活，因为您可以通过优化类.

为表达式分配权重。

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

Answer 1

虽然z3 (或任何SMT求解器)都可以处理所有这些，但是获得满意任务的良好抽样是很难控制的。SMT求解器是为您提供一个模型而优化的，而且它们在您想要的解决方案空间样本方面没有太多。

顺便说一句，这是SMT解决中的一个积极研究领域。这是一篇6周前才发表的关于这个主题的论文：https://ieeexplore.ieee.org/document/8894251

因此，如果支持“良好抽样”是您的主要动机，那么使用SMT求解器可能不是最好的选择。如果您的目标是为表示方便的位向量找到令人满意的假设(现在的任何语言都有高级的API)，那么z3将是一个非常好的选择。

从你的描述来看，好的采样听起来是最主要的动机，而对于SMT的求解者可能并不是很好。至少暂时不是。