变量或子表达式的数量哪个更重要？答案

【问题标题】：which is more important, number of variables or subexpressions?变量或子表达式的数量哪个更重要？
【发布时间】：2014-07-15 04:32:26
【问题描述】：

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

如果有人能回答/解释对 SMT 求解器的性能影响更大的因素、变量的数量或子表达式的数量，我将不胜感激？

【问题讨论】：

对此没有普遍有效的答案。启发式方法可能对具有更多变量的文件很幸运，或者它们可能对具有较少变量的文件不走运。我不知道这个特定文件会发生什么，因为我无法访问您的输入文件。你能把这些公开吗？
感谢您的提醒！他们现在是公开的。我不应该忘记分享它们。提前感谢您的进一步帮助！

标签： preprocessor z3 smt simplification

【解决方案1】：

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

【讨论】：

谢谢克里斯托夫。这就说得通了！我可以假设检测共享表达式是在检查 input1 时花费大部分额外时间的预处理器吗？
再次，我可以假设 z3 在预处理步骤中创建映射到共享表达式的临时变量吗？换句话说，在调用实际求解器之前，input1 和 input2 存在相同数量的变量？
Z3 使用 hash consing 来检测结构相等的表达式，因此结构相等的表达式只创建一次。确实，这可能会在施工期间产生一些时间开销。 Z3 不会为每个子表达式显式创建新变量，但如果您愿意，可以这样想（实际上它们只是内存中的指针）。
感谢您的回答！请允许我问一个天真的问题，相等表达式的结构检测发生在 z3 的解析器中，还是在求解引擎中？
每当创建表达式时都会发生这种情况，这可能是在解析器运行时，或者通过 API 调用任何 Z3_mk_* 函数时。