| Computer Science and Technology |
|
|
|
|
| Equality detection for linear arithmetic constraints |
| Li LI, Kai-duo HE, Ming GU, Xiao-yu SONG |
| Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China; School of Software, Tsinghua University, Beijing 100084, China; MOE Key Laboratory for Information System Security, Beijing 100084, China; Department of Electrical and Computer Engineering, Portland State University, Oregon 97207, USA |
|
|
|
Abstract 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.
|
|
Received: 12 November 2008
Published: 21 October 2009
|
|
|
|
Viewed |
|
|
|
Full text
|
|
|
|
|
Abstract
|
|
|
|
|
Cited |
|
|
|
|
| |
Shared |
|
|
|
|
| |
Discussed |
|
|
|
|
