• 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
        • Decomp.lisp
          • Svex-env-compat-union
          • Svdecomp-symenv-compat-union
          • Svexlists-rewrite-until-same
          • Svdecomp-normalize-svexlist-eval
          • Svex-decomp-process-env-term
          • Map-alist-term-keys-to-val-terms
          • Envmap-extract-union-env
          • Alist-collect-compositions
          • Envmap-entry-extract-env
          • Svdecomp-env-extract
          • Svex-alist-evaluation-to-symenv
          • Envmap-entry-to-term-alist
          • Svar-lookup
          • Svar-alist-keys
          • Map-alist-const-keys-to-val-terms
          • Svdecomp-svex?-eval-compare-term
          • Svdecomp-equal-svex-evals-metafun
          • Svdecomp-equal-svex-alist-evals-metafun
          • Envmap->svex-alist
          • Envmap-to-term-alist
          • Svdecomp-equal-svexlist-evals-metafun
          • Pseudo-term-fix
          • Svdecomp-symenv->term
          • Svdecomp-svex-alist-eval-metafun
          • Svdecomp-ev-symenv
          • Svdecomp-svexlist-eval-metafun
          • Svdecomp-svex-eval-metafun
          • Svdecomp-ev-envmap
          • Envmap
          • Svex-alist-alist
          • Svdecomp-symenv
          • Svdecomp-get-rewrite-limit
        • Svdecomp-hints
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Decomp.lisp

Svexlists-rewrite-until-same

Signature

(svexlists-rewrite-until-same x y limit) → (mv xx yy)

Arguments

x — Guard (svexlist-p x).

y — Guard (svexlist-p y).

limit — Guard (natp limit).

Returns

xx — Type (svexlist-p xx).

yy — Type (svexlist-p yy).

Definitions and Theorems

Function: svexlists-rewrite-until-same

(defun svexlists-rewrite-until-same (x y limit)
 (declare (xargs :guard (and (svexlist-p x)
                             (svexlist-p y)
                             (natp limit))))
 (let ((__function__ 'svexlists-rewrite-until-same))
  (declare (ignorable __function__))
  (b*
   (((when (zp limit))
     (cw
      "svexlists-rewrite-until-same: limit ran out.  Total size: ~x0, x: ~x1, y: ~x2~%"
      (svexlist-opcount (append x y))
      (svexlist-opcount x)
      (svexlist-opcount y))
     (mv (svexlist-fix x) (svexlist-fix y)))
    ((when (hons-equal (svexlist-fix x)
                       (svexlist-fix y)))
     (cw "svexlists-rewrite-until-same: success~%")
     (mv (svexlist-fix x) (svexlist-fix y)))
    (rw (svexlist-rewrite-top (append x y)
                              :verbosep t))
    (len (len x))
    (newx (take len rw))
    (newy (nthcdr len rw))
    ((when (and (hons-equal newx (svexlist-fix x))
                (hons-equal newy (svexlist-fix y))))
     (cw "svexlists-rewrite-until-same: fail, sizes: ~x0, ~x1~%"
         (svexlist-opcount newx)
         (svexlist-opcount newy))
     (mv newx newy)))
   (svexlists-rewrite-until-same newx newy (1- limit)))))

Theorem: svexlist-p-of-svexlists-rewrite-until-same.xx

(defthm svexlist-p-of-svexlists-rewrite-until-same.xx
  (b* (((mv ?xx ?yy)
        (svexlists-rewrite-until-same x y limit)))
    (svexlist-p xx))
  :rule-classes :rewrite)

Theorem: svexlist-p-of-svexlists-rewrite-until-same.yy

(defthm svexlist-p-of-svexlists-rewrite-until-same.yy
  (b* (((mv ?xx ?yy)
        (svexlists-rewrite-until-same x y limit)))
    (svexlist-p yy))
  :rule-classes :rewrite)

Theorem: svexlists-rewrite-until-same-correct

(defthm svexlists-rewrite-until-same-correct
  (b* (((mv newx newy)
        (svexlists-rewrite-until-same x y limit)))
    (and (equal (svexlist-eval newx env)
                (svexlist-eval x env))
         (equal (svexlist-eval newy env)
                (svexlist-eval y env)))))

Theorem: len-of-svexlists-rewrite-until-same

(defthm len-of-svexlists-rewrite-until-same
  (b* (((mv newx newy)
        (svexlists-rewrite-until-same x y limit)))
    (and (equal (len newx) (len x))
         (equal (len newy) (len y)))))

Theorem: consp-of-svexlists-rewrite-until-same

(defthm consp-of-svexlists-rewrite-until-same
  (b* (((mv newx newy)
        (svexlists-rewrite-until-same x y limit)))
    (and (equal (consp newx) (consp x))
         (equal (consp newy) (consp y)))))

Theorem: svexlists-rewrite-until-same-of-svexlist-fix-x

(defthm svexlists-rewrite-until-same-of-svexlist-fix-x
  (equal (svexlists-rewrite-until-same (svexlist-fix x)
                                       y limit)
         (svexlists-rewrite-until-same x y limit)))

Theorem: svexlists-rewrite-until-same-svexlist-equiv-congruence-on-x

(defthm svexlists-rewrite-until-same-svexlist-equiv-congruence-on-x
  (implies (svexlist-equiv x x-equiv)
           (equal (svexlists-rewrite-until-same x y limit)
                  (svexlists-rewrite-until-same x-equiv y limit)))
  :rule-classes :congruence)

Theorem: svexlists-rewrite-until-same-of-svexlist-fix-y

(defthm svexlists-rewrite-until-same-of-svexlist-fix-y
  (equal (svexlists-rewrite-until-same x (svexlist-fix y)
                                       limit)
         (svexlists-rewrite-until-same x y limit)))

Theorem: svexlists-rewrite-until-same-svexlist-equiv-congruence-on-y

(defthm svexlists-rewrite-until-same-svexlist-equiv-congruence-on-y
  (implies (svexlist-equiv y y-equiv)
           (equal (svexlists-rewrite-until-same x y limit)
                  (svexlists-rewrite-until-same x y-equiv limit)))
  :rule-classes :congruence)

Theorem: svexlists-rewrite-until-same-of-nfix-limit

(defthm svexlists-rewrite-until-same-of-nfix-limit
  (equal (svexlists-rewrite-until-same x y (nfix limit))
         (svexlists-rewrite-until-same x y limit)))

Theorem: svexlists-rewrite-until-same-nat-equiv-congruence-on-limit

(defthm svexlists-rewrite-until-same-nat-equiv-congruence-on-limit
  (implies (nat-equiv limit limit-equiv)
           (equal (svexlists-rewrite-until-same x y limit)
                  (svexlists-rewrite-until-same x y limit-equiv)))
  :rule-classes :congruence)