3

我认为检测共享表达式的技术已应用于大多数现代 SMT 求解器。当它处理一系列相似的表达式时，性能应该非常好。但是，在input1和input2上运行 Z3 后，我得到了意想不到的结果。不是在“input1”中构建一个长约束A ，而是定义了一些中间变量来映射到“input2”中A的子表达式。在这种情况下，input1 的变量较少，应该比 input2 解决得更快。我无法从统计数据中找到有用的信息，因为它们除了求解时间和消耗的内存外完全相同：

z3 统计量

如果有人能回答/解释什么会更多地影响 SMT 求解器的性能，变量的数量或子表达式的数量，我将非常感激？

4

1 回答 1

2

我做了一些分析，似乎两个输入在求解器中的行为完全相同。所有（check-sat）命令都需要完全相同的时间。注意输入2是一个255KB大小的文件，而输入1是一个240MB大小的文件，即这个文件比第一个大1000倍左右。根据我的分析器，解决这些查询所需的所有额外时间都花在了解析器中。因此，读取和检查输入只需要很长时间；实际查询都很容易。

于 2014-05-29T17:08:15.970 回答