In the field of static analysis of logic programs, the optimality of abstract operators is a valuable theoretical property, as it provides insight into the structure of abstract domains and the maximum precision that can be achieved. However, implementing optimal operators is often complex and may significantly impact performance, giving rise to a trade-off between precision and efficiency. We experimentally investigate this trade-off in the context of sharing and linearity analysis of logic programs. Our experiments build on previous work that proposed several optimal operators for unification and matching. We have implemented these abstract operators and the corresponding abstract domains within the PLAI analyzer, part of the CiaoPP preprocessor, and we report the impact of increasing operator precision on the accuracy and performance of the overall analysis.

翻译：在逻辑程序的静态分析领域中，抽象算子的最优性是一项极具价值理论性质，它有助于揭示抽象域的结构以及可达到的最大精度。然而，最优算子的实现往往较为复杂，并可能显著影响性能，从而在精度与效率之间形成权衡。本文针对共享性和线性分析中的这种权衡开展实验研究。我们的实验基于先前提出的用于合一与匹配的若干最优算子。我们在CiaoPP预处理器中PLAI分析器内实现了这些抽象算子及相应的抽象域，并报告了提高算子精度对整体分析准确性和性能的影响。