z3 - Z3 是否使用了用户在“AUFLIA-p”部分中为 smtComp 结果提供的模式？

Question

我正在测试一些简化的一般性（主要是：有向部分量词实例化）。因此，我在 smtComp 的“AUFLIA-p”部分运行了一组基准测试，无论是否简化。为了尽可能减少副作用，我有兴趣在没有（用户提供）模式的情况下运行 Z3。

我在“AUFLIA-p”部分检查了一些基准，我想知道为什么这部分的基准包含模式。也许您已经为本节运行了 Z3，并带有禁用模式的选项。最近，我刚刚放弃了一些基准测试中的模式，并观察到性能的急剧下降。

问题：
“AUFLIA-p”和“AUFLIA+p”部分之间有什么区别吗？
我如何告诉 Z3 忽略（用户提供的）模式？

问候，
Aboubakr Achraf El Ghazi

Answer 1

AUFLIA-p 和 AUFLIA+p 之间的区别在于前者不包含模式，但后者包含。然而，SMTLIB 中只有一类基准，称为 AUFLIA。（一些）这些基准包含在运行工具之前在 SMTCOMP 期间被删除的模式。例如，比较unscrambled benchmark和scrambled benchmark，其中第一个确实包含模式，但后者不包含。

我相信模式的去除是通过基准加扰器完成的。