		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-abs-s

Signature
(sv::aig-abs-s x) → xabs
Arguments: x — Guard (true-listp x).
Returns: xabs — Type (true-listp xabs).

Definitions and Theorems

Function: aig-abs-s

(defun sv::aig-abs-s (x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'sv::aig-abs-s))
    (declare (ignorable __function__))
    (let ((sign (sv::aig-sign-s x)))
      (sv::aig-loghead-ns
           (integer-length-bound-s x)
           (sv::aig-+-ss sign nil
                         (sv::aig-logxor-ss (sv::aig-sterm sign)
                                            x))))))

Theorem: true-listp-of-aig-abs-s

(defthm sv::true-listp-of-aig-abs-s
  (b* ((xabs (sv::aig-abs-s x)))
    (true-listp xabs))
  :rule-classes :type-prescription)

Theorem: aig-abs-s-correct

(defthm sv::aig-abs-s-correct
  (b* ((xabs (sv::aig-abs-s x)))
    (and (equal (sv::aig-list->s xabs env)
                (abs (sv::aig-list->s x env))))))