Abstract
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.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Notes
In [22] this was proven more generally, for order-sorted logics which extend many-sorted logics with subsorts.
For the results proven below, this full generality regarding V is not needed (e.g., it is sufficient to consider only variables in \(\phi \)). However, for the validity of other results in polite theory combination, an arbitrary (finite) V is required. For more details, see Footnote 4 of [14].
In [9], the first condition is written \({\left| \sigma _{1}^{{{\mathcal {A}}}}\right| }\ge 2\). We use equality as this is equivalent and we believe it makes things clearer.
The case of non-empty signatures is addressed in a recent paper by Toledo et al. [24].
Notice that \({{{\mathcal {T}}}_{\textrm{Even}}^{\infty }}\) can be axiomatized using the set \(\left\{ \lnot \psi _{=2n+1}^{\sigma }\mid n\in {\mathbb {N}}\right\} \) (see Fig. 2).
An artifact which includes the compiled binary of the implementation, the benchmark, the raw results, as well as reproduction instructions is available at https://doi.org/10.5281/zenodo.6538824.
References
Amsden, Z., Arora, R., Bano, S., Baudet, M., Blackshear, S., Bothra, A., Cabrera, G., Catalini, C., Chalkias, K., Cheng, E., Ching, A., Chursin, A., Danezis, G., Giacomo, G.D., Dill, D.L., Ding, H., Doudchenko, N., Gao, V., Gao, Z., Garillot, F., Gorven, M., Hayes, P., Hou, J.M., Hu, Y., Hurley, K., Lewi, K., Li, C., Li, Z., Malkhi, D., Margulis, S., Maurer, B., Mohassel, P., de Naurois, L., Nikolaenko, V., Nowacki, T., Orlov, O., Perelman, D., Pott, A., Proctor, B., Qadeer, S., Rain, Russi, D., Schwab, B., Sezer, S., Sonnino, A., Venter, H., Wei, L., Wernerfelt, N., Williams, B., Wu, Q., Yan, X., Zakian, T., Zhou, R.: The Diem blockchain. https://developers.diem.com/docs/technical-papers/the-diem-blockchain-paper/ (2019)
Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Noetzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: a versatile and industrial-strength SMT solver. In: Proceedings of TACAS 2022 (2022)
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org
Barrett, C.W.: Checking validity of quantifier-free formulas in combinations of first-order theories. Ph.D., Stanford University (2003). http://www.cs.stanford.edu/~barrett/pubs/B03.pdf. Stanford, California
Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification—23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14–20, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6806, pp. 171–177. Springer, New York (2011). https://doi.org/10.1007/978-3-642-22110-1_14
Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisfiability Boolean Model. Comput. 3(1–2), 21–46 (2007)
Blackshear, S., Cheng, E., Dill, D.L., Gao, V., Maurer, B., Nowacki, T., Pott, A., Qadeer, S., Rain, Russi, D., Sezer, S., Zakian, T., Zhou, R.: Move: a language with programmable resources. https://developers.diem.com/docs/technical-papers/move-paper/ (2019)
Casal, F., Rasga, J.: Revisiting the equivalence of shininess and politeness. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8312, pp. 198–212. Springer, New York (2013). https://doi.org/10.1007/978-3-642-45221-5_15
Casal, F., Rasga, J.: Many-sorted equivalence of shiny and strongly polite theories. J. Autom. Reason. 60(2), 221–236 (2018). https://doi.org/10.1007/s10817-017-9411-y
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (2001)
Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16–18, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5749, pp. 263–278. Springer, New York (2009). https://doi.org/10.1007/978-3-642-04222-5_16
Jovanovic, D., Barrett, C.W.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning—17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings, Lecture Notes in Computer Science, vol. 6397, pp. 402–416. Springer, New York (2010). https://doi.org/10.1007/978-3-642-16242-8_29
Jovanovic, D., Barrett, C.W.: Polite theories revisited. Tech. rep., New York University (2019). http://theory.stanford.edu/~barrett/pubs/JB10-TR.pdf. Technical Report TR2010-922
Krstic, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24–April 1, 2007, Proceedings, Lecture Notes in Computer Science, vol. 4424, pp. 602–617. Springer, New York (2007). https://doi.org/10.1007/978-3-540-71209-1_47
Leino, K.R.M.: This is Boogie 2. manuscript KRML 178(131), 9 (2008). https://www.microsoft.com/en-us/research/publication/this-is-boogie-2-2/
Nelson, G.: Techniques for program verification. Tech. Rep. CSL-81-10, Xerox, Palo Alto Research Center (1981)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979). https://doi.org/10.1145/357073.357079
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19–21, 2005, Proceedings, Lecture Notes in Computer Science, vol. 3717, pp. 48–64. Springer, New York (2005). Extended technical report is available at https://hal.inria.fr/inria-00070335/
Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Politeness for the theory of algebraic datatypes. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning—10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I, Lecture Notes in Computer Science, vol. 12166, pp. 238–255. Springer, New York (2020). https://doi.org/10.1007/978-3-030-51074-9_14
Sheng, Y., Zohar, Y., Ringeissen, C., Reynolds, A., Barrett, C.W., Tinelli, C.: Politeness and stable infiniteness: stronger together. In: CADE, Lecture Notes in Computer Science, vol. 12699, pp. 148–165. Springer, New York (2021)
Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J.A. (eds.) Logics in Artificial Intelligence, 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27–30, 2004, Proceedings, Lecture Notes in Computer Science, vol. 3229, pp. 641–653. Springer, New York (2004)
Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reason. 34(3), 209–238 (2005). https://doi.org/10.1007/s10817-005-5204-9
Toledo, G., Zohar, Y., Barrett, C.: Combining combination properties: an analysis of stable infiniteness, convexity, and politeness. In: Proceedings of CADE 2023 (2023)
Zhong, J.E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C.W., Dill, D.L.: The Move prover. In: Lahiri, S.K., Wang, C., (eds.) Computer Aided Verification—32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part I, Lecture Notes in Computer Science, vol. 12224, pp. 137–150. Springer, New York (2020). https://doi.org/10.1007/978-3-030-53288-8_7
Author information
Authors and Affiliations
Contributions
All authors contributed equally.
Corresponding author
Ethics declarations
Competing interests
The authors declare no competing interests.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This work was funded in part by the Stanford Center for Blockchain Research, NSF-BSF Grant numbers 2110397 (NSF) and 2020704 (BSF), ISF Grant number 619/21, and a gift from Meta Novi to the University of Iowa.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Sheng, Y., Zohar, Y., Ringeissen, C. et al. Combining Stable Infiniteness and (Strong) Politeness. J Autom Reasoning 67, 34 (2023). https://doi.org/10.1007/s10817-023-09684-0
Received:
Accepted:
Published:
DOI: https://doi.org/10.1007/s10817-023-09684-0