		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Svex-envs-common-constants-aux

Signature
(svex-envs-common-constants-aux keys masks env1 env2 acc) → new-env
Arguments: keys — Guard (svarlist-p keys).; masks — Guard (svex-mask-alist-p masks).; env1 — Guard (svex-env-p env1).; env2 — Guard (svex-env-p env2).; acc — Guard (svex-env-p acc).
Returns: new-env — Type (svex-env-p new-env).

Definitions and Theorems

Function: svex-envs-common-constants-aux

(defun svex-envs-common-constants-aux (keys masks env1 env2 acc)
  (declare (xargs :guard (and (svarlist-p keys)
                              (svex-mask-alist-p masks)
                              (svex-env-p env1)
                              (svex-env-p env2)
                              (svex-env-p acc))))
  (let ((__function__ 'svex-envs-common-constants-aux))
    (declare (ignorable __function__))
    (b* (((when (atom keys)) (svex-env-fix acc))
         (key (car keys))
         (mask (svex-mask-lookup (svex-var key) masks))
         ((when (equal mask 0))
          (svex-envs-common-constants-aux (cdr keys)
                                          masks env1 env2 acc))
         (boundp1 (svex-env-boundp key env1))
         ((unless boundp1)
          (svex-envs-common-constants-aux (cdr keys)
                                          masks env1 env2 acc))
         (boundp2 (svex-env-boundp key env2))
         ((unless boundp2)
          (svex-envs-common-constants-aux (cdr keys)
                                          masks env1 env2 acc))
         (val1 (4vec-mask mask (svex-env-lookup key env1)))
         (val2 (4vec-mask mask (svex-env-lookup key env2)))
         (acc (if (equal val1 val2)
                  (hons-acons (svar-fix key) val1 acc)
                acc)))
      (svex-envs-common-constants-aux (cdr keys)
                                      masks env1 env2 acc))))

Theorem: svex-env-p-of-svex-envs-common-constants-aux

(defthm svex-env-p-of-svex-envs-common-constants-aux
  (b*
   ((new-env
         (svex-envs-common-constants-aux keys masks env1 env2 acc)))
   (svex-env-p new-env))
  :rule-classes :rewrite)

Theorem: svex-env-lookup-of-svex-envs-common-constants-aux

(defthm svex-env-lookup-of-svex-envs-common-constants-aux
  (b*
   ((?new-env
         (svex-envs-common-constants-aux keys masks env1 env2 acc)))
   (equal
        (svex-env-lookup key new-env)
        (if (member-equal (svar-fix key)
                          (svarlist-fix keys))
            (b* ((mask (svex-mask-lookup (svex-var key) masks))
                 (val1 (4vec-mask mask (svex-env-lookup key env1)))
                 (val2 (4vec-mask mask (svex-env-lookup key env2))))
              (if (and (svex-env-boundp key env1)
                       (svex-env-boundp key env2)
                       (not (equal 0 mask))
                       (equal val1 val2))
                  val1
                (svex-env-lookup key acc)))
          (svex-env-lookup key acc)))))

Theorem: svex-env-boundp-of-svex-envs-common-constants-aux

(defthm svex-env-boundp-of-svex-envs-common-constants-aux
  (b*
   ((?new-env
         (svex-envs-common-constants-aux keys masks env1 env2 acc)))
   (equal
        (svex-env-boundp key new-env)
        (if (member-equal (svar-fix key)
                          (svarlist-fix keys))
            (b* ((mask (svex-mask-lookup (svex-var key) masks))
                 (val1 (4vec-mask mask (svex-env-lookup key env1)))
                 (val2 (4vec-mask mask (svex-env-lookup key env2))))
              (or (and (svex-env-boundp key env1)
                       (svex-env-boundp key env2)
                       (not (equal 0 mask))
                       (equal val1 val2))
                  (svex-env-boundp key acc)))
          (svex-env-boundp key acc)))))