		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-+-ss

Signature
(sv::aig-+-ss c v1 v2) → sum
Arguments: v1 — Guard (true-listp v1).; v2 — Guard (true-listp v2).
Returns: sum — Type (true-listp sum).

Definitions and Theorems

Function: aig-+-ss

(defun sv::aig-+-ss (c v1 v2)
  (declare (xargs :guard (and (true-listp v1) (true-listp v2))))
  (let ((__function__ 'sv::aig-+-ss))
    (declare (ignorable __function__))
    (b* (((mv head1 tail1 end1)
          (first/rest/end v1))
         ((mv head2 tail2 end2)
          (first/rest/end v2))
         (axorb (acl2::aig-xor head1 head2))
         (s (acl2::aig-xor c axorb))
         ((when (and end1 end2))
          (let ((last (acl2::aig-ite axorb (acl2::aig-not c)
                                     head1)))
            (sv::aig-scons s (sv::aig-sterm last))))
         (c (acl2::aig-or (acl2::aig-and c axorb)
                          (acl2::aig-and head1 head2)))
         (rst (sv::aig-+-ss c tail1 tail2)))
      (sv::aig-scons s rst))))

Theorem: true-listp-of-aig-+-ss

(defthm sv::true-listp-of-aig-+-ss
  (b* ((sum (sv::aig-+-ss c v1 v2)))
    (true-listp sum))
  :rule-classes :type-prescription)

Theorem: aig-+-ss-correct

(defthm sv::aig-+-ss-correct
  (b* ((sum (sv::aig-+-ss c v1 v2)))
    (and (equal (sv::aig-list->s sum env)
                (+ (bool->bit (acl2::aig-eval c env))
                   (sv::aig-list->s v1 env)
                   (sv::aig-list->s v2 env))))))