• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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

Svstack-merge-branches

Signature

(svstack-merge-branches cond then-st else-st) → merged-st

Arguments

cond — Guard (svex-p cond).

then-st — Guard (svstack-p then-st).

else-st — Guard (svstack-p else-st).

Returns

merged-st — Type (svstack-p merged-st).

Definitions and Theorems

Function: svstack-merge-branches

(defun svstack-merge-branches (cond then-st else-st)
  (declare (xargs :guard (and (svex-p cond)
                              (svstack-p then-st)
                              (svstack-p else-st))))
  (let ((__function__ 'svstack-merge-branches))
    (declare (ignorable __function__))
    (b* (((when (or (atom then-st) (atom else-st)))
          nil)
         (then-alist (car then-st))
         (else-alist (car else-st))
         (first (b* (((with-fast then-alist else-alist))
                     (first nil)
                     (first (svex-alist-merge-branches
                                 then-alist
                                 cond then-alist else-alist first))
                     (first (svex-alist-merge-branches
                                 else-alist
                                 cond then-alist else-alist first)))
                  first)))
      (cons first
            (svstack-merge-branches cond (cdr then-st)
                                    (cdr else-st))))))

Theorem: svstack-p-of-svstack-merge-branches

(defthm svstack-p-of-svstack-merge-branches
  (b* ((merged-st (svstack-merge-branches cond then-st else-st)))
    (svstack-p merged-st))
  :rule-classes :rewrite)

Theorem: svstack-merge-branches-lookup-under-iff

(defthm svstack-merge-branches-lookup-under-iff
 (implies
  (double-rewrite (svstacks-compatible then-st else-st))
  (iff
   (svex-lookup k
                (svstack-to-svex-alist
                     (svstack-merge-branches cond then-st else-st)))
   (or (svex-lookup k (svstack-to-svex-alist then-st))
       (svex-lookup k (svstack-to-svex-alist else-st))))))

Theorem: svstack-merge-branches-when-cond-true-lookup

(defthm svstack-merge-branches-when-cond-true-lookup
 (implies
  (and (equal (4vec-reduction-or (svex-eval cond env))
              -1)
       (svstacks-compatible then-st else-st))
  (equal
      (svex-eval
           (svex-lookup
                k
                (svstack-to-svex-alist
                     (svstack-merge-branches cond then-st else-st)))
           env)
      (if (svex-lookup k (svstack-to-svex-alist then-st))
          (svex-eval (svex-lookup k (svstack-to-svex-alist then-st))
                     env)
        (if (svex-lookup k (svstack-to-svex-alist else-st))
            (svex-env-lookup k env)
          (4vec-x))))))

Theorem: svstack-merge-branches-when-cond-false-lookup

(defthm svstack-merge-branches-when-cond-false-lookup
 (implies
  (and (equal (4vec-reduction-or (svex-eval cond env))
              0)
       (svstacks-compatible then-st else-st))
  (equal
      (svex-eval
           (svex-lookup
                k
                (svstack-to-svex-alist
                     (svstack-merge-branches cond then-st else-st)))
           env)
      (if (svex-lookup k (svstack-to-svex-alist else-st))
          (svex-eval (svex-lookup k (svstack-to-svex-alist else-st))
                     env)
        (if (svex-lookup k (svstack-to-svex-alist then-st))
            (svex-env-lookup k env)
          (4vec-x))))))

Theorem: keys-of-svstack-merge-branches

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

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

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

Theorem: vars-of-svstack-merge-branches

(defthm vars-of-svstack-merge-branches
 (implies
  (and
    (not (member v (svex-vars cond)))
    (not (member v
                 (svex-alist-vars (svstack-to-svex-alist then-st))))
    (not (member v
                 (svex-alist-vars (svstack-to-svex-alist else-st))))
    (not (member v
                 (svex-alist-keys (svstack-to-svex-alist then-st))))
    (not (member v
                 (svex-alist-keys (svstack-to-svex-alist else-st))))
    (double-rewrite (svstacks-compatible then-st else-st)))
  (not
   (member
       v
       (svex-alist-vars
            (svstack-to-svex-alist
                 (svstack-merge-branches cond then-st else-st)))))))

Theorem: svstack-merge-branches-compatible

(defthm svstack-merge-branches-compatible
  (b* ((?merged-st (svstack-merge-branches cond then-st else-st)))
    (implies
         (double-rewrite (svstacks-compatible then-st else-st))
         (svstacks-compatible merged-st (double-rewrite then-st)))))

Theorem: svstack-merge-branches-consp

(defthm svstack-merge-branches-consp
  (b* ((?merged-st (svstack-merge-branches cond then-st else-st)))
    (implies (and (consp then-st) (consp else-st))
             (consp merged-st))))

Theorem: svstack-merge-branches-len

(defthm svstack-merge-branches-len
  (b* ((?merged-st (svstack-merge-branches cond then-st else-st)))
    (equal (len merged-st)
           (min (len then-st) (len else-st)))))

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

(defthm svstack-merge-branches-of-svex-fix-cond
  (equal (svstack-merge-branches (svex-fix cond)
                                 then-st else-st)
         (svstack-merge-branches cond then-st else-st)))

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

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

Theorem: svstack-merge-branches-of-svstack-fix-then-st

(defthm svstack-merge-branches-of-svstack-fix-then-st
  (equal (svstack-merge-branches cond (svstack-fix then-st)
                                 else-st)
         (svstack-merge-branches cond then-st else-st)))

Theorem: svstack-merge-branches-svstack-equiv-congruence-on-then-st

(defthm svstack-merge-branches-svstack-equiv-congruence-on-then-st
  (implies
       (svstack-equiv then-st then-st-equiv)
       (equal (svstack-merge-branches cond then-st else-st)
              (svstack-merge-branches cond then-st-equiv else-st)))
  :rule-classes :congruence)

Theorem: svstack-merge-branches-of-svstack-fix-else-st

(defthm svstack-merge-branches-of-svstack-fix-else-st
  (equal (svstack-merge-branches cond then-st (svstack-fix else-st))
         (svstack-merge-branches cond then-st else-st)))

Theorem: svstack-merge-branches-svstack-equiv-congruence-on-else-st

(defthm svstack-merge-branches-svstack-equiv-congruence-on-else-st
  (implies
       (svstack-equiv else-st else-st-equiv)
       (equal (svstack-merge-branches cond then-st else-st)
              (svstack-merge-branches cond then-st else-st-equiv)))
  :rule-classes :congruence)