Evaluate an AIG list and interpret the resulting bits as a signed integer, as in gl::bfr-list->s.
(aig-list->s x env) → ans
Function:
(defun aig-list->s (x env) (declare (xargs :guard (true-listp x))) (let ((__function__ 'aig-list->s)) (declare (ignorable __function__)) (b* (((mv first rest end) (gl::first/rest/end x))) (if end (gl::bool->sign (aig-eval first env)) (logcons (bool->bit (aig-eval first env)) (aig-list->s rest env))))))
Theorem:
(defthm integerp-of-aig-list->s (b* ((ans (aig-list->s x env))) (integerp ans)) :rule-classes :type-prescription)
Theorem:
(defthm aig-list->s-of-list-fix-x (equal (aig-list->s (list-fix x) env) (aig-list->s x env)))
Theorem:
(defthm aig-list->s-list-equiv-congruence-on-x (implies (list-equiv x x-equiv) (equal (aig-list->s x env) (aig-list->s x-equiv env))) :rule-classes :congruence)