		Search-engine friendly clone of the ACL2 documentation.

Fgl-handling-if-then-elses

Discussion of how if-then-else objects are dealt with in FGL.

Why If-Then-Elses Are A Problem

One of the most powerful and advantageous things about FGL is that it can avoid case splits in proofs by encoding the case splits into Boolean functions that are later handled by fast solvers. For example, if a function might return either 3 or 5, then instead of considering the two cases separately we can encode both cases into a symbolic integer value. But for some case splits the cases aren't so easily merged into a single symbolic value, except by directly encoding the case split. For example, if we have ((a . b) . c) in one case but (d . (e . f)) in the other case, it isn't clear how best to represent that.

Such cases can cause dilemmas and problems for FGL's symbolic interpretation. For example, suppose we have the following rewrite rules:

(foo (bar x) y) = (baz x y)
(foo (zar x) y) = (fuz x y)

But suppose that when we encounter a call of foo, we have (if c (bar 3) (zar 5)) as the first argument. What do we do? We could always split into cases for all the IFs in all the arguments of a function we're processing, but this could easily get stuck in exponential case splits. But otherwise, we might miss rewrites that the user might expect to happen. The user could fix this case by adding the following rewrite rule:

(foo (if c a b) y) = (if c (foo a y) (foo b y))

But this means the user needs to know all of the places this might happen and make a rewrite rule for each of them, and by that time it might be just as catastrophic for performance.

Disallowing If-Then-Elses

Because of the dilemma above, the default approach in FGL is to cause an error whenever we are unable to merge the two branches of an if-then-else into a single symbolic form automatically. When this happens, the FGL clause processor will produce an error saying that an if-then-else failed to merge and to look at the debug object. This behavior can be disabled as follows:

(assign :fgl-make-ites t)

It is also possible to use rewrite rules to allow if-then-else objects to be created in certain cases; we discuss how this is used to handle a couple of common cases in the next section. The FGL interpreter includes support for making ifs transparent to certain functions, so that rewrite rules for that purpose needn't proliferate. But often the best option is to encode data so that you don't need to represent it using if-then-elses; some examples of how to do that follow.

Merge Rules

FGL uses a function gl-object-basic-merge to merge certain combinations of objects: it can merge two symbolic or concrete integers into a symbolic integer, or merge two symbolic or concrete Boolean values into a symbolic Boolean. It also comes with some merging rules that allow a couple of common idioms: the use of nil as a "bottom" element for various types, and the use of symbols as enum types.

To force the creation of an if-then-else, overriding the setting of :fgl-make-ites, use the function if! instead of if in the right-hand side. For example, one of the rules that allows the use of nil as bottom follows:

(def-gl-branch-merge if-with-if-with-nil-nil
  (equal (if test (if test2 then nil) nil)
         (if! (and test test2) then nil)))

