• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • 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

Svjumpstate-merge-svstate-branches

Signature

(svjumpstate-merge-svstate-branches 
     cond thencond elsecond thenst elsest) 
 
  → 
merged-st

Arguments

cond — Guard (svex-p cond).

thencond — Guard (svex-p thencond).

elsecond — Guard (svex-p elsecond).

thenst — Guard (svstate-p thenst).

elsest — Guard (svstate-p elsest).

Returns

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

Definitions and Theorems

Function: svjumpstate-merge-svstate-branches

(defun svjumpstate-merge-svstate-branches
       (cond thencond elsecond thenst elsest)
  (declare (xargs :guard (and (svex-p cond)
                              (svex-p thencond)
                              (svex-p elsecond)
                              (svstate-p thenst)
                              (svstate-p elsest))))
  (let ((__function__ 'svjumpstate-merge-svstate-branches))
    (declare (ignorable __function__))
    (b* ((thencond (svex-fix thencond))
         (elsecond (svex-fix elsecond))
         (thenst (svstate-fix thenst))
         (elsest (svstate-fix elsest))
         ((when (eql 0 elsecond)) thenst)
         ((when (eql 0 thencond)) elsest))
      (svstate-merge-branches cond thenst elsest))))

Theorem: svstate-p-of-svjumpstate-merge-svstate-branches

(defthm svstate-p-of-svjumpstate-merge-svstate-branches
  (b* ((merged-st (svjumpstate-merge-svstate-branches
                       cond thencond elsecond thenst elsest)))
    (svstate-p merged-st))
  :rule-classes :rewrite)

Theorem: vars-of-svjumpstate-merge-svstate-branches

(defthm vars-of-svjumpstate-merge-svstate-branches
  (b* ((?merged-st (svjumpstate-merge-svstate-branches
                        cond thencond elsecond thenst elsest)))
    (implies (and (svstates-compatible thenst elsest)
                  (not (member v (svex-vars cond)))
                  (not (member v (svstate-vars thenst)))
                  (not (member v (svstate-vars elsest))))
             (not (member v (svstate-vars merged-st))))))

Theorem: svjumpstate-merge-svstate-branches-preserves-compatible

(defthm svjumpstate-merge-svstate-branches-preserves-compatible
  (b* ((?merged-st (svjumpstate-merge-svstate-branches
                        cond thencond elsecond thenst elsest)))
    (implies (svstates-compatible thenst elsest)
             (svstates-compatible merged-st thenst))))

Theorem: svjumpstate-merge-svstate-branches-of-svex-fix-cond

(defthm svjumpstate-merge-svstate-branches-of-svex-fix-cond
  (equal (svjumpstate-merge-svstate-branches
              (svex-fix cond)
              thencond elsecond thenst elsest)
         (svjumpstate-merge-svstate-branches
              cond thencond elsecond thenst elsest)))

Theorem: svjumpstate-merge-svstate-branches-svex-equiv-congruence-on-cond

(defthm
   svjumpstate-merge-svstate-branches-svex-equiv-congruence-on-cond
  (implies (svex-equiv cond cond-equiv)
           (equal (svjumpstate-merge-svstate-branches
                       cond thencond elsecond thenst elsest)
                  (svjumpstate-merge-svstate-branches
                       cond-equiv
                       thencond elsecond thenst elsest)))
  :rule-classes :congruence)

Theorem: svjumpstate-merge-svstate-branches-of-svex-fix-thencond

(defthm svjumpstate-merge-svstate-branches-of-svex-fix-thencond
 (equal (svjumpstate-merge-svstate-branches cond (svex-fix thencond)
                                            elsecond thenst elsest)
        (svjumpstate-merge-svstate-branches
             cond thencond elsecond thenst elsest)))

Theorem: svjumpstate-merge-svstate-branches-svex-equiv-congruence-on-thencond

(defthm
 svjumpstate-merge-svstate-branches-svex-equiv-congruence-on-thencond
 (implies (svex-equiv thencond thencond-equiv)
          (equal (svjumpstate-merge-svstate-branches
                      cond thencond elsecond thenst elsest)
                 (svjumpstate-merge-svstate-branches
                      cond
                      thencond-equiv elsecond thenst elsest)))
 :rule-classes :congruence)

Theorem: svjumpstate-merge-svstate-branches-of-svex-fix-elsecond

(defthm svjumpstate-merge-svstate-branches-of-svex-fix-elsecond
  (equal (svjumpstate-merge-svstate-branches
              cond thencond (svex-fix elsecond)
              thenst elsest)
         (svjumpstate-merge-svstate-branches
              cond thencond elsecond thenst elsest)))

Theorem: svjumpstate-merge-svstate-branches-svex-equiv-congruence-on-elsecond

(defthm
 svjumpstate-merge-svstate-branches-svex-equiv-congruence-on-elsecond
 (implies (svex-equiv elsecond elsecond-equiv)
          (equal (svjumpstate-merge-svstate-branches
                      cond thencond elsecond thenst elsest)
                 (svjumpstate-merge-svstate-branches
                      cond
                      thencond elsecond-equiv thenst elsest)))
 :rule-classes :congruence)

Theorem: svjumpstate-merge-svstate-branches-of-svstate-fix-thenst

(defthm svjumpstate-merge-svstate-branches-of-svstate-fix-thenst
  (equal (svjumpstate-merge-svstate-branches
              cond
              thencond elsecond (svstate-fix thenst)
              elsest)
         (svjumpstate-merge-svstate-branches
              cond thencond elsecond thenst elsest)))

Theorem: svjumpstate-merge-svstate-branches-svstate-equiv-congruence-on-thenst

(defthm
 svjumpstate-merge-svstate-branches-svstate-equiv-congruence-on-thenst
 (implies (svstate-equiv thenst thenst-equiv)
          (equal (svjumpstate-merge-svstate-branches
                      cond thencond elsecond thenst elsest)
                 (svjumpstate-merge-svstate-branches
                      cond
                      thencond elsecond thenst-equiv elsest)))
 :rule-classes :congruence)

Theorem: svjumpstate-merge-svstate-branches-of-svstate-fix-elsest

(defthm svjumpstate-merge-svstate-branches-of-svstate-fix-elsest
  (equal (svjumpstate-merge-svstate-branches
              cond thencond
              elsecond thenst (svstate-fix elsest))
         (svjumpstate-merge-svstate-branches
              cond thencond elsecond thenst elsest)))

Theorem: svjumpstate-merge-svstate-branches-svstate-equiv-congruence-on-elsest

(defthm
 svjumpstate-merge-svstate-branches-svstate-equiv-congruence-on-elsest
 (implies (svstate-equiv elsest elsest-equiv)
          (equal (svjumpstate-merge-svstate-branches
                      cond thencond elsecond thenst elsest)
                 (svjumpstate-merge-svstate-branches
                      cond
                      thencond elsecond thenst elsest-equiv)))
 :rule-classes :congruence)