Politeness and Stable Infiniteness: Stronger Together
Politeness and Stable Infiniteness: Stronger Together
复制标题
礼貌与稳定无限：强强联手
DOI：
10.1007/978-3-030-79876-5_9
复制
发表时间：
2021
影响因子：
7.3
通讯作者：
C. Tinelli
中科院分区：
文献类型：
--
作者：
Ying Sheng;Yoni Zohar;C. Ringeissen;Andrew Reynolds;Clark W. Barrett;C. Tinelli
本文对可满足模理论中礼貌组合的研究做出了两个贡献。第一种是通过提出一种非强礼貌的礼貌理论来区分礼貌和强礼貌。这一结果表明，为了使用礼貌组合，有时需要证明强礼貌（这往往比证明礼貌更难）。第二个贡献是优化礼貌的组合方法，通过借用纳尔逊-奥本方法。纳尔逊-奥本方法是基于对共享变量的猜测安排。相比之下，礼貌组合需要对共享排序的所有变量进行安排。我们表明，当使用礼貌的组合，如果其他的理论是稳定的无限的共享排序，只有共享变量的排序需要考虑的安排，在纳尔逊-奥本方法。在最坏的情况下，推理安排所需的时间是指数级的，因此减少考虑的变量数量有可能显著提高性能。我们通过展示智能合约验证基准的加速来展示这一点的初步证据。
We make two contributions to the study of polite combination in satisfiability modulo theories. The first is a separation between politeness and strong politeness, by presenting a polite theory that is not strongly polite. This result shows that proving strong politeness (which is often harder than proving politeness) is sometimes needed in order to use polite combination. The second contribution is an optimization to the polite combination method, obtained by borrowing from the Nelson-Oppen method. The Nelson-Oppen method is based on guessing arrangements over shared variables. In contrast, polite combination requires an arrangement over all variables of the shared sorts. We show that when using polite combination, if the other theory is stably infinite with respect to a shared sort, only the shared variables of that sort need be considered in arrangements, as in the Nelson-Oppen method. The time required to reason about arrangements is exponential in the worst case, so reducing the number of variables considered has the potential to improve performance significantly. We show preliminary evidence for this by demonstrating a speed-up on a smart contract verification benchmark.