Abstract
The Nelson-Oppen combination method is ubiquitous in Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to particular non-disjoint unions of theories connected via bridging functions. The motivation is, e.g., to solve verification problems expressed in a combination of data structures connected to arithmetic with bridging functions such as the length of lists and the size of trees. We present a sound and complete combination procedure à la Nelson-Oppen for the theory of absolutely free data structures, including lists and trees. This combination procedure is then refined for standard interpretations. The resulting theory has a nice politeness property, enabling combinations with arbitrary decidable theories of elements.
This work has been partially supported by the project ANR-13-IS02-0001 of the Agence Nationale de la Recherche, by the European Union Seventh Framework Programme under grant agreement no. 295261 (MEALS), and by the STIC AmSud MISMT.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4 (2009)
Baader, F., Ghilardi, S.: Connecting many-sorted theories. J. Symb. Log. 72(2), 535–583 (2007)
Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 39–57. Springer, Heidelberg (2013)
Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 122–136. Springer, Heidelberg (2014). http://hal.inria.fr/hal-00985135
Chocron, P., Fontaine, P., Ringeissen, C.: A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited (Extended Version) (2015). http://hal.inria.fr
Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 51–66. Springer, Heidelberg (2005)
Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. J. Autom. Reasoning 33(3–4), 221–249 (2004)
Jovanović, D., Barrett, C.: Polite theories revisited. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 402–416. Springer, Heidelberg (2010)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245–257 (1979)
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable extensions of abelian groups. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 51–66. Springer, Heidelberg (2009)
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combining satisfiability procedures for unions of theories with a shared counting operator. Fundam. Inf. 105(1–2), 163–187 (2010)
Pham, T.-H., Whalen, M.W.: An improved unrolling-based decision procedure for algebraic data types. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 129–148. Springer, Heidelberg (2014)
Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 48–64. Springer, Heidelberg (2005)
Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 67–83. Springer, Heidelberg (2009)
Suter, P., Dotta, M., Kuncak, V.: Decision procedures for algebraic data types with abstractions. In: Hermenegildo, M.V., Palsberg, J. (eds.) Principles of Programming Languages (POPL), pp. 199–210. ACM, New York (2010)
Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011)
Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems (FroCoS), Applied Logic, pp. 103–120. Kluwer Academic Publishers (1996)
Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoret. Comput. Sci. 290(1), 291–353 (2003)
Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 366–382. Springer, Heidelberg (2009)
Zarba, C.G.: Combining lists with integers. In: International Joint Conference on Automated Reasoning (Short Papers), Technical report DII 11/01, pp. 170–179. University of Siena (2001)
Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 363–376. Springer, Heidelberg (2002)
Zarba, C.G.: Combining sets with cardinals. J. Autom. Reasoning 34(1), 1–29 (2005)
Zhang, T., Sipma, H.B., Manna, Z.: Decision procedures for term algebras with integer constraints. Inf. Comput. 204(10), 1526–1574 (2006)
Acknowledgments
We are grateful to Jasmin Blanchette and to the anonymous reviewers for many constructive remarks.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Chocron, P., Fontaine, P., Ringeissen, C. (2015). A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_29
Download citation
DOI: https://doi.org/10.1007/978-3-319-21401-6_29
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21400-9
Online ISBN: 978-3-319-21401-6
eBook Packages: Computer ScienceComputer Science (R0)