我们使用 Z3 进行有界模型检查。为此，我们提供了一大堆如下形式的表达式：
state_A_1 && !state_B_1 && sometrigger => !state_A_2 & state_B_2
换句话说，我们通过为每个时间步提供单独的表达式来编码时间（步）的流逝。显然，这会导致数千个表达式。
虽然 Z3 解决这些问题所花费的时间是可以接受的（考虑到我们拥有的状态机的复杂性），但通过 Z3 JNI Java API 构建所有这些表达式需要相当长的时间（几秒钟）。
所以这是我的问题：有没有更简单的方法来告诉 Z3 通过一些专门的 API 创建所有这些时间展开的表达式？
也许您可以制作一个对时间步长进行编码的函数（例如TimeStep new = Next(old)）。
Z3 有一个“宏查找器”，可以将未解释的函数和量词转换为扩展表达式。也许以这种方式创建扩展更快，因为它都是 Z3 内部的。
否则，我发现表达式创建性能很好。我想知道您的代码是否效率很低？剖析它。您是如何得出 Z3 速度慢的结论的？
我不知道 Z3 中有任何快速 API 可以改善您的情况。几秒钟内的几千个表达方式并没有那么糟糕。您仍然拥有像分析和并行处理这样的传统方法。
此外，如果您的问题允许，而不是使用布尔变量，您可以考虑将它们分解为位向量并在向量级别工作（即一次处理一组变量，而不是一个一个地处理所有变量）这可以（如果你的问题允许它）节省一些时间。