Algebraic datatypes; Automated reasoning; Polite combination; Satisfiability Modulo Theories; Theory combination; Algebraic data-types; Combination method; Datatypes; Satisfiability modulo Theories; Theory solvers; Computational Theory and Mathematics; Artificial Intelligence
Abstract :
[en] Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.
Disciplines :
Computer science
Author, co-author :
Sheng, Ying; Stanford University, Stanford, United States
Zohar, Yoni; Bar Ilan University, Ramat Gan, Israel
Ringeissen, Christophe; Université de Lorraine, CNRS, Inria, LORIA, France
Lange, Jane; MIT, Cambridge, United States
Fontaine, Pascal ; Université de Liège - ULiège > Département d'électricité, électronique et informatique (Institut Montefiore) > Systèmes informatiques distribués
Barrett, Clark; Stanford University, Stanford, United States
This project was partially supported by a Grant from the Defense Advanced Research Projects Agency (N66001-18-C-4012), the Stanford CURIS program, and Jasmin Blanchette’s European Research Council (ERC) starting Grant Matryoshka (713999)
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4:1-4:51 (2009) DOI: 10.1145/1459010.1459014
Baader, F., Snyder, W., Narendran, P., Schmidt-Schauß, M., Schulz, K.U.: Unification theory. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 Volumes), pp. 445–532. Elsevier/MIT Press, New York (2001) DOI: 10.1016/B978-044450813-3/50010-2
Barrett, C.W., Dill, D.L., Stump, A.: A generalization of shostak’s method for combining decision procedures. In: A. Armando (ed.) Frontiers of Combining Systems, 4th International Workshop, FroCoS 2002, Santa Margherita Ligure, Italy, April 8–10, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2309, pp. 132–146. Springer (2002)
Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisfiab. Boolean Model. Comput. 3(1–2), 21–46 (2007) DOI: 10.3233/SAT190028
Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of the 23rd International Conference on Computer Aided Verification, CAV’11, pp. 171–177. Springer (2011). http://dl.acm.org/citation.cfm?id=2032305.2032319
Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). Available at www.SMT-LIB.org
Berthon, R., Ringeissen, C.: Satisfiability modulo free data structures combined with bridging functions. In: T. King, R. Piskac (eds.) Proceedings of SMT@IJCAR 2016, CEUR Workshop Proceedings, vol. 1617, pp. 71–80. CEUR-WS.org (2016)
Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C.: Theory combination: Beyond equality sharing. In: C. Lutz, U. Sattler, C. Tinelli, A. Turhan, F. Wolter (eds.) Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 11560, pp. 57–89. Springer (2019)
Casal, F., Rasga, J.: Many-sorted equivalence of shiny and strongly polite theories. J. Autom. Reason. 60(2), 221–236 (2018) DOI: 10.1007/s10817-017-9411-y
Chocron, P., Fontaine, P., Ringeissen, C.: Politeness and combination methods for theories with bridging functions. J. Autom. Reason. 64(1), 97–134 (2020) DOI: 10.1007/s10817-019-09512-4
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: S. Ghilardi, R. Sebastiani (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 (2009)
Gutiérrez, R., Meseguer, J.: Variant-based decidable satisfiability in initial algebras with predicates. In: F. Fioravanti, J.P. Gallagher (eds.) Logic-Based Program Synthesis and Transformation—27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10–12, 2017, Revised Selected Papers, Lecture Notes in Computer Science, vol. 10855, pp. 306–322. Springer (2017)
Hojjat, H., Rümmer, P.: Deciding and interpolating algebraic data types by reduction. In: T. Jebelean, V. Negru, D. Petcu, D. Zaharie, T. Ida, S.M. Watt (eds.) 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, September 21–24, 2017, pp. 145–152. IEEE Computer Society (2017)
Jovanovic, D., Barrett, C.W.: Polite theories revisited. In: C.G. Fermüller, A. Voronkov (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 (2010). Extended technical report is available at http://theory.stanford.edu/~barrett/pubs/JB10-TR.pdf
Kovács, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: G. Castagna, A.D. Gordon (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18–20, 2017, pp. 260–270. ACM (2017)
Krstic, S., Conchon, S.: Canonization for disjoint unions of theories. Inf. Comput. 199(1–2), 87–106 (2005) DOI: 10.1016/j.ic.2004.11.001
Krstic, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: O. Grumberg, M. Huth (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 (2007)
Manna, Z., Zarba, C.G.: Combining decision procedures. In: B.K. Aichernig, T.S.E. Maibaum (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18–20, 2002, Revised Papers, Lecture Notes in Computer Science, vol. 2757, pp. 381–422. Springer (2002)
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: B. Gramlich (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 (2005). Extended technical report is available at https://hal.inria.fr/inria-00070335/
Reynolds, A., Blanchette, J.C.: A decision procedure for (co)datatypes in SMT solvers. J. Autom. Reason. 58(3), 341–362 (2017) DOI: 10.1007/s10817-016-9372-6
Reynolds, A., Viswanathan, A., Barbosa, H., Tinelli, C., Barrett, C.W.: Datatypes with shared selectors. In: D. Galmiche, S. Schulz, R. Sebastiani (eds.) Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Lecture Notes in Computer Science, vol. 10900, pp. 591–608. Springer (2018)
Sheng, Y., Zohar, Y., Ringeissen, C., Lange, J., Fontaine, P., Barrett, C.W.: Politeness for the theory of algebraic datatypes. In: IJCAR (1), Lecture Notes in Computer Science, vol. 12166, pp. 238–255. Springer (2020)
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 (2021)
Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. J. ACM 26(2), 351–360 (1979) DOI: 10.1145/322123.322137
Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: R.A. Schmidt (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2–7, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5663, pp. 67–83. Springer (2009)
Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. J. Autom. Reason. 30(1), 1–31 (2003) DOI: 10.1023/A:1022587501759
Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: J.J. Alferes, J.A. Leite (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 (2004)
