		Search-engine friendly clone of the ACL2 documentation.

Parametrize

Ubdd-to-aignet-memo-ok

Signature
(ubdd-to-aignet-memo-ok memo litarr aignet invals regvals) → ok
Arguments: memo — Guard (ubdd-to-aignet-memo-p memo).

Definitions and Theorems

Function: ubdd-to-aignet-memo-ok

(defun ubdd-to-aignet-memo-ok (memo litarr aignet invals regvals)
 (declare (xargs :stobjs (litarr aignet invals regvals)))
 (declare (xargs :guard (ubdd-to-aignet-memo-p memo)))
 (let ((__function__ 'ubdd-to-aignet-memo-ok))
  (declare (ignorable __function__))
  (b*
   (((when (atom memo)) t)
    ((unless (mbt (and (consp (car memo))
                       (ubdd/level-p (caar memo)))))
     (ubdd-to-aignet-memo-ok (cdr memo)
                             litarr aignet invals regvals))
    ((cons (ubdd/level key) lit) (car memo))
    (values
     (bits->bools
          (non-exec (lit-eval-list litarr invals regvals aignet)))))
   (and
     (equal
          (lit-eval lit invals regvals aignet)
          (bool->bit
               (acl2::eval-bdd key.ubdd (nthcdr key.level values))))
     (ubdd-to-aignet-memo-ok (cdr memo)
                             litarr aignet invals regvals)))))

Theorem: ubdd-to-aignet-memo-ok-implies-rewrite

(defthm ubdd-to-aignet-memo-ok-implies-rewrite
 (b*
  ((?ok (ubdd-to-aignet-memo-ok memo litarr aignet invals regvals)))
  (implies
   (and ok (ubdd/level-p key)
        (hons-assoc-equal key memo))
   (equal
    (lit-eval (cdr (hons-assoc-equal key memo))
              invals regvals aignet)
    (b*
     (((ubdd/level key))
      (values
        (bits->bools (lit-eval-list litarr invals regvals aignet))))
     (bool->bit (acl2::eval-bdd key.ubdd
                                (nthcdr key.level values))))))))

Theorem: ubdd-to-aignet-memo-ok-of-aignet-extension

(defthm ubdd-to-aignet-memo-ok-of-aignet-extension
 (implies
  (and (aignet-extension-binding)
       (aignet-lit-listp (alist-vals (ubdd-to-aignet-memo-fix memo))
                         orig)
       (aignet-lit-listp litarr orig))
  (iff (ubdd-to-aignet-memo-ok memo litarr new invals regvals)
       (ubdd-to-aignet-memo-ok memo litarr orig invals regvals))))

Theorem: ubdd-to-aignet-memo-ok-of-nil

(defthm ubdd-to-aignet-memo-ok-of-nil
  (ubdd-to-aignet-memo-ok nil litarr aignet invals regvals))

Theorem: ubdd-to-aignet-memo-ok-of-ubdd-to-aignet-memo-fix-memo

(defthm ubdd-to-aignet-memo-ok-of-ubdd-to-aignet-memo-fix-memo
 (equal (ubdd-to-aignet-memo-ok (ubdd-to-aignet-memo-fix memo)
                                litarr aignet invals regvals)
        (ubdd-to-aignet-memo-ok memo litarr aignet invals regvals)))

Theorem: ubdd-to-aignet-memo-ok-ubdd-to-aignet-memo-equiv-congruence-on-memo

(defthm
 ubdd-to-aignet-memo-ok-ubdd-to-aignet-memo-equiv-congruence-on-memo
 (implies
   (ubdd-to-aignet-memo-equiv memo memo-equiv)
   (equal (ubdd-to-aignet-memo-ok memo litarr aignet invals regvals)
          (ubdd-to-aignet-memo-ok memo-equiv
                                  litarr aignet invals regvals)))
 :rule-classes :congruence)

Theorem: ubdd-to-aignet-memo-ok-of-node-list-fix-aignet

(defthm ubdd-to-aignet-memo-ok-of-node-list-fix-aignet
 (equal (ubdd-to-aignet-memo-ok memo litarr (node-list-fix aignet)
                                invals regvals)
        (ubdd-to-aignet-memo-ok memo litarr aignet invals regvals)))

Theorem: ubdd-to-aignet-memo-ok-node-list-equiv-congruence-on-aignet

(defthm ubdd-to-aignet-memo-ok-node-list-equiv-congruence-on-aignet
 (implies
  (node-list-equiv aignet aignet-equiv)
  (equal
       (ubdd-to-aignet-memo-ok memo litarr aignet invals regvals)
       (ubdd-to-aignet-memo-ok memo
                               litarr aignet-equiv invals regvals)))
 :rule-classes :congruence)