This will ensure that a :g-ite object will be created without checking whether then can be merged with nil (presumably this was already tried since (if test2 then nil) was matched in the left-hand side.

Making Functions Transparent to If-Then-Elses

The FGL interpreter can be told to distribute calls of a given function over if-then-else objects that might appear in their arguments as follows:

(enable-split-ifs foo)

This is similar to creating a rewrite rule matching an if in each argument of foo and distributing the call of foo into it, as follows:

(def-gl-rewrite foo-of-if-1
   (equal (foo (if test a1 a2) b)
          (if test
              (foo a1 b)
            (foo a2 b))))
(def-gl-rewrite foo-of-if-2
   (equal (foo a (if test b1 b2))
          (if test
              (foo a b1)
            (foo a b2))))

(Enabling if splitting for a function enables it for all the arguments; if this isn't desired, then providing rewrite rules like the ones above is a reasonable alternative.)

Generally speaking, it is likely to be advantageous to enable splitting ifs on a couple of kinds of functions:

Functions that are handled in FGL via rewrite rules wherein their arguments are other function calls, such as datatype accessors and predicates.
Primitives, especially if they always return an integer or always return a Boolean, since these then eliminate the if-then-else once their branches are merged.

Conversely, it is likely not advantageous to enable splitting ifs on functions that are handled by expanding a definition-style rule where the arguments to the function on the LHS are just variables.

Encoding Data to Avoid If-Then-Elses

Here are some general ideas for encoding data so as to avoid if-then-elses. After that, we provide some examples to give a flavor for how this works.

Think about the types of the data you'll be dealing with and how best to encode them symbolically.
Wrap any if-then-elses inside function definitions and turn off expansion of those function definitions (see below).
Set up branch merge rules to merge these functions with other data of the same type.
Set up rewrite rules to deal with accesses to those functions, likely including checks for equality.

Example 1: Enumeration Type

(Note: the built-in support for symbols as enum types makes the following example largely unnecessary, but still illustrative.)

(defun vector-kind (x)
  (cond ((equal (loghead 2 x) 0) :big)
        ((equal (logtail 2 x) 0) :little)
        (t                       :neither)))

;; Want to prove:
(fgl::fgl-thm
  :hyp (unsigned-byte-p 4 x)
  :concl
  (let* ((kind (vector-kind x)))
     (case kind
       (:big (not (logbitp 0 x)))
       (:little (and (or (logbitp 0 x) (logbitp 1 x)) (not (logbitp 2 x))))
       (:neither (or (logbitp 2 x) (logbitp 3 x))))))

;; But when we try this we get a merge error -- (@ :fgl-interp-error-debug-obj) shows
;; (14 :LITTLE :NEITHER) and (@ :fgl-interp-error-debug-stack) shows we were
;; applying the definition of VECTOR-KIND.

;; Vector-kind produces a symbol that is one of (:big :little :neither) -- an enumeration type.
;; We can encode that in a few different ways -- as a number or as a priority-encoding.
(defun vector-kind-encoding (littlep bigp)
  (cond (littlep :little)
        (bigp :big)
        (t :neither)))

;; Turn off this function's definition! Keep the if-then-else inside it hidden.
(fgl::disable-definition vector-kind-encoding)
(table fgl::fgl-fn-modes 'vector-kind-encoding
       (fgl::make-fgl-function-mode :dont-concrete-exec t))

;; Now rephrase vector-kind in terms of vector-kind-encoding:
(fgl::def-fgl-rewrite vector-kind-to-encoding2
  (equal (vector-kind x)
         (cond ((equal (loghead 2 x) 0) (vector-kind-encoding nil t))
               ((equal (logtail 2 x) 0) (vector-kind-encoding t nil))
               (t                       (vector-kind-encoding nil nil)))))

;; At minimum we need a rule for checking equality of a vector-kind-encoding.
;; Note: EQUAL will unify both ways, so no need to worry about the order of the
;; arguments!
(fgl::def-fgl-rewrite equal-of-vector-kind-encoding
  (equal (equal (vector-kind-encoding littlep bigp) x)
         (cond (littlep (equal x :little))
               (bigp    (equal x :big))
               (t       (equal x :neither)))))

;; Now the fgl-thm above will go through.

;; Often we might also need a rule for merging if-then-elses where the encoding
;; is one branch. But we can only merge if the other branch is also one of the
;; symbols in the enumeration, so we need to test for that.
(defun vector-kind-p (x)
  (or (equal x :big) (equal x :little) (equal x :neither)))

(fgl::disable-definition vector-kind-p)

(fgl::def-fgl-rewrite vector-kind-p-of-vector-kind-encoding
  (vector-kind-p (vector-kind-encoding littlep bigp)))

(fgl::def-fgl-branch-merge if-with-vector-kind-encoding
  (implies (vector-kind-p else)
           (equal (if test (vector-kind-encoding littlep bigp) else)
                  (vector-kind-encoding (if test littlep (equal else :little))
                                        (if test bigp (equal else :big))))))

;; Alternatively, we could instead turn off expansion of (vector-kind x) and
;; write rules directly on that:
:ubt! vector-kind-encoding

(fgl::disable-definition vector-kind)

(fgl::def-fgl-rewrite equal-of-vector-kind
  (equal (equal y (vector-kind x))
         (cond ((equal (loghead 2 x) 0) (equal y :big))
               ((equal (logtail 2 x) 0) (equal y :little))
               (t (equal y :neither)))))

(defun vector-kind-p (x)
  (or (equal x :big) (equal x :little) (equal x :neither)))

(fgl::disable-definition vector-kind-p)

(fgl::def-fgl-rewrite vector-kind-p-of-vector-kind
  (vector-kind-p (vector-kind x)))

(fgl::def-fgl-branch-merge if-then-else-of-vector-kind
  (implies (vector-kind-p else)
           (equal (if test (vector-kind x) else)
                  (vector-kind (if test x
                                 (case else
                                   (:big 4)
                                   (:little 2)
                                   (otherwise 6)))))))

Example 2: Member-Equal

Member-equal is often used to just test whether or not an object is a member of a list. But it returns much more information than that -- it returns the tail of the list beginning with that object. Because that extra information is inconvenient to represent in FGL, we represent it instead in a way that prevents us from needing to reason about this extra information.

;; This function is just IF, but we'll turn off its definition.
(defun fgl-hidden-if (test then else)
  (if test then else))

(fgl::disable-definition fgl-hidden-if)

;; This function represents a value that is likely to be just treated as
;; Boolean, but may not actually be T when it is non-NIL.  The TRUE input
;; determines its truth value and VAL determines its actual form when non-NIL.
;; We use this function when we think we won't need the actual value of val,
;; just its truth value.
(defun maybe-value (true val)
  (and true
       (or val t)))

(fgl::disable-definition maybe-value)

;; Under IFF, maybe-value is just its truth value.
(def-fgl-rewrite maybe-value-under-iff
  (iff (maybe-value true val)
       true))

;; To merge a maybe-value with some other object, merge with the test under an
;; IFF context and then merge the value using fgl-hidden-if.
(def-fgl-branch-merge maybe-value-merge
  (equal (if test (maybe-value true val) else)
         (maybe-value (if test true (and else t)) (fgl-hidden-if test val else))))

;; We probably shouldn't need to compare maybe-value with equal, but this might
;; succeed if we end up needing to.
(def-fgl-rewrite equal-of-maybe-value
  (equal (equal (maybe-value true val) x)
         (if true
             (if val
                 (equal x val)
               (equal x t))
           (not x))))
 
         
;; We'll represent member-equal using maybe-value.  Memberp-equal gives its
;; truth value:
(defun memberp-equal (x lst)
  (if (atom lst)
      nil
    (or (equal x (car lst))
        (memberp-equal x (cdr lst)))))

;; We introduce a version of member-equal about which we won't prove any rules,
;; so as to hide it away in the value of the maybe-value:
(defun hide-member-equal (x lst)
  (member-equal x lst))

;; Turn off both member-equal and hide-member-equal...
(fgl::disable-definition member-equal)
(fgl::disable-definition hide-member-equal)

(defthm memberp-equal-iff-member-equal
  (iff (memberp-equal x lst) (member-equal x lst)))

;; Now when we see member-equal, we'll hide its full value away using
;; hide-member-equal and expose its Boolean value (memberp-equal) through
;; maybe-value.
(def-fgl-rewrite member-equal-to-maybe-value
  (equal (member-equal x lst)
         (maybe-value (memberp-equal x lst) (hide-member-equal x lst))))

Subtopics

Enable-split-ifs: Enable if splitting for arguments of the given function in FGL rewriting.
Disable-split-ifs: Disable if splitting for arguments to the given function in FGL rewriting.