  Compiling programs to an instruction set architecture (ISA) requires a set of
rewrite rules that map patterns consisting of compiler instructions to patterns
consisting of ISA instructions. We synthesize such rules by constructing SMT
queries, whose solutions represent two functionally equivalent programs. These
two programs are interpreted as an instruction selection rewrite rule. Existing
work is limited to single-instruction ISA patterns, whereas our solution does
not have that restriction. Furthermore, we address inefficiencies of existing
work by developing two optimized algorithms. The first only generates unique
rules by preventing synthesis of duplicate and composite rules. The second only
generates lowest-cost rules by preventing synthesis of higher-cost rules. We
evaluate our algorithms on multiple ISAs. Without our optimizations, the vast
majority of synthesized rewrite rules are either duplicates, composites, or
higher cost. Our optimizations result in synthesis speed-ups of up to 768x and
4004x for the two algorithms.
