Evaluate an AIG list and interpret the resulting bits as an unsigned integer, as in gl::bfr-list->u.
(aig-list->u x env) → ans
Function:
(defun aig-list->u (x env) (declare (xargs :guard (true-listp x))) (let ((__function__ 'aig-list->u)) (declare (ignorable __function__)) (if (atom x) 0 (logcons (bool->bit (aig-eval (car x) env)) (aig-list->u (cdr x) env)))))
Theorem:
(defthm natp-of-aig-list->u (b* ((ans (aig-list->u x env))) (natp ans)) :rule-classes :type-prescription)
Theorem:
(defthm aig-list->u-of-list-fix-x (equal (aig-list->u (list-fix x) env) (aig-list->u x env)))
Theorem:
(defthm aig-list->u-list-equiv-congruence-on-x (implies (list-equiv x x-equiv) (equal (aig-list->u x env) (aig-list->u x-equiv env))) :rule-classes :congruence)