ACL2 Seminar, 5/5/2017

Speaker: Sol Swords

Title: Term-level Reasoning in Support of Bit-blasting

Abstract:

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 possible
values 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.