		Search-engine friendly clone of the ACL2 documentation.

Onehot-rewriting

4v-onehot-filter

Filter a sexpr-alist to avoid unnecessary onehot-rewriting.

Definitions and Theorems

Function: 4v-sexpr-mentions

(defun 4v-sexpr-mentions (x vars-fal)
  (declare (xargs :guard t))
  (if (atom x)
      (hons-get x vars-fal)
    (4v-sexpr-list-mentions (cdr x)
                            vars-fal)))

Function: 4v-sexpr-list-mentions

(defun 4v-sexpr-list-mentions (x vars-fal)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (or (4v-sexpr-mentions (car x) vars-fal)
        (4v-sexpr-list-mentions (cdr x)
                                vars-fal))))

Function: 4v-sexpr-mentions-memoize-condition

(defun 4v-sexpr-mentions-memoize-condition (x vars-fal)
  (declare (ignorable x vars-fal)
           (xargs :guard 't))
  (consp x))

Function: 4v-onehot-filter

(defun 4v-onehot-filter (x vars-fal keep skip)
  (declare (xargs :guard t))
  (cond ((atom x) (mv keep skip))
        ((atom (car x))
         (4v-onehot-filter (cdr x)
                           vars-fal keep skip))
        ((4v-sexpr-mentions (cdar x) vars-fal)
         (4v-onehot-filter (cdr x)
                           vars-fal (cons (car x) keep)
                           skip))
        (t (4v-onehot-filter (cdr x)
                             vars-fal keep (cons (car x) skip)))))

Theorem: 4v-onehot-filter-correct

(defthm 4v-onehot-filter-correct
  (b* (((mv keep skip)
        (4v-onehot-filter x vars-fal nil nil)))
    (implies (no-duplicatesp-equal (alist-keys x))
             (equal (hons-assoc-equal key x)
                    (or (hons-assoc-equal key keep)
                        (hons-assoc-equal key skip)))))
  :rule-classes nil)