(vl-enumvalues->constraint subexp values) → constraint
Function:
(defun vl-enumvalues->constraint (subexp values) (declare (xargs :guard (and (sv::svex-p subexp) (vl-exprlist-p values)))) (let ((__function__ 'vl-enumvalues->constraint)) (declare (ignorable __function__)) (if (atom values) 0 (b* (((unless (vl-expr-case (car values) :vl-literal)) (vl-enumvalues->constraint subexp (cdr values))) ((mv ?err svval) (vl-value-to-svex (vl-literal->val (car values))))) (sv::svcall sv::bitor (sv::svcall sv::== subexp svval) (vl-enumvalues->constraint subexp (cdr values)))))))
Theorem:
(defthm svex-p-of-vl-enumvalues->constraint (b* ((constraint (vl-enumvalues->constraint subexp values))) (sv::svex-p constraint)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-enumvalues->constraint (b* ((?constraint (vl-enumvalues->constraint subexp values))) (implies (not (member v (sv::svex-vars subexp))) (not (member v (sv::svex-vars constraint))))))
Theorem:
(defthm vl-enumvalues->constraint-of-svex-fix-subexp (equal (vl-enumvalues->constraint (sv::svex-fix subexp) values) (vl-enumvalues->constraint subexp values)))
Theorem:
(defthm vl-enumvalues->constraint-svex-equiv-congruence-on-subexp (implies (sv::svex-equiv subexp subexp-equiv) (equal (vl-enumvalues->constraint subexp values) (vl-enumvalues->constraint subexp-equiv values))) :rule-classes :congruence)
Theorem:
(defthm vl-enumvalues->constraint-of-vl-exprlist-fix-values (equal (vl-enumvalues->constraint subexp (vl-exprlist-fix values)) (vl-enumvalues->constraint subexp values)))
Theorem:
(defthm vl-enumvalues->constraint-vl-exprlist-equiv-congruence-on-values (implies (vl-exprlist-equiv values values-equiv) (equal (vl-enumvalues->constraint subexp values) (vl-enumvalues->constraint subexp values-equiv))) :rule-classes :congruence)