(vl-casestmt-violation-conds x size test ss scopes config) → (mv vttree constraint wrapper-xcond full-conservative part-conservative)
Function:
(defun vl-casestmt-violation-conds (x size test ss scopes config) (declare (xargs :guard (and (vl-stmt-p x) (natp size) (sv::svex-p test) (vl-scopestack-p ss) (vl-elabscopes-p scopes) (svstmt-config-p config)))) (declare (xargs :guard (vl-stmt-case x :vl-casestmt))) (let ((__function__ 'vl-casestmt-violation-conds)) (declare (ignorable __function__)) (b* (((vl-casestmt x)) ((svstmt-config config)) ((when (or (not x.check) (eq x.check :vl-priority))) (mv nil nil 0 0 0)) ((when (and (eql 0 config.uniquecase-conservative) (not config.uniquecase-constraints))) (mv nil nil 0 0 0)) ((mv vttree nonematch multimatch) (vl-caselist-none/multiple x.caselist size test x.casetype x.casekey ss scopes)) ((mv full-conservative part-conservative) (case config.uniquecase-conservative (0 (mv 0 0)) (1 (mv (if (and (eq x.check :vl-unique) (vl-stmt-case x.default :vl-nullstmt)) nonematch 0) multimatch)) (2 (mv (if (and (eq x.check :vl-unique) (vl-stmt-case x.default :vl-nullstmt)) (sv::svcall sv::bitor nonematch multimatch) multimatch) 0)) (t (mv 0 0)))) (wrapper-xcond (if (eql config.uniquecase-conservative 3) (if (and (eq x.check :vl-unique) (vl-stmt-case x.default :vl-nullstmt)) (sv::svcall sv::bitor nonematch multimatch) multimatch) 0)) (constraint (and config.uniquecase-constraints (b* ((name (cat (vl-casecheck-string x.check) " " (vl-casetype-string x.casetype) " at " (vl-location-string x.loc))) (onehot (sv::svcall sv::bitnot (sv::svcall sv::uor multimatch))) (cond (if (eq x.check :vl-unique) onehot (sv::svcall sv::bitor onehot nonematch)))) (list (sv::make-svstmt-constraints :constraints (list (sv::make-constraint :name name :cond cond)))))))) (mv vttree constraint wrapper-xcond full-conservative part-conservative))))
Theorem:
(defthm return-type-of-vl-casestmt-violation-conds.vttree (b* (((mv ?vttree ?constraint ?wrapper-xcond ?full-conservative ?part-conservative) (vl-casestmt-violation-conds x size test ss scopes config))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm svstmtlist-p-of-vl-casestmt-violation-conds.constraint (b* (((mv ?vttree ?constraint ?wrapper-xcond ?full-conservative ?part-conservative) (vl-casestmt-violation-conds x size test ss scopes config))) (sv::svstmtlist-p constraint)) :rule-classes :rewrite)
Theorem:
(defthm svex-p-of-vl-casestmt-violation-conds.wrapper-xcond (b* (((mv ?vttree ?constraint ?wrapper-xcond ?full-conservative ?part-conservative) (vl-casestmt-violation-conds x size test ss scopes config))) (sv::svex-p wrapper-xcond)) :rule-classes :rewrite)
Theorem:
(defthm svex-p-of-vl-casestmt-violation-conds.full-conservative (b* (((mv ?vttree ?constraint ?wrapper-xcond ?full-conservative ?part-conservative) (vl-casestmt-violation-conds x size test ss scopes config))) (sv::svex-p full-conservative)) :rule-classes :rewrite)
Theorem:
(defthm svex-p-of-vl-casestmt-violation-conds.part-conservative (b* (((mv ?vttree ?constraint ?wrapper-xcond ?full-conservative ?part-conservative) (vl-casestmt-violation-conds x size test ss scopes config))) (sv::svex-p part-conservative)) :rule-classes :rewrite)
Theorem:
(defthm svex-addr-p-of-vl-caselist-violation-conds (b* (((mv ?vttree ?constraint ?wrapper-xcond ?full-conservative ?part-conservative) (vl-casestmt-violation-conds x size test ss scopes config))) (implies (sv::svarlist-addr-p (sv::svex-vars test)) (and (sv::svarlist-addr-p (sv::svex-vars wrapper-xcond)) (sv::svarlist-addr-p (sv::svex-vars full-conservative)) (sv::svarlist-addr-p (sv::svex-vars part-conservative)) (sv::svarlist-addr-p (sv::svstmtlist-vars constraint))))))
Theorem:
(defthm vl-casestmt-violation-conds-of-vl-stmt-fix-x (equal (vl-casestmt-violation-conds (vl-stmt-fix x) size test ss scopes config) (vl-casestmt-violation-conds x size test ss scopes config)))
Theorem:
(defthm vl-casestmt-violation-conds-vl-stmt-equiv-congruence-on-x (implies (vl-stmt-equiv x x-equiv) (equal (vl-casestmt-violation-conds x size test ss scopes config) (vl-casestmt-violation-conds x-equiv size test ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-violation-conds-of-nfix-size (equal (vl-casestmt-violation-conds x (nfix size) test ss scopes config) (vl-casestmt-violation-conds x size test ss scopes config)))
Theorem:
(defthm vl-casestmt-violation-conds-nat-equiv-congruence-on-size (implies (acl2::nat-equiv size size-equiv) (equal (vl-casestmt-violation-conds x size test ss scopes config) (vl-casestmt-violation-conds x size-equiv test ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-violation-conds-of-svex-fix-test (equal (vl-casestmt-violation-conds x size (sv::svex-fix test) ss scopes config) (vl-casestmt-violation-conds x size test ss scopes config)))
Theorem:
(defthm vl-casestmt-violation-conds-svex-equiv-congruence-on-test (implies (sv::svex-equiv test test-equiv) (equal (vl-casestmt-violation-conds x size test ss scopes config) (vl-casestmt-violation-conds x size test-equiv ss scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-violation-conds-of-vl-scopestack-fix-ss (equal (vl-casestmt-violation-conds x size test (vl-scopestack-fix ss) scopes config) (vl-casestmt-violation-conds x size test ss scopes config)))
Theorem:
(defthm vl-casestmt-violation-conds-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-casestmt-violation-conds x size test ss scopes config) (vl-casestmt-violation-conds x size test ss-equiv scopes config))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-violation-conds-of-vl-elabscopes-fix-scopes (equal (vl-casestmt-violation-conds x size test ss (vl-elabscopes-fix scopes) config) (vl-casestmt-violation-conds x size test ss scopes config)))
Theorem:
(defthm vl-casestmt-violation-conds-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-casestmt-violation-conds x size test ss scopes config) (vl-casestmt-violation-conds x size test ss scopes-equiv config))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-violation-conds-of-svstmt-config-fix-config (equal (vl-casestmt-violation-conds x size test ss scopes (svstmt-config-fix config)) (vl-casestmt-violation-conds x size test ss scopes config)))
Theorem:
(defthm vl-casestmt-violation-conds-svstmt-config-equiv-congruence-on-config (implies (svstmt-config-equiv config config-equiv) (equal (vl-casestmt-violation-conds x size test ss scopes config) (vl-casestmt-violation-conds x size test ss scopes config-equiv))) :rule-classes :congruence)