		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Bed-order

Ordering mechanism for canonicalizing symmetric operators.

Signature
(bed-order a b order) → (mv okp order)
Arguments: a — The first node to consider.; b — The second node to consider.; order — Table mapping nodes to ranks.
Returns: okp — Is a <= b per this order?.; order — Possibly updated order table.

One of the main drawbacks of using a Hons-based representation is that there isn't a convenient way to ask whether one node comes "earlier" than another. In a DAG-based representation you could just compare the indices of the nodes. But our DAG, being extralogical, is inaccessible and can't be used in this heuristic way.

Well, we still want to be able to reorder the children of, e.g., AND nodes, since keeping things in a particular order will encourage structure sharing and help us to notice opportunities for additional reductions such as A & A --> A. So, we impose an order on the nodes using an explicit table.

We want to keep the reasoning impact of this table to a minimum. Accordingly, we don't require any guards on it. The general idea is that the order table maps nodes to numbers. These numbers are assigned in an arbitrary way as we happen to encounter nodes. That is, if a or b hasn't yet been assigned an index, we will go ahead and assign it one here.

The nature of hons-acons means that the car of order will be the most recently assigned node. So, it's easy to assign sequential indices without having to maintain some separate free counter.

Definitions and Theorems

Function: bed-order

(defun bed-order (a b order)
  (declare (xargs :guard t))
  (let ((__function__ 'bed-order))
    (declare (ignorable __function__))
    (b* (((when (or (atom a) (atom b)))
          (cond ((and (atom a) (atom b))
                 (mv (or a (not b)) order))
                ((atom a) (mv t order))
                (t (mv nil order))))
         (alook (hons-get a order))
         (blook (hons-get b order))
         ((when (and alook blook))
          (mv (<= (ifix (cdr alook))
                  (ifix (cdr blook)))
              order))
         (free (ifix (and (consp order)
                          (consp (car order))
                          (cdar order))))
         ((mv aidx order free)
          (b* (((when alook)
                (mv (ifix (cdr alook)) order free))
               (free (+ 1 free))
               (order (hons-acons a free order)))
            (mv free order free)))
         ((mv bidx order)
          (b* (((when blook)
                (mv (ifix (cdr blook)) order))
               (free (+ 1 free))
               (order (hons-acons b free order)))
            (mv free order))))
      (mv (<= aidx bidx) order))))