  GL is a verified tool for proving ACL2 theorems using Boolean methods such as
BDD reasoning and satisfiability checking. In its typical operation, GL
recursively traverses a term, computing a symbolic object representing the
value of each subterm. In older versions of GL, such a symbolic object could
use Boolean functions to compactly represent many possible values for integer
and Boolean subfields, but otherwise needed to reflect the concrete structure
of all possiblealues that its term might take. When a term has many possible
values that can't share such a representation, this can easily cause blowups
because GL must then case-split. To address this problem, we have added several
features to GL that allow it to reason about term-like symbolic objects using
various forms of rewriting. These features allow GL to be programmed with rules
much like the ACL2 rewriter, so that users may choose a better normal form for
terms for which the default, value-like representation would otherwise cause
case explosions. In this paper we describe these new features; as a motivating
example, we show how to program the rewriter to reason effectively about the
theory of records.
