Report Number: CS-TR-78-652
Institution: Stanford University, Department of Computer Science
Title: Simplification by cooperating decision procedures
Author: Nelson, Charles Gregory
Author: Oppen, Derek C.
Date: April 1978
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, equality, the
conditional function cond (denoting if-then-else), the
numerals, the arithmetic functions and predicates +, - and
$\leq$, 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 reals, the set of arrays, LISP list structure and the
booleans true and false.
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 reals, arrays and list
structure under the above functions and predicates.
The organization of the simplifier is based on a method for
combining decision procedures for several theories into a
single decision procedure for a theory combining 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
predicate and function symbols are in S. We give a general
procedure for combining satisfiability programs for sets S
and T into a single satisfiability program for S $\cup$ T,
given certain conditions on S and T.
The simplifier described in this paper is currently used in
the Stanford Pascal Verifier.