Abstract
We present a layered bit-blasting-free algorithm for existentially quantifying variables from conjunctions of linear modular (bit-vector) equations (LMEs) and disequations (LMDs). We then extend our algorithm to work with arbitrary Boolean combinations of LMEs and LMDs using two approaches – one based on decision diagrams and the other based on SMT solving. Our experiments establish conclusively that our technique significantly outperforms alternative techniques for eliminating quantifiers from systems of LMEs and LMDs in practice.
This work was supported by a research grant from Board of Research in Nuclear Sciences, India.
Chapter PDF
Similar content being viewed by others
References
Chaki, S., Gurfinkel, A., Strichman, O.: Decision diagrams for linear arithmetic. In: FMCAD (2009)
Monniaux, D.: A quantifier elimination algorithm for linear real arithmetic. In: LPAR (2008)
Kroening, D., Strichman, O.: Decision procedures: an algorithmic point of view. Texts In Theoretical Computer Science. Springer, Heidelberg (2008)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
Pugh, W.: The Omega Test: A fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 102–114 (1992)
Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)
Jain, H., Clarke, E., Grumberg, O.: Efficient craig interpolation for linear diophantine (dis)equations and linear modular equations. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 254–267. Springer, Heidelberg (2008)
Ganesh, V., Berezin, S., Dill, D.: Deciding Presburger arithmetic by model checking and comparisons with other methods. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 171–186. Springer, Heidelberg (2002)
ITC 99 benchmarks, http://www.cad.polito.it/downloads/tools/itc99.html
SMTLib website, http://goedel.cs.uiowa.edu/smtlib/
CUDD release 2.4.2 website, vlsi.colorado.edu/~simfabio/CUDD
STP website, http://sites.google.com/site/stpfastprover/
John, A., Chakraborty, S.: A quantifier elimination algorithm for linear modular equations and disequations, Technical Report TR-11-33, CFDVS, IIT Bombay, http://www.cfdvs.iitb.ac.in/reports/reports/ajith_report.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
John, A.K., Chakraborty, S. (2011). A Quantifier Elimination Algorithm for Linear Modular Equations and Disequations. In: Gopalakrishnan, G., Qadeer, S. (eds) Computer Aided Verification. CAV 2011. Lecture Notes in Computer Science, vol 6806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22110-1_39
Download citation
DOI: https://doi.org/10.1007/978-3-642-22110-1_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22109-5
Online ISBN: 978-3-642-22110-1
eBook Packages: Computer ScienceComputer Science (R0)