		Search-engine friendly clone of the ACL2 documentation.

Fgl-getting-bits-from-objects

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.

Generating Boolean variables

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 loghead of some object:

(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 (loghead 3 z) results in three new Boolean variables being generated due to the subterm (and (intcar x) t), which is really (if (intcar x) t nil). The full expression reduces to a g-integer form whose bits are the variables generated from (intcar z), (intcar (intcdr z)), and (intcar (intcdr (intcdr z))).

So one way of getting from free variables to Boolean formulas that FGL can use is to access them through functions like loghead, and to have rules like loghead-const-width that rewrite those in a way that expose the Boolean variables that we want to reason about.

Normalizing Variables to Bit-blasted Objects

Often instead of accessing a variable only through accessors like loghead, we'll have a hyp that describes the type of the variable. We can use such hyps to reduce the variables to bit-blasted objects. For example, we have the following rule in "fgl/bitops.lisp":

(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 (unsigned-byte-p 3 z), we end up with the formula (equal z (loghead 3 z)), but (loghead 3 z) gets rewritten to a symbolic integer as described above. Since this equal term is in an IF test (and (equal z ...) t), we add a Boolean variable for it. When we add a Boolean variable for an equal term, we also can add an entry in a database that maps terms to Boolean variables that equate them to other terms. Whenever the FGL interpreter produces a symbolic object that has an entry in this database, we check whether any of those Boolean variables are currently assumed to be true, and replace that symbolic object with the object it is equated to. In this case, we create an entry for z in the database mapping it to the Boolean variable representing the equal term. Since this occurred as a hypothesis in the theorem, we're going to be assuming that to be true in the conclusion, so whenever we see the variable z there we'll then replace it with the symbolic integer generated from the loghead.

Pitfalls and Suggestions

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 (intcar (intcdr x)) and (logbitp 1 x), then you're likely to have false counterexamples where these two variables are assigned opposite values. Choose a single normal form and rewrite other accessors to that -- e.g., use a rule like logbitp-const-index to ensure that logbitp calls are normalized correctly to (intcar (intcdr ...)) form.

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 if test guarding each use of the variable (aside from the type assumption itself). For example, the following probably works (depending what rules are installed):

(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))