• 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
        • Alias-normalization
          • Alias-norm.lisp
            • Lhs-alias-canonicalize-replace-top
            • Aliases-bound-fix
            • Lhs-pairs-set-aliases
            • Setalias
            • Lhs-replace-range
            • Lhatom-bound-fix
            • Constraintlist-subst-from-svexarr
            • Aliases-add-pair
            • Lhs-alias-canonicalize-top
            • Lhs-varbound-fix
            • Aliases-bound-fix-aux
            • Canonicalize-alias-pairs
            • Aliases-finish-canonicalize
            • Assigns-subst
            • Aliases-put-pairs
            • Getalias
            • Lhs-alias-norm
            • Constraintlist-subst-from-svexarr-nrev
            • Assigns-subst-nrev
            • Svex-subst-from-svexarr-memo-ok
            • Collect-aliases
            • Aliases-fix
            • Aliases-empty
        • Svex-design-flatten-and-normalize
        • Svex-design-compile
        • Svex-composition
        • Compile.lisp
        • Assign->segment-drivers
        • Segment-driver-map-resolve
        • Assigns->segment-drivers
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Alias-norm.lisp

Lhs-pairs-set-aliases

Signature

(lhs-pairs-set-aliases x y aliases) → aliases1

Arguments

x — Guard (lhs-p x).

y — Guard (lhs-p y).

aliases — Guard (aliases-normorderedp aliases).

Returns

aliases1 — Type (aliases-normorderedp aliases1).

Definitions and Theorems

Function: lhs-pairs-set-aliases

(defun lhs-pairs-set-aliases (x y aliases)
 (declare (xargs :stobjs (aliases)))
 (declare (xargs :guard (and (lhs-p x)
                             (lhs-p y)
                             (aliases-normorderedp aliases))))
 (declare
   (xargs :guard (and (svarlist-boundedp (lhs-vars x)
                                         (aliass-length aliases))
                      (svarlist-boundedp (lhs-vars y)
                                         (aliass-length aliases)))))
 (let ((__function__ 'lhs-pairs-set-aliases))
  (declare (ignorable __function__))
  (b*
   (((mv xf xrest) (lhs-decomp x))
    ((mv yf yrest) (lhs-decomp y))
    ((when (or (not xf) (not yf)))
     (aliases-bound-fix aliases))
    ((lhrange xf) xf)
    ((lhrange yf) yf)
    (xkind (lhatom-kind xf.atom))
    (ykind (lhatom-kind yf.atom))
    ((mv blkw nextx nexty)
     (cond ((< xf.w yf.w)
            (mv xf.w xrest (lhs-rsh xf.w y)))
           ((< yf.w xf.w)
            (mv yf.w (lhs-rsh yf.w x) yrest))
           (t (mv xf.w xrest yrest))))
    ((unless (and (eql (lhatom-kind xf.atom) :var)
                  (eql (lhatom-kind yf.atom) :var)
                  (not (equal xf.atom yf.atom))))
     (lhs-pairs-set-aliases nextx nexty aliases))
    ((lhatom-var xf.atom) xf.atom)
    ((lhatom-var yf.atom) yf.atom)
    (xidx (svar-index xf.atom.name))
    (yidx (svar-index yf.atom.name))
    ((mv less-idx less-offset gr-idx gr-offset)
     (cond ((< xidx yidx)
            (mv xidx xf.atom.rsh yidx yf.atom.rsh))
           ((< yidx xidx)
            (mv yidx yf.atom.rsh xidx xf.atom.rsh))
           ((< xf.atom.rsh yf.atom.rsh)
            (mv xidx xf.atom.rsh yidx yf.atom.rsh))
           (t (mv yidx yf.atom.rsh xidx xf.atom.rsh))))
    (greater-full (getalias gr-idx aliases))
    (less-full (getalias less-idx aliases))
    (less-range (lhs-rsh less-offset less-full))
    (greater-new
         (lhs-replace-range gr-offset blkw less-range greater-full))
    (aliases (setalias gr-idx greater-new aliases)))
   (lhs-pairs-set-aliases nextx nexty aliases))))

Theorem: aliases-normorderedp-of-lhs-pairs-set-aliases

(defthm aliases-normorderedp-of-lhs-pairs-set-aliases
  (b* ((aliases1 (lhs-pairs-set-aliases x y aliases)))
    (aliases-normorderedp aliases1))
  :rule-classes :rewrite)

Theorem: len-of-lhs-pairs-set-aliases-bound

(defthm len-of-lhs-pairs-set-aliases-bound
  (>= (len (lhs-pairs-set-aliases x y aliases))
      (len aliases))
  :rule-classes :linear)

Theorem: len-of-lhs-pairs-set-aliases

(defthm len-of-lhs-pairs-set-aliases
  (implies (and (svarlist-boundedp (lhs-vars x)
                                   (len aliases))
                (svarlist-boundedp (lhs-vars y)
                                   (len aliases)))
           (equal (len (lhs-pairs-set-aliases x y aliases))
                  (len aliases))))

Theorem: lhs-pairs-set-aliases-of-lhs-fix-x

(defthm lhs-pairs-set-aliases-of-lhs-fix-x
  (equal (lhs-pairs-set-aliases (lhs-fix x)
                                y aliases)
         (lhs-pairs-set-aliases x y aliases)))

Theorem: lhs-pairs-set-aliases-lhs-equiv-congruence-on-x

(defthm lhs-pairs-set-aliases-lhs-equiv-congruence-on-x
  (implies (lhs-equiv x x-equiv)
           (equal (lhs-pairs-set-aliases x y aliases)
                  (lhs-pairs-set-aliases x-equiv y aliases)))
  :rule-classes :congruence)

Theorem: lhs-pairs-set-aliases-of-lhs-fix-y

(defthm lhs-pairs-set-aliases-of-lhs-fix-y
  (equal (lhs-pairs-set-aliases x (lhs-fix y)
                                aliases)
         (lhs-pairs-set-aliases x y aliases)))

Theorem: lhs-pairs-set-aliases-lhs-equiv-congruence-on-y

(defthm lhs-pairs-set-aliases-lhs-equiv-congruence-on-y
  (implies (lhs-equiv y y-equiv)
           (equal (lhs-pairs-set-aliases x y aliases)
                  (lhs-pairs-set-aliases x y-equiv aliases)))
  :rule-classes :congruence)

Theorem: lhs-pairs-set-aliases-of-aliases-bound-fix-aliases

(defthm lhs-pairs-set-aliases-of-aliases-bound-fix-aliases
  (equal (lhs-pairs-set-aliases x y (aliases-bound-fix aliases))
         (lhs-pairs-set-aliases x y aliases)))

Theorem: lhs-pairs-set-aliases-aliases-equiv-congruence-on-aliases

(defthm lhs-pairs-set-aliases-aliases-equiv-congruence-on-aliases
  (implies (aliases-equiv aliases aliases-equiv)
           (equal (lhs-pairs-set-aliases x y aliases)
                  (lhs-pairs-set-aliases x y aliases-equiv)))
  :rule-classes :congruence)