×

Equality detection for linear arithmetic constraints. (English) Zbl 1237.91075

Summary: Satisfiability modulo theories (SMT) play a key role in verification applications. A crucial SMT problem is to combine separate theory solvers for the union of theories. In previous work, the simplex method is used to determine the solvability of constraint systems and the equalities implied by constraint systems are detected by a multitude of applications of the dual simplex method. We present an effective simplex tableau-based method to identify all implicit equalities such that the simplex method is harnessed to an irreducible minimum. Experimental results show that the method is feasible and effective.

MSC:

91B06 Decision theory
90C05 Linear programming
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Barrett, C., Berezin, S., 2004. CVC Lite: a new implementation of the cooperating validity checker. LNCS, 3114:515-518. · Zbl 1103.68605
[2] Barrett, C., Dill, D., Levitt, J., 1996. Validity checking for combinations of theories with equality. LNCS, 1166:187-201. [doi:10.1007/BFb0031808]
[3] Barrett, C., de Moura, L., Stump, A., 2005. SMT-COMP: satisfiability modulo theories competition. LNCS, 3576: 20-23. [doi:10.1007/11513988_4] · Zbl 1081.68607
[4] Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Rossum, P.V., Schulz, S., Sebastiani, R., 2005. The MathSAT 3 System. LNCS, 3632:315-321. [doi:10.1007/11532231_23] · Zbl 1087.68630
[5] Chvatal, V., 1983. Linear Programming. Springer-Verlag New York, LLC, p.34-45. · Zbl 0537.90067
[6] Dantzig, G.B., 1973. Fourier-Motzkin elimination and its dual. J. Comb. Theory Ser. A, 14(3):288-297. [doi:10.1016/0097-3165(73)90004-6] · Zbl 0258.15010 · doi:10.1016/0097-3165(73)90004-6
[7] Detlefs, D., Nelson, G., Saxe, J.B., 2005. Simplify: a theorem prover for program checking. J. ACM, 52(3):365-473. [doi:10.1145/1066100.1066102] · Zbl 1323.68462 · doi:10.1145/1066100.1066102
[8] Dutertre, B., de Moura, L., 2006. A fast linear-arithmetic solver for DPLL(T). LNCS, 4144:81-94. [doi:10.1007/11817963_11]
[9] Filliatre, J.C., Owre, S., Rueb, H., Shankar, N., 2001. ICS: Integrated Canonization and Solving. Int. Conf. on Computer Aided Verification, p.246-249.
[10] Kroening, D., Strichman, O., 2008. Decision Procedures: An Algorithmic Point of View. Springer-Verlag New York Inc., p.113-122. · Zbl 1149.68071
[11] Lassez, J.L., McAloon, K., 1992. A canonical form for generalized linear constraints. J. Symb. Comput., 13(1):1-24. [doi:10.1016/0747-7171(92)90002-L] · Zbl 0745.90046 · doi:10.1016/0747-7171(92)90002-L
[12] McMillan, K.L., 2004. An Interpolating Theorem Prover. TACAS 2004: Tools and Algorithms for Construction and Analysis of Systems, p.102-121. · Zbl 1079.68092
[13] Nelson, G., Techniques for Program Verification (1981), Palo Alto, CA
[14] Nieuwenhuis, R., Oliveras, A., 2005. DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. Int. Conf. on Computer Aided Verification, p.321-324. · Zbl 1081.68629
[15] Refalo, P., 1998. Approaches to the Incremental Detection of Implicit Equalities with the Revised Simplex Method. Proc. 10th Int. Symp. on Principles of Declarative Programming, p.481-496. [doi:10.1007/BFb0056634]
[16] Rueß, H.; Shankar, N., Solving Linear Arithmetic Constraints (2004), Menlo Park, CA, USA
[17] Sheini, H.M., Sakallah, K.A., 2005. A scalable method for solving satisfiability of integer linear arithmetic logic. LNCS, 3569:241-256. [doi:10.1007/11499107_18] · Zbl 1128.68483
[18] Stuckey, P.J., 1991. Incremental linear constraint solving and detection of implicit equalities. ORSA J. Comput., 3(4): 269-271. · Zbl 0755.90058 · doi:10.1287/ijoc.3.4.269
[19] Stump, A., Barrett, C.W., Dill, D.L., 2002. CVC: a cooperating validity checker. LNCS, 2404:500-504. [doi:10.1007/3-540-45657-0_40] · Zbl 1010.68720
[20] Vanderbei, R.J., 2001. Linear Programming: Foundations and Extensions (2nd Ed.). Springer-Verlag New York, LLC, p.16-22. · Zbl 1043.90002 · doi:10.1007/978-1-4757-5662-3
[21] Wang, C., Ivancic, F., Ganai, M., Gupta, A., 2005. Deciding separation logic formulae by SAT and incremental negative cycle elimination. LNCS, 3835:322-336. [doi:10.1007/11591191_23] · Zbl 1143.68583
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.