A simplifier based on efficient decision algorithms

ABSTRACT

We describe a simplifier for use in program manipulation and verification. The simplifier finds a normal form for any expression over the language consisting of individual variables, the usual boolean connectives, the conditional function cond (denoting if-then-else), the integers (numerals), the arithmetic functions and predicates +, - and ≤, the LISP constants, functions and predicates nil, car, cdr, cons and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. Individual variables range over the union of the rationals, the set of arrays, the LISP s-expressions and the booleans true and false. The constant, function and predicate symbols take their natural interpretations.The simplifier is complete; that is, it simplifies every valid formula to true. Thus it is also a decision procedure for the quantifier-free theory of rationals, arrays and s-expressions under the above functions and predicates.The organization of the simplifier is based on a method for combining decision algorithms for several theories into a single decision algorithm for a larger theory containing the original theories. More precisely, given a set S of functions and predicates over a fixed domain, a satisfiability program for S is a program which determines the satisfiability of conjunctions of literals (signed atomic formulas) whose predicates and function signs are in S. We give a general procedure for combining satisfiability programs for sets S and T into a single satisfiability program for S ∪ T, given certain conditions on S and T. We show how a satisfiability program for a set S can be used to write a complete simplifier for expressions containing functions and predicates of S as well as uninterpreted function symbols.The simplifier described in this paper is currently used in the Stanford Pascal Verifier.

REFERENCES

• 1: {Craig 1957} W. Craig, "Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory", Journal of Symbolic Logic, volume 22.
• 2: {Downey and Sethi 1976} P. Downey and R. Sethi, "Assignment Commands and Array Structures", manuscript.
• 3: {Johnson and Tarjan 1977} D. S. Johnson and R. E. Tarjan, "Finding Equivalent Expressions", manuscript.
• 4: {McCarthy 1963} J. McCarthy, "A Basis for a Mathematical Theory of Computation", in Computing Programming and Formal Systems, edited by P. Braffort and D. Hirshberg, North-Holland Amsterdam.
• 5: {Nelson 1976} C. G. Nelson, "Documentation for Z", unpublished memorandum.
• 6: {Nelson and Oppen 1977} C. G. Nelson and D. C. Oppen, "Fast Decision Algorithms based on Union and Find", Proceedings of the 18th Annual IEEE Symposium on Foundations of Computer Science, October 1977.
• 7: Derek C. Oppen, Reasoning about recursively defined data structures, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.151-157, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512776]