Combining Stable Infiniteness and (Strong) Politeness
Combining Stable Infiniteness and (Strong) Politeness
复制标题
DOI：
10.1007/s10817-023-09684-0
复制
发表时间：
2023-12-01
期刊：
影响因子：
--
通讯作者：
Tinelli，Cesare
中科院分区：
文献类型：
--
作者：
Sheng，Ying;Zohar，Yoni;Tinelli，Cesare
礼貌理论组合是一种方法，用于获得两个（或更多）理论的组合的求解器，使用每个单独理论的求解器作为黑盒。与早期的纳尔逊-奥本方法不同，该方法仅在两个理论都是稳定无限时才可用，只有一个理论需要是强礼貌的才能使用礼貌组合方法。在其最初的介绍中，礼貌是从理论之一，而不是强礼貌，后来被证明是不够的。本文的第一个贡献是证明，这两个概念确实是不同的，通过提出一个礼貌的理论，是不是很礼貌。我们还研究了这个问题的几个变体。与纳尔逊-奥本方法相比，礼貌组合方法提供的一般性的代价是需要考虑更大的安排空间，涉及的变量不一定在输入公式的纯化部分之间共享。本文的第二个贡献是一个混合方法（建立在礼貌和纳尔逊-奥本组合），其目的是减少所考虑的变量的数量时，理论是稳定的无限的一些种类，但不是所有的。在最坏的情况下，推理安排所需的时间是指数级的，因此减少考虑的变量数量有可能显著提高性能。我们通过展示智能合约验证基准的显着加速来展示这一点的初步证据。
Polite theory combination is a method for obtaining a solver for a combination of two (or more) theories using the solvers of each individual theory as black boxes. Unlike the earlier Nelson–Oppen method, which is usable only when both theories are stably infinite, only one of the theories needs to be strongly polite in order to use the polite combination method. In its original presentation, politeness was required from one of the theories rather than strong politeness, which was later proven to be insufficient. The first contribution of this paper is a proof that indeed these two notions are different, obtained by presenting a polite theory that is not strongly polite. We also study several variants of this question.The cost of the generality afforded by the polite combination method, compared to the Nelson–Oppen method, is a larger space of arrangements to consider, involving variables that are not necessarily shared between the purified parts of the input formula. The second contribution of this paper is a hybrid method (building on both polite and Nelson–Oppen combination), which aims to reduce the number of considered variables when a theory is stably infinite with respect to some of its sorts but not all of them. 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 significant speed-up on a smart contract verification benchmark.