Reduction procedures reduce the satisfiability of a formula over a
complex theory to the satisfiability of a formula over a simpler
theory.

In the first part of this talk, we present a reduction procedure that
allows us to reduce the theory of sets to the theory of equality.  As
an added bonus, the procedure allows us to compute interpolants for
the theory of sets.

In the second part of the talk, we present a method for combining
reduction procedures.  As an application, we obtain a decision
procedure for a theory combining equality with uninterpreted function
symbols, fixed-sized bit-vectors, integer linear arithmetic, lists,
arrays, sets, and multisets.  The decision procedure has been
implemented in the SMT solver Caissa.