BDD performance can sometimes be improved by breaking a problem into subcases. The standard example is floating-point addition, which benefits from separating the problem into cases based on the difference between the two inputs' exponents. (See for instance work by Chen and Bryant and Aagard, Jones, and Seger.)

For each exponent difference, the two mantissas are aligned differently before being added together, so a different BDD order is necessary to interleave their bits at the right offset. Without case splitting, a single BDD ordering has to be used for the whole problem; no matter what ordering we choose, the mantissas will be poorly interleaved for some exponent differences, causing severe performance problems. Separating the cases allows the appropriate order to be used for each difference.

GL provides a def-gl-param-thm command that supports this technique. This command splits the goal formula into several subgoals and attempts to prove each of them using the def-gl-thm approach, so for each subgoal there is a symbolic execution step and coverage proof. To show the subgoals suffice to prove the goal formula, it also does another def-gl-thm-style proof that establishes that any inputs satisfying the hypothesis are covered by some case.

Here is how we might split the proof for

(def-gl-param-thm fast-logcount-32-correct-alt :hyp (unsigned-byte-p 32 x) :concl (equal (fast-logcount-32 x) (logcount x)) :param-bindings `((((msb 1) (low nil)) ((x ,(g-int 32 -1 33)))) (((msb 0) (low 0)) ((x ,(g-int 0 1 33)))) (((msb 0) (low 1)) ((x ,(g-int 5 1 33)))) (((msb 0) (low 2)) ((x ,(g-int 0 2 33)))) (((msb 0) (low 3)) ((x ,(g-int 3 1 33))))) :param-hyp (and (equal msb (ash x -31)) (or (equal msb 1) (equal (logand x 3) low))) :cov-bindings `((x ,(g-int 0 1 33))))

We specify the five subgoals to consider using two new variables,

The

The

How do we know the case-split is complete? One final proof is needed to
show that whenever the hypothesis holds for some

(implies (unsigned-byte-p 32 x) (or (let ((msb 1) (low nil)) (and (equal msb (ash x -31)) (or (equal msb 1) (equal (logand x 3) low)))) (let ((msb 0) (low 0)) ...) (let ((msb 0) (low 1)) ...) (let ((msb 0) (low 2)) ...) (let ((msb 0) (low 3)) ...)))

This proof is also done in the def-gl-thm style, so we need we need
one last set of symbolic bindings, which is provided by the

Suppose we want to prove the commutativity of

(def-gl-param-thm finite-commute-of-* :hyp (and (natp a) (< a (expt 2 16)) (natp n) (< n 8)) :concl (equal (* n a) (* a n)) :param-bindings `((((lsb 0) (mid-sb 0) (high-sb 0)) ,(gl::auto-bindings (:nat a 16) (:nat n 3))) (((lsb 0) (mid-sb 0) (high-sb 1)) ,(gl::auto-bindings (:nat a 16) (:nat n 3))) (((lsb 0) (mid-sb 1) (high-sb 0)) ,(gl::auto-bindings (:nat a 16) (:nat n 3))) (((lsb 0) (mid-sb 1) (high-sb 1)) ,(gl::auto-bindings (:nat a 16) (:nat n 3))) (((lsb 1) (mid-sb 0) (high-sb 0)) ,(gl::auto-bindings (:nat a 16) (:nat n 3))) (((lsb 1) (mid-sb 0) (high-sb 1)) ,(gl::auto-bindings (:nat a 16) (:nat n 3))) (((lsb 1) (mid-sb 1) (high-sb 0)) ,(gl::auto-bindings (:nat a 16) (:nat n 3))) (((lsb 1) (mid-sb 1) (high-sb 1)) ,(gl::auto-bindings (:nat a 16) (:nat n 3)))) :param-hyp (equal n (logapp 1 lsb (logapp 1 mid-sb high-sb))) :cov-bindings (gl::auto-bindings (:nat a 16) (:nat n 3)))

The

As in the previous example, the

The syntax for specifying the variable ordering for each case-split is a bit
strange. Currently, for each