Abstract
We apply an extension of the Nelson-Oppen combination method to develop a decision procedure for the non-disjoint union of theories modeling data structures with a counting operator and fragments of arithmetic. We present some data structures and some fragments of arithmetic for which the combination method is complete and effective. To achieve effectiveness, the combination method relies on particular procedures to compute sets that are representative of all the consequences over the shared theory. We show how to compute these sets by using a superposition calculus for the theories of the considered data structures and various solving and reduction techniques for the fragments of arithmetic we are interested in, including Gauss elimination, Fourier-Motzkin elimination and Groebner bases computation.
This work is partly funded by the ANR project “DeCert”.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armando, A., Bonacina, M.-P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. on Computational Logic 10(1) (2009)
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation 183(2), 140–164 (2003)
Bonacina, M.P., Echenim, M.: On variable-inactivity and polynomial T-satisfiability procedures. Journal of Logic and Computation 18(1), 77–96 (2008)
Buchberger, B.: A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bull. 10(3), 19–29 (1976)
de Moura, L.M., Bjørner, N.: Engineering DPLL(T) + Saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 475–490. Springer, Heidelberg (2008)
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York-London (1972)
Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning 33(3-4), 221–249 (2004)
Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Transactions on Computational Logic 9(2), 1–54 (2008)
Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On superposition-based satisfiability procedures and their combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 594–608. Springer, Heidelberg (2005)
Lassez, J.-L., Maher, M.J.: On Fourier’s algorithm for linear arithmetic constraints. Journal of Automated Reasoning 9(3), 373–379 (1992)
Lassez, J.-L., McAloon, K.: A canonical form for generalized linear constraints. Journal of Symbolic Computation 13(1), 1–24 (1992)
Lynch, C., Tran, D.-K.: Automatic decidability and combinability revisited. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, pp. 328–344. Springer, Heidelberg (2007)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transaction on Programming Languages and Systems 1(2), 245–257 (1979)
Nicolini, E.: Combined decision procedures for constraint satisfiability. PhD thesis. Università degli Studi di Milano (2007)
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Combinable extensions of abelian groups. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 51–66. Springer, Heidelberg (2009)
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Data structures with arithmetic constraints: a non-disjoint combination. Report, INRIA, RR-6963 (2009)
Nicolini, E., Ringeissen, C., Rusinowitch, M.: Satisfiability procedures for combination of theories sharing integer offsets. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 428–442. Springer, Heidelberg (2009)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 7, vol. I, pp. 371–443. Elsevier Science, Amsterdam (2001)
Shostak, R.E.: Deciding combinations of theories. J. of the ACM 31, 1–12 (1984)
Zucchelli, D.: Combination methods for software verification. PhD thesis, Università degli Studi di Milano and Université Henri Poincaré - Nancy 1 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nicolini, E., Ringeissen, C., Rusinowitch, M. (2009). Data Structures with Arithmetic Constraints: A Non-disjoint Combination. In: Ghilardi, S., Sebastiani, R. (eds) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science(), vol 5749. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04222-5_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-04222-5_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04221-8
Online ISBN: 978-3-642-04222-5
eBook Packages: Computer ScienceComputer Science (R0)