• 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
        • 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
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Alias-norm.lisp

Constraintlist-subst-from-svexarr

Signature

(constraintlist-subst-from-svexarr x aliases svexarr) → xx

Arguments

x — Guard (constraintlist-p x).

Returns

xx — Type (constraintlist-p xx).

Definitions and Theorems

Function: constraintlist-subst-from-svexarr

(defun constraintlist-subst-from-svexarr (x aliases svexarr)
 (declare (xargs :stobjs (aliases svexarr)))
 (declare (xargs :guard (constraintlist-p x)))
 (declare
    (xargs :guard (and (svarlist-boundedp (constraintlist-vars x)
                                          (aliass-length aliases))
                       (svarlist-boundedp (constraintlist-vars x)
                                          (svexs-length svexarr)))))
 (let ((__function__ 'constraintlist-subst-from-svexarr))
  (declare (ignorable __function__))
  (mbe :logic
       (b* (((when (atom x)) nil)
            ((constraint x1) (car x))
            (cond (svex-subst-from-svexarr x1.cond svexarr)))
         (cons (change-constraint x1 :cond cond)
               (constraintlist-subst-from-svexarr (cdr x)
                                                  aliases svexarr)))
       :exec
       (if (atom x)
           nil
         (with-local-stobj
              nrev
              (mv-let (ans nrev)
                      (b* ((nrev (constraintlist-subst-from-svexarr-nrev
                                      x aliases svexarr nrev))
                           ((mv ans nrev)
                            (acl2::nrev-finish nrev)))
                        (mv ans nrev))
                ans))))))

Theorem: constraintlist-p-of-constraintlist-subst-from-svexarr

(defthm constraintlist-p-of-constraintlist-subst-from-svexarr
  (b* ((xx (constraintlist-subst-from-svexarr x aliases svexarr)))
    (constraintlist-p xx))
  :rule-classes :rewrite)

Theorem: constraintlist-subst-from-svexarr-of-constraintlist-fix-x

(defthm constraintlist-subst-from-svexarr-of-constraintlist-fix-x
  (equal (constraintlist-subst-from-svexarr (constraintlist-fix x)
                                            aliases svexarr)
         (constraintlist-subst-from-svexarr x aliases svexarr)))

Theorem: constraintlist-subst-from-svexarr-constraintlist-equiv-congruence-on-x

(defthm
 constraintlist-subst-from-svexarr-constraintlist-equiv-congruence-on-x
 (implies
  (constraintlist-equiv x x-equiv)
  (equal
       (constraintlist-subst-from-svexarr x aliases svexarr)
       (constraintlist-subst-from-svexarr x-equiv aliases svexarr)))
 :rule-classes :congruence)

Theorem: constraintlist-subst-from-svexarr-of-lhslist-fix-aliases

(defthm constraintlist-subst-from-svexarr-of-lhslist-fix-aliases
  (equal (constraintlist-subst-from-svexarr x (lhslist-fix aliases)
                                            svexarr)
         (constraintlist-subst-from-svexarr x aliases svexarr)))

Theorem: constraintlist-subst-from-svexarr-lhslist-equiv-congruence-on-aliases

(defthm
 constraintlist-subst-from-svexarr-lhslist-equiv-congruence-on-aliases
 (implies
  (lhslist-equiv aliases aliases-equiv)
  (equal
       (constraintlist-subst-from-svexarr x aliases svexarr)
       (constraintlist-subst-from-svexarr x aliases-equiv svexarr)))
 :rule-classes :congruence)

Theorem: svarlist-addr-p-of-constraintlist-subst-from-svexarr

(defthm svarlist-addr-p-of-constraintlist-subst-from-svexarr
 (implies
  (and (svarlist-addr-p (svexarr-vars svexarr))
       (svarlist-addr-p (aliases-vars aliases)))
  (svarlist-addr-p
      (constraintlist-vars
           (constraintlist-subst-from-svexarr x aliases svexarr)))))