Date: Tue, 4 Nov 2008 23:46:27 -0600
From: "Jared C. Davis"
Subject: [acl2-mtg] Abstract for this week's ACL2 talk

Hi,

At this week's ACL2 meeting, I'll talk about some improvements that
Sol Swords and I made to the UBDD library over the summer.

UBDDs are a canonical way to represent Boolean functions introduced by
Warren Hunt and Bob Boyer.  The core UBDD operations only take up a
couple of pages to define, but when memoized they produce a fairly
efficient BDD package.  Today, UBDDs are used extensively at Centaur:
they are an integral part of the "G" system (both the current version
and Sol's "GL" revision); they are also a fundamental part of the
hardware description language, E, which our analysis is based on.

A good part of the talk will have little to do with UBDDs, but instead
will be about the supporting utilities that we have come up with.
These include:

  (1) a better alternative to deftheory,
  (2) an automatic tool for introducing "flag" functions for mutual-recursion,
  (3) a generalization clause-processor which can be useful for
computed hints, and
  (4) an optimization called "opportunistic laziness" which may be
useful in improving the efficiency of your functions

All of these are lightly used in our new version of the UBDD library,
and they are all publically available via the acl2-books repository.

The remainder of the talk will be about some new approaches we have
developed for reasoning about UBDDs.  These techniques center around
the isomorphism between a Boolean function and the set of vectors
which satisfy it.  That is, we can transform the question of whether
``f = g'' into ``f(v) = g(v) for an arbitrary v.''  This allows us to
avoid dealing with the peculiar structure of UBDDs, and instead reason
about them abstractly.

We have developed some elaborate techniques (computed hints, clause
processors, or hints, etc.) that allow us to effectively,
automatically use this approach. As a result, we have been able to
eliminate many lemmas and hints from some previously-accomplished UBDD
proofs.  Also, Sol is now using our most advanced approach in his GL
work, and it is successfully proving hundreds (thousands?) of subgoals
automatically.

Jared