(vl-gateinstlist-remove-toohard x warnings) → (mv warnings new-x)
Function:
(defun vl-gateinstlist-remove-toohard (x warnings) (declare (xargs :guard (and (vl-gateinstlist-p x) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-gateinstlist-remove-toohard)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (ok) nil)) ((mv warnings cdr-prime) (vl-gateinstlist-remove-toohard (cdr x) warnings)) (x1 (vl-gateinst-fix (car x))) (car-exprs (vl-gateinst-allexprs x1)) (car-hard (vl-exprlist-toohard-subexpr car-exprs)) ((when car-hard) (mv (fatal :type :vl-dropped-gateinst :msg "Deleting ~a0 because it has unsupported ~ subexpression ~a1. This deletion may cause our ~ analysis to be flawed." :args (list x1 car-hard)) cdr-prime)) (x-prime (cons x1 cdr-prime))) (mv warnings x-prime))))
Theorem:
(defthm vl-warninglist-p-of-vl-gateinstlist-remove-toohard.warnings (b* (((mv ?warnings ?new-x) (vl-gateinstlist-remove-toohard x warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-p-of-vl-gateinstlist-remove-toohard.new-x (b* (((mv ?warnings ?new-x) (vl-gateinstlist-remove-toohard x warnings))) (vl-gateinstlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-remove-toohard-of-vl-gateinstlist-fix-x (equal (vl-gateinstlist-remove-toohard (vl-gateinstlist-fix x) warnings) (vl-gateinstlist-remove-toohard x warnings)))
Theorem:
(defthm vl-gateinstlist-remove-toohard-vl-gateinstlist-equiv-congruence-on-x (implies (vl-gateinstlist-equiv x x-equiv) (equal (vl-gateinstlist-remove-toohard x warnings) (vl-gateinstlist-remove-toohard x-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-gateinstlist-remove-toohard-of-vl-warninglist-fix-warnings (equal (vl-gateinstlist-remove-toohard x (vl-warninglist-fix warnings)) (vl-gateinstlist-remove-toohard x warnings)))
Theorem:
(defthm vl-gateinstlist-remove-toohard-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-gateinstlist-remove-toohard x warnings) (vl-gateinstlist-remove-toohard x warnings-equiv))) :rule-classes :congruence)