(vl-vardecl-enum-constraint x portdecls config) → vttree
Function:
(defun vl-vardecl-enum-constraint (x portdecls config) (declare (xargs :guard (and (vl-vardecl-p x) (vl-simpconfig-p config)))) (declare (xargs :guard (b* (((vl-vardecl x))) (and (vl-datatype-resolved-p x.type) (b* (((mv err size) (vl-datatype-size x.type))) (and (not err) size)))))) (let ((__function__ 'vl-vardecl-enum-constraint)) (declare (ignorable __function__)) (b* (((vl-simpconfig config)) ((vl-vardecl x)) (vttree nil) ((unless config.enum-constraints) vttree) ((unless (or (eq config.enum-constraints :all) (hons-get x.name portdecls))) vttree) ((mv constraint &) (vl-datatype-constraint x.type (sv::make-simple-svar x.name) 0)) (constraint (sv::svex-reduce-consts constraint))) (if (sv::svex-case constraint :quote (eql constraint.val 0) :otherwise t) (vttree-add-constraints (list (sv::make-constraint :name (cat "Enum constraint for " x.name) :cond constraint)) vttree) vttree))))
Theorem:
(defthm return-type-of-vl-vardecl-enum-constraint (b* ((vttree (vl-vardecl-enum-constraint x portdecls config))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecl-enum-constraint-of-vl-vardecl-fix-x (equal (vl-vardecl-enum-constraint (vl-vardecl-fix x) portdecls config) (vl-vardecl-enum-constraint x portdecls config)))
Theorem:
(defthm vl-vardecl-enum-constraint-vl-vardecl-equiv-congruence-on-x (implies (vl-vardecl-equiv x x-equiv) (equal (vl-vardecl-enum-constraint x portdecls config) (vl-vardecl-enum-constraint x-equiv portdecls config))) :rule-classes :congruence)
Theorem:
(defthm vl-vardecl-enum-constraint-of-vl-simpconfig-fix-config (equal (vl-vardecl-enum-constraint x portdecls (vl-simpconfig-fix config)) (vl-vardecl-enum-constraint x portdecls config)))
Theorem:
(defthm vl-vardecl-enum-constraint-vl-simpconfig-equiv-congruence-on-config (implies (vl-simpconfig-equiv config config-equiv) (equal (vl-vardecl-enum-constraint x portdecls config) (vl-vardecl-enum-constraint x portdecls config-equiv))) :rule-classes :congruence)