Ordering mechanism for canonicalizing symmetric operators.
(bed-order a b order) → (mv okp order)
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
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
(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))))