• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
        • Svstmt-case
        • Svstmt-while
        • Svstmt-p
        • Svstmt-if
        • Svstmt-equiv
        • Svstmt-xcond
        • Svstmt-scope
        • Svstmt-assign
        • Svstmt-compile
          • Svstmt-compile.lisp
            • Svstate-merge-branches
            • Svex-alist-merge-branches
            • Svstmt-assign->subst
            • Svstack-merge-branches
            • Svstacks-compatible
            • Svjumpstate-merge-svstate-branches
            • Svjumpstate-svstate-compatible
            • Svstmt-lhs-check-masks
            • Svjumpstate
            • Svjumpstates-compatible
            • Svstmtlist-compile-top
            • Svjumpstate-sequence-svstates
            • Constraintlist-merge-branches
            • Svjumpstate-merge-branches
            • Svex-replace-range
            • Svex-svstmt-ite
            • Svstmt-process-write
            • Svjumpstate-sequence
            • Svstmt-process-writelist
            • Svstack-assign
            • Svstmt-writelist-var-sizes
            • Svstates-compatible
            • 4vec-replace-range
            • Svstmt-write-var-sizes
            • Make-empty-svjumpstate
            • Constraintlist-add-pathcond
            • Svjumpstate-pop-scope
            • Constraintlist-compose-svstack
            • Svstack-to-svex-alist
            • Svstack-filter-global-lhs-vars
            • Svjumpstate-vars
            • Svex-svstmt-or
            • Svex-svstmt-andc1
            • Svstate-push-scope
            • Svstate-pop-scope
            • Svstate-vars
            • Svstack-lookup
            • Svar-subtract-delay
            • Svstmt-initialize-locals
            • Svstack-fork
            • Svstack-clean
            • Svstack-nonempty-fix
            • Svstate-fork
            • Svstate-clean
            • Svstack-globalp
            • Svjumpstate-fork
            • Svar-delayed-member
            • Svjumpstate-levels
            • Svjumpstate-free
            • Svstate-free
            • Svstack-free
            • Svstack
            • Svar-size-alist
          • Svstate
        • Svstmt-constraints
        • Svstmt-jump
        • Svstmtlist
        • Svstmt-kind
        • Svstmt.lisp
        • Svstmt-fix
        • Svstmt-count
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svstmt-compile.lisp

Svex-alist-merge-branches

Signature

(svex-alist-merge-branches key-alist cond then-st else-st st-acc) 
  → 
merged-st

Arguments

key-alist — Guard (svex-alist-p key-alist).

cond — Guard (svex-p cond).

then-st — Guard (svex-alist-p then-st).

else-st — Guard (svex-alist-p else-st).

st-acc — Guard (svex-alist-p st-acc).

Returns

merged-st — Type (svex-alist-p merged-st).

Definitions and Theorems

Function: svex-alist-merge-branches

