		Search-engine friendly clone of the ACL2 documentation.

Def-gl-boolean-constraint

Define a rule that recognizes constraints among GL generated Boolean variables

When using GL in a term-level style (see term-level-reasoning), GL may generate new Boolean variables from terms that appear as IF tests.

Sometimes, the terms from which these variables are generated have interdependent meanings. For example, if Boolean variable a represents (logbitp 5 x) and Boolean variable b represents (integerp x), it should be impossible for a to be true when b is false. However, by default, the Boolean variables generated this way are unconstrained. When this sort of interdependency among variables exists but is not accounted for, it can cause GL to find false-counterexamples.

Def-gl-boolean-constraint provides a mechanism to make such constraints known to GL. While symbolically executing a form, GL maintains a constraint, a Boolean formula known to always be true (under the evolving assignment of Boolean variables to terms). A constraint rule generated by def-gl-boolean-constraint is triggered when a Boolean variable is generated from an IF condition term and can cause the constraint to be updated with a new conjunct.

A Boolean constraint rule is formulated as follows:

(def-gl-boolean-constraint gl-logbitp-implies-integerp
   :bindings ((bit    (logbitp n x))
              (intp   (integerp x)))
   :body (implies bit intp)
   ;; optional arguments:
   :syntaxp ...
   :hints ...)

This generates a proof obligation:

(defthm gl-logbitp-implies-integerp
  (let ((bit    (gl-bool-fix (logbitp n x)))
        (intp   (gl-bool-fix (integerp x))))
    (implies bit intp))
 :hints ...
 :rule-classes nil)

(The optional :hints argument to def-gl-boolean-constraint provides the hints for the proof obligation.)

Once this rule is established, GL will generate constraints as follows:

When a Boolean variable a is generated from an IF condition matching (logbitp n x), GL will search for an existing generated Boolean variable b whose IF condition was (integerp x) and, if it exists, add the constraint (implies a b).
Conversely, when a Boolean variable b is generated from an IF condition matching (integerp x), GL will search for existing generated Boolean variables ai matching (logbitp n x), and for each of them, add the constraint (implies ai b).

To show that this rule works, you can verify that the following events fail prior to introducing the constraint rule above, but succeed after:

(def-gl-thm foo1
   :hyp t
   :concl (if (integerp x) t (not (logbitp n x)))
   :g-bindings nil
   :rule-classes nil)

(def-gl-thm foo2
   :hyp t
   :concl (if (logbitp n x) (integerp x) t)
   :g-bindings nil
   :rule-classes nil)