		Search-engine friendly clone of the ACL2 documentation.

Keep-insts-with-feat

Keep all instructions from inst-lst that have ANY feature present in feat

Signature
(keep-insts-with-feat inst-lst feat) → new-inst-lst
Arguments: inst-lst — Guard (inst-list-p inst-lst).; feat — Guard (acl2::keyword-listp feat).
Returns: new-inst-lst — Type (inst-list-p new-inst-lst), given (inst-list-p inst-lst).

Definitions and Theorems

Function: keep-insts-with-feat

(defun keep-insts-with-feat (inst-lst feat)
  (declare (xargs :guard (and (inst-list-p inst-lst)
                              (acl2::keyword-listp feat))))
  (let ((__function__ 'keep-insts-with-feat))
    (declare (ignorable __function__))
    (if (endp inst-lst)
        nil
      (b* ((inst (car inst-lst))
           (rest (keep-insts-with-feat (cdr inst-lst)
                                       feat))
           ((inst inst))
           (opcode inst.opcode)
           ((opcode opcode))
           ((when (any-present-in feat opcode.feat))
            (cons inst rest)))
        rest))))

Theorem: inst-list-p-of-keep-insts-with-feat

(defthm inst-list-p-of-keep-insts-with-feat
  (implies (inst-list-p inst-lst)
           (b* ((new-inst-lst (keep-insts-with-feat inst-lst feat)))
             (inst-list-p new-inst-lst)))
  :rule-classes :rewrite)