How to ensure that FGL can reduce your conjecture to a Boolean formula

FGL is intended to reduce ACL2 conjectures to Boolean formulas that can be solved with a SAT solver. The first step in this process is to reduce the variables of the theorem -- which could represent any object at all -- into a bit-blasted representation of some sort. In GL, this was typically done by providing a shape specifier for each variable, and providing a coverage proof to show that the shape specifier was sufficient to cover all the values of the variable that satisfy the hypotheses of the theorem. In FGL, shape specifiers are not supported (yet); instead, theorem variables are just variables, but rewrite rules can be used to extract a Boolean representation from them.

When the FGL interpreter process an IF term, it interprets the test of the
IF, resulting in a symbolic object. If that symbolic object is a function call
or variable object, then we check the Boolean variable database of the
interpreter state to see whether that object has already been bound to a
Boolean variable. If not, we add a new Boolean variable representing that
object's truth value. This is the only way that Boolean variables are
generated in FGL. An example of how this can be used can be seen in the
following rule (from "fgl/bitops.lisp") for expanding the

(def-fgl-rewrite loghead-const-width (implies (syntaxp (integerp n)) (equal (loghead n x) (if (or (zp n) (and (check-int-endp x (syntax-bind xsyn (g-concrete x))) (not (intcar x)))) 0 (intcons (and (intcar x) t) (loghead (1- n) (intcdr x)))))))

Applying this rule to

So one way of getting from free variables to Boolean formulas that FGL can
use is to access them through functions like

Often instead of accessing a variable only through accessors like

(def-fgl-rewrite unsigned-byte-p-const-width (implies (syntaxp (integerp n)) (equal (unsigned-byte-p n x) (and (natp n) (equal x (loghead n x)) t))))

When we assume

Make sure the terms that are assigned Boolean variables don't alias each
other -- otherwise proofs may end up having false counterexamples. For
example, if you generate a Boolean variable for both

When taking the approach of normalizing typed variables to bit-blasted
objects, it is important that the variable's correct type be assumed at each
use of the variable. That is, the assumption should be in a top-level
hypothesis or else an

(fgl-thm (if (and (unsigned-byte-p 3 x) (unsigned-byte-p 3 y)) (equal (+ x y) (+ y x)) t))

But the following probably doesn't, or at least not by bitblasting:

(fgl-thm (if (not (equal (+ x y) (+ y x))) (not (and (unsigned-byte-p 3 x) (unsigned-byte-p 3 y))) t))