(vl-expr-simp-qmark x args) → new-x
Function:
(defun vl-expr-simp-qmark (x args) (declare (xargs :guard (and (vl-expr-p x) (vl-exprlist-p args)))) (declare (xargs :guard (and (not (vl-atom-p x)) (equal (vl-nonatom->op x) :vl-qmark) (equal (len args) 3)))) (let ((__function__ 'vl-expr-simp-qmark)) (declare (ignorable __function__)) (b* (((list a b c) args) ((when (and (not (vl-atom-p a)) (eq (vl-nonatom->op a) :vl-unary-bitnot))) (b* (((list ~a b c) args) (a (first (vl-nonatom->args ~a))) (ans (change-vl-nonatom x :args (list a c b)))) (vl-cw-ps-seq (vl-cw "QM~ Rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (vl-expr-resolved-p a) (eql (vl-resolved->val a) 1) (equal (vl-expr->finalwidth x) (vl-expr->finalwidth b)) (equal (vl-expr->finaltype x) (vl-expr->finaltype b)))) (b* ((ans (vl-expr-fix b))) (vl-cw-ps-seq (vl-cw "QM1 rewrite ~a0 to ~a1~%" x ans)) ans)) ((when (and (vl-expr-resolved-p a) (eql (vl-resolved->val a) 0) (equal (vl-expr->finalwidth x) (vl-expr->finalwidth c)) (equal (vl-expr->finaltype x) (vl-expr->finaltype c)))) (b* ((ans (vl-expr-fix c))) (vl-cw-ps-seq (vl-cw "QM0 rewrite ~a0 to ~a1~%" x ans)) ans))) (change-vl-nonatom x :args args))))
Theorem:
(defthm vl-expr-p-of-vl-expr-simp-qmark (b* ((new-x (vl-expr-simp-qmark x args))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-simp-qmark-of-vl-expr-fix-x (equal (vl-expr-simp-qmark (vl-expr-fix x) args) (vl-expr-simp-qmark x args)))
Theorem:
(defthm vl-expr-simp-qmark-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-simp-qmark x args) (vl-expr-simp-qmark x-equiv args))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-simp-qmark-of-vl-exprlist-fix-args (equal (vl-expr-simp-qmark x (vl-exprlist-fix args)) (vl-expr-simp-qmark x args)))
Theorem:
(defthm vl-expr-simp-qmark-vl-exprlist-equiv-congruence-on-args (implies (vl-exprlist-equiv args args-equiv) (equal (vl-expr-simp-qmark x args) (vl-expr-simp-qmark x args-equiv))) :rule-classes :congruence)