		Search-engine friendly clone of the ACL2 documentation.

Observability-fix

Aignet-build-wide-and

Signature
(aignet-build-wide-and lits gatesimp strash aignet) → (mv and-lit new-strash new-aignet)
Arguments: lits — Guard (lit-listp lits).; gatesimp — Guard (gatesimp-p gatesimp).
Returns: and-lit — Type (litp and-lit).

Definitions and Theorems

Function: aignet-build-wide-and

(defun aignet-build-wide-and (lits gatesimp strash aignet)
  (declare (xargs :stobjs (strash aignet)))
  (declare (xargs :guard (and (lit-listp lits)
                              (gatesimp-p gatesimp))))
  (declare (xargs :guard (aignet-lit-listp lits aignet)))
  (let ((__function__ 'aignet-build-wide-and))
    (declare (ignorable __function__))
    (b* (((when (atom lits))
          (b* ((aignet (aignet-fix aignet)))
            (mv 1 strash aignet)))
         ((mv rest strash aignet)
          (aignet-build-wide-and (cdr lits)
                                 gatesimp strash aignet)))
      (aignet-hash-and (car lits)
                       rest gatesimp strash aignet))))

Theorem: litp-of-aignet-build-wide-and.and-lit

(defthm litp-of-aignet-build-wide-and.and-lit
  (b* (((mv ?and-lit ?new-strash ?new-aignet)
        (aignet-build-wide-and lits gatesimp strash aignet)))
    (litp and-lit))
  :rule-classes :rewrite)

Theorem: aignet-extension-p-of-aignet-build-wide-and

(defthm aignet-extension-p-of-aignet-build-wide-and
  (b* (((mv ?and-lit ?new-strash ?new-aignet)
        (aignet-build-wide-and lits gatesimp strash aignet)))
    (aignet-extension-p new-aignet aignet)))

Theorem: aignet-litp-of-aignet-build-wide-and

(defthm aignet-litp-of-aignet-build-wide-and
  (b* (((mv ?and-lit ?new-strash ?new-aignet)
        (aignet-build-wide-and lits gatesimp strash aignet)))
    (implies (aignet-lit-listp lits aignet)
             (aignet-litp and-lit new-aignet))))

Theorem: lit-eval-of-aignet-build-wide-and

(defthm lit-eval-of-aignet-build-wide-and
 (b* (((mv ?and-lit ?new-strash ?new-aignet)
       (aignet-build-wide-and lits gatesimp strash aignet)))
  (implies
     (aignet-lit-listp lits aignet)
     (equal (lit-eval and-lit invals regvals new-aignet)
            (aignet-eval-conjunction lits invals regvals aignet)))))

Theorem: stype-counts-of-aignet-build-wide-and

(defthm stype-counts-of-aignet-build-wide-and
  (b* (((mv ?and-lit ?new-strash ?new-aignet)
        (aignet-build-wide-and lits gatesimp strash aignet)))
    (implies (and (not (equal (stype-fix stype) (and-stype)))
                  (not (equal (stype-fix stype) (xor-stype))))
             (equal (stype-count stype new-aignet)
                    (stype-count stype aignet)))))

Theorem: aignet-build-wide-and-of-lit-list-fix-lits

(defthm aignet-build-wide-and-of-lit-list-fix-lits
  (equal (aignet-build-wide-and (lit-list-fix lits)
                                gatesimp strash aignet)
         (aignet-build-wide-and lits gatesimp strash aignet)))

Theorem: aignet-build-wide-and-lit-list-equiv-congruence-on-lits

(defthm aignet-build-wide-and-lit-list-equiv-congruence-on-lits
 (implies
  (satlink::lit-list-equiv lits lits-equiv)
  (equal (aignet-build-wide-and lits gatesimp strash aignet)
         (aignet-build-wide-and lits-equiv gatesimp strash aignet)))
 :rule-classes :congruence)

Theorem: aignet-build-wide-and-of-gatesimp-fix-gatesimp

(defthm aignet-build-wide-and-of-gatesimp-fix-gatesimp
  (equal (aignet-build-wide-and lits (gatesimp-fix gatesimp)
                                strash aignet)
         (aignet-build-wide-and lits gatesimp strash aignet)))

Theorem: aignet-build-wide-and-gatesimp-equiv-congruence-on-gatesimp

(defthm aignet-build-wide-and-gatesimp-equiv-congruence-on-gatesimp
 (implies
  (gatesimp-equiv gatesimp gatesimp-equiv)
  (equal (aignet-build-wide-and lits gatesimp strash aignet)
         (aignet-build-wide-and lits gatesimp-equiv strash aignet)))
 :rule-classes :congruence)

Theorem: aignet-build-wide-and-of-node-list-fix-aignet

(defthm aignet-build-wide-and-of-node-list-fix-aignet
 (equal
      (aignet-build-wide-and lits
                             gatesimp strash (node-list-fix aignet))
      (aignet-build-wide-and lits gatesimp strash aignet)))

Theorem: aignet-build-wide-and-node-list-equiv-congruence-on-aignet

(defthm aignet-build-wide-and-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal (aignet-build-wide-and lits gatesimp strash aignet)
         (aignet-build-wide-and lits gatesimp strash aignet-equiv)))
 :rule-classes :congruence)