(defun svex-alist-merge-branches
       (key-alist cond then-st else-st st-acc)
  (declare (xargs :guard (and (svex-alist-p key-alist)
                              (svex-p cond)
                              (svex-alist-p then-st)
                              (svex-alist-p else-st)
                              (svex-alist-p st-acc))))
  (let ((__function__ 'svex-alist-merge-branches))
    (declare (ignorable __function__))
    (b* (((when (atom key-alist))
          (svex-alist-fix st-acc))
         ((unless (mbt (and (consp (car key-alist))
                            (svar-p (caar key-alist)))))
          (svex-alist-merge-branches (cdr key-alist)
                                     cond then-st else-st st-acc))
         (key (caar key-alist))
         ((when (svex-fastlookup key st-acc))
          (svex-alist-merge-branches (cdr key-alist)
                                     cond then-st else-st st-acc))
         (then-val (or (svex-fastlookup key then-st)
                       (make-svex-var :name key)))
         (else-val (or (svex-fastlookup key else-st)
                       (make-svex-var :name key)))
         (val (svex-svstmt-ite cond then-val else-val))
         (st-acc (hons-acons key val st-acc)))
      (svex-alist-merge-branches (cdr key-alist)
                                 cond then-st else-st st-acc))))

Theorem: svex-alist-p-of-svex-alist-merge-branches

(defthm svex-alist-p-of-svex-alist-merge-branches
  (b* ((merged-st (svex-alist-merge-branches
                       key-alist cond then-st else-st st-acc)))
    (svex-alist-p merged-st))
  :rule-classes :rewrite)

Theorem: svex-alist-merge-branches-lookup-under-iff

(defthm svex-alist-merge-branches-lookup-under-iff
  (iff (svex-lookup k
                    (svex-alist-merge-branches
                         key-alist cond then-st else-st st-acc))
       (or (svex-lookup k st-acc)
           (svex-lookup k key-alist))))

Theorem: svex-alist-merge-branches-when-cond-true-lookup

(defthm svex-alist-merge-branches-when-cond-true-lookup
 (implies
  (equal (4vec-reduction-or (svex-eval cond env))
         -1)
  (equal
      (svex-eval
           (svex-lookup k
                        (svex-alist-merge-branches
                             key-alist cond then-st else-st st-acc))
           env)
      (if (svex-lookup k st-acc)
          (svex-eval (svex-lookup k st-acc) env)
        (if (svex-lookup k key-alist)
            (if (svex-lookup k then-st)
                (svex-eval (svex-lookup k then-st) env)
              (svex-env-lookup k env))
          (4vec-x))))))

Theorem: svex-alist-merge-branches-when-cond-false-lookup

(defthm svex-alist-merge-branches-when-cond-false-lookup
 (implies
  (equal (4vec-reduction-or (svex-eval cond env))
         0)
  (equal
      (svex-eval
           (svex-lookup k
                        (svex-alist-merge-branches
                             key-alist cond then-st else-st st-acc))
           env)
      (if (svex-lookup k st-acc)
          (svex-eval (svex-lookup k st-acc) env)
        (if (svex-lookup k key-alist)
            (if (svex-lookup k else-st)
                (svex-eval (svex-lookup k else-st) env)
              (svex-env-lookup k env))
          (4vec-x))))))

Theorem: keys-of-svex-alist-merge-branches

(defthm keys-of-svex-alist-merge-branches
 (implies
  (and (not (member v (svex-alist-keys then-st)))
       (not (member v (svex-alist-keys else-st)))
       (not (member v (svex-alist-keys st-acc)))
       (not (member v (svex-alist-keys key-alist))))
  (not
   (member
    v
    (svex-alist-keys
        (svex-alist-merge-branches key-alist
                                   cond then-st else-st st-acc))))))

Theorem: svex-lookup-of-svex-alist-merge-branches

(defthm svex-lookup-of-svex-alist-merge-branches
 (implies
  (and (not (member v (svex-alist-keys then-st)))
       (not (member v (svex-alist-keys else-st)))
       (not (member v (svex-alist-keys st-acc)))
       (not (member v (svex-alist-keys key-alist)))
       (svar-p v))
  (not
    (svex-lookup
         v
         (svex-alist-merge-branches key-alist
                                    cond then-st else-st st-acc)))))

Theorem: vars-of-svex-alist-merge-branches

(defthm vars-of-svex-alist-merge-branches
 (implies
  (and (not (member v (svex-vars cond)))
       (not (member v (svex-alist-vars then-st)))
       (not (member v (svex-alist-vars else-st)))
       (not (member v (svex-alist-vars st-acc)))
       (not (member v (svex-alist-keys key-alist))))
  (not
   (member
    v
    (svex-alist-vars
        (svex-alist-merge-branches key-alist
                                   cond then-st else-st st-acc))))))

Theorem: svex-alist-merge-branches-of-svex-alist-fix-key-alist

(defthm svex-alist-merge-branches-of-svex-alist-fix-key-alist
  (equal (svex-alist-merge-branches (svex-alist-fix key-alist)
                                    cond then-st else-st st-acc)
         (svex-alist-merge-branches
              key-alist cond then-st else-st st-acc)))

Theorem: svex-alist-merge-branches-svex-alist-equiv-congruence-on-key-alist

(defthm
 svex-alist-merge-branches-svex-alist-equiv-congruence-on-key-alist
 (implies
  (svex-alist-equiv key-alist key-alist-equiv)
  (equal
   (svex-alist-merge-branches key-alist cond then-st else-st st-acc)
   (svex-alist-merge-branches key-alist-equiv
                              cond then-st else-st st-acc)))
 :rule-classes :congruence)

Theorem: svex-alist-merge-branches-of-svex-fix-cond

(defthm svex-alist-merge-branches-of-svex-fix-cond
  (equal (svex-alist-merge-branches key-alist (svex-fix cond)
                                    then-st else-st st-acc)
         (svex-alist-merge-branches
              key-alist cond then-st else-st st-acc)))

Theorem: svex-alist-merge-branches-svex-equiv-congruence-on-cond

(defthm svex-alist-merge-branches-svex-equiv-congruence-on-cond
 (implies
  (svex-equiv cond cond-equiv)
  (equal
   (svex-alist-merge-branches key-alist cond then-st else-st st-acc)
   (svex-alist-merge-branches key-alist
                              cond-equiv then-st else-st st-acc)))
 :rule-classes :congruence)

Theorem: svex-alist-merge-branches-of-svex-alist-fix-then-st

(defthm svex-alist-merge-branches-of-svex-alist-fix-then-st
 (equal
  (svex-alist-merge-branches key-alist cond (svex-alist-fix then-st)
                             else-st st-acc)
  (svex-alist-merge-branches
       key-alist cond then-st else-st st-acc)))

Theorem: svex-alist-merge-branches-svex-alist-equiv-congruence-on-then-st

(defthm
   svex-alist-merge-branches-svex-alist-equiv-congruence-on-then-st
 (implies
  (svex-alist-equiv then-st then-st-equiv)
  (equal
   (svex-alist-merge-branches key-alist cond then-st else-st st-acc)
   (svex-alist-merge-branches key-alist
                              cond then-st-equiv else-st st-acc)))
 :rule-classes :congruence)

Theorem: svex-alist-merge-branches-of-svex-alist-fix-else-st

(defthm svex-alist-merge-branches-of-svex-alist-fix-else-st
 (equal
    (svex-alist-merge-branches key-alist
                               cond then-st (svex-alist-fix else-st)
                               st-acc)
    (svex-alist-merge-branches
         key-alist cond then-st else-st st-acc)))

Theorem: svex-alist-merge-branches-svex-alist-equiv-congruence-on-else-st

(defthm
   svex-alist-merge-branches-svex-alist-equiv-congruence-on-else-st
 (implies
  (svex-alist-equiv else-st else-st-equiv)
  (equal
   (svex-alist-merge-branches key-alist cond then-st else-st st-acc)
   (svex-alist-merge-branches key-alist
                              cond then-st else-st-equiv st-acc)))
 :rule-classes :congruence)

Theorem: svex-alist-merge-branches-of-svex-alist-fix-st-acc

(defthm svex-alist-merge-branches-of-svex-alist-fix-st-acc
  (equal (svex-alist-merge-branches
              key-alist cond
              then-st else-st (svex-alist-fix st-acc))
         (svex-alist-merge-branches
              key-alist cond then-st else-st st-acc)))

Theorem: svex-alist-merge-branches-svex-alist-equiv-congruence-on-st-acc

(defthm
    svex-alist-merge-branches-svex-alist-equiv-congruence-on-st-acc
 (implies
  (svex-alist-equiv st-acc st-acc-equiv)
  (equal
   (svex-alist-merge-branches key-alist cond then-st else-st st-acc)
   (svex-alist-merge-branches key-alist
                              cond then-st else-st st-acc-equiv)))
 :rule-classes :congruence)