Skip to Main content Skip to Navigation
New interface
Conference papers

Politeness and Stable Infiniteness: Stronger Together

Abstract : We make two contributions to the study of polite combination in satisfiability modulo theories. The first contribution 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. In its non-deterministic form, the Nelson-Oppen method is based on guessing arrangements over shared variables. In contrast, polite combination requires an arrangement over \emph{all} variables of the shared sort (not just the shared variables). 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. Reasoning about arrangements of variables is exponential in the worst case, so reducing the number of variables that are considered has the potential to improve performance significantly. We show preliminary evidence for this in practice by demonstrating a speed-up on a smart contract verification benchmark.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03346663
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Thursday, September 16, 2021 - 3:00:50 PM
Last modification on : Friday, November 18, 2022 - 9:24:00 AM

Links full text

Identifiers

Collections

Citation

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett, et al.. Politeness and Stable Infiniteness: Stronger Together. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA / online, United States. pp.148-165, ⟨10.1007/978-3-030-79876-5_9⟩. ⟨hal-03346663⟩

Share

Metrics

Record views

20