		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Eval-collection-of-a4vecs-and-aigs

Signature
(eval-collection-of-a4vecs-and-aigs a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env) → (mv a4vecs1-eval a4vecs2-eval aigs1-eval aigs2-eval aigs3-eval)
Arguments: a4vecs1 — Guard (a4veclist-p a4vecs1).; a4vecs2 — Guard (a4veclist-p a4vecs2).; aigs1 — Guard (true-listp aigs1).; aigs2 — Guard (true-listp aigs2).; aigs3 — Guard (true-listp aigs3).
Returns: a4vecs1-eval — Type (4veclist-p a4vecs1-eval).; a4vecs2-eval — Type (4veclist-p a4vecs2-eval).; aigs1-eval — Type (true-listp aigs1-eval).; aigs2-eval — Type (true-listp aigs2-eval).; aigs3-eval — Type (true-listp aigs3-eval).

Definitions and Theorems

Function: eval-collection-of-a4vecs-and-aigs

(defun eval-collection-of-a4vecs-and-aigs
       (a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env)
 (declare (xargs :guard (and (a4veclist-p a4vecs1)
                             (a4veclist-p a4vecs2)
                             (true-listp aigs1)
                             (true-listp aigs2)
                             (true-listp aigs3))))
 (let ((__function__ 'eval-collection-of-a4vecs-and-aigs))
  (declare (ignorable __function__))
  (b*
   ((a4vecs1-aiglist (a4veclist->aiglist a4vecs1))
    (a4vecs2-aiglist (a4veclist->aiglist a4vecs2))
    (all-aigs (my-append a4vecs1-aiglist
                         a4vecs2-aiglist aigs1 aigs2 aigs3))
    (bitlist
     (time$
         (aig-eval-list all-aigs env)
         :msg
         "; SV bit-blasting: aig-eval-list: ~st sec, ~sa bytes.~%"))
    (a4vecs1-len (length a4vecs1-aiglist))
    (a4vecs2-len (length a4vecs2-aiglist))
    (aigs1-len (len aigs1))
    (aigs2-len (len aigs2))
    (a4vecs1-eval
         (time$ (4veclist-from-bitlist a4vecs1 bitlist)
                :msg "; bits->4vecs: ~st sec, ~sa bytes.~%"))
    (bitlist-tail (nthcdr a4vecs1-len bitlist))
    (a4vecs2-eval
         (time$ (4veclist-from-bitlist a4vecs2 bitlist-tail)
                :msg "; bits->4vecs: ~st sec, ~sa bytes.~%"))
    (bitlist-tail (nthcdr a4vecs2-len bitlist-tail))
    (aigs1-eval (take aigs1-len bitlist-tail))
    (bitlist-tail (nthcdr aigs1-len bitlist-tail))
    (aigs2-eval (take aigs2-len bitlist-tail))
    (aigs3-eval (nthcdr aigs2-len bitlist-tail)))
   (mv a4vecs1-eval a4vecs2-eval
       aigs1-eval aigs2-eval aigs3-eval))))

Theorem: 4veclist-p-of-eval-collection-of-a4vecs-and-aigs.a4vecs1-eval

(defthm
      4veclist-p-of-eval-collection-of-a4vecs-and-aigs.a4vecs1-eval
  (b* (((mv ?a4vecs1-eval ?a4vecs2-eval
            ?aigs1-eval ?aigs2-eval ?aigs3-eval)
        (eval-collection-of-a4vecs-and-aigs
             a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env)))
    (4veclist-p a4vecs1-eval))
  :rule-classes :rewrite)

Theorem: 4veclist-p-of-eval-collection-of-a4vecs-and-aigs.a4vecs2-eval

(defthm
      4veclist-p-of-eval-collection-of-a4vecs-and-aigs.a4vecs2-eval
  (b* (((mv ?a4vecs1-eval ?a4vecs2-eval
            ?aigs1-eval ?aigs2-eval ?aigs3-eval)
        (eval-collection-of-a4vecs-and-aigs
             a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env)))
    (4veclist-p a4vecs2-eval))
  :rule-classes :rewrite)

Theorem: true-listp-of-eval-collection-of-a4vecs-and-aigs.aigs1-eval

(defthm true-listp-of-eval-collection-of-a4vecs-and-aigs.aigs1-eval
  (b* (((mv ?a4vecs1-eval ?a4vecs2-eval
            ?aigs1-eval ?aigs2-eval ?aigs3-eval)
        (eval-collection-of-a4vecs-and-aigs
             a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env)))
    (true-listp aigs1-eval))
  :rule-classes :rewrite)

Theorem: true-listp-of-eval-collection-of-a4vecs-and-aigs.aigs2-eval

(defthm true-listp-of-eval-collection-of-a4vecs-and-aigs.aigs2-eval
  (b* (((mv ?a4vecs1-eval ?a4vecs2-eval
            ?aigs1-eval ?aigs2-eval ?aigs3-eval)
        (eval-collection-of-a4vecs-and-aigs
             a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env)))
    (true-listp aigs2-eval))
  :rule-classes :rewrite)

Theorem: true-listp-of-eval-collection-of-a4vecs-and-aigs.aigs3-eval

(defthm true-listp-of-eval-collection-of-a4vecs-and-aigs.aigs3-eval
  (b* (((mv ?a4vecs1-eval ?a4vecs2-eval
            ?aigs1-eval ?aigs2-eval ?aigs3-eval)
        (eval-collection-of-a4vecs-and-aigs
             a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env)))
    (true-listp aigs3-eval))
  :rule-classes :rewrite)

Theorem: eval-collection-of-a4vecs-and-aigs-correct

(defthm eval-collection-of-a4vecs-and-aigs-correct
  (b* (((mv ?a4vecs1-eval ?a4vecs2-eval
            ?aigs1-eval ?aigs2-eval ?aigs3-eval)
        (eval-collection-of-a4vecs-and-aigs
             a4vecs1 a4vecs2 aigs1 aigs2 aigs3 env)))
    (and (equal a4vecs1-eval
                (a4veclist-eval a4vecs1 env))
         (equal a4vecs2-eval
                (a4veclist-eval a4vecs2 env))
         (equal aigs1-eval (aig-eval-list aigs1 env))
         (equal aigs2-eval (aig-eval-list aigs2 env))
         (equal aigs3-eval (aig-eval-list aigs3 env)))))