• 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
      • Sv-tutorial
      • Expressions
        • Rewriting
          • Svex-rewrite
          • Svexlist-rewrite-nrev
          • Svex-args-apply-masks
          • 4veclist-quote
          • Svex-simpconfig-p
          • Svex-rewrite-memo-correct
          • Svex-alist-maybe-rewrite-fixpoint
          • Svexlist-compute-masks
          • Svexlist-rewrite-under-masks
          • Svex-alist-rewrite-fixpoint
          • Svexlist-maybe-rewrite-fixpoint
          • Svexlist-rewrite-fixpoint
          • Svexlist-mask-acons
          • Svexlist-mask-alist/toposort
          • Svex-call-simp
          • Svex-alist-compose
          • Svexlist-rewrite-top
          • Svex-alist-subst
          • Svex-alist-compose-rw
          • Svex-argmasks-lookup
          • Svex-alist-subst-rw
          • Svexlist-mask-acons-rev
          • Svex-mask-lookup
          • Svex-mask-acons
          • Svexlist-mask-alist
          • Svex-alist-rewrite-top
          • Constraintlist-compose
          • Svex-substconfig
          • Svex-simpconfig-fix
          • Svex-subst
          • Svex-rewrite-memo-vars-ok
          • Svex-norm-call
          • Svex-3value-mask
          • Svexlist-count-calls-aux
          • Svex-mask-alist-keys
          • Rewriter-tracing
          • Svex-rewrite-top
          • Svexlist-maskfree-rewrite-nrev
          • Svexlist-multirefs-top
          • Svexlist-count-calls
          • Svex-unify
          • Svexlist-toposort-p
          • Svexlist-maskfree-rewrite-top
          • Svex-alist-compose-nrev
          • Rewriting-concatenations
          • Svex-svex-memo
          • Svex-mask-alist
          • Svex-alist-subst-nrev
          • Svex-simpconfig-fix!
          • Svex-rewrite-rules
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Rewriting

Svex-call-simp

Signature

(svex-call-simp fn args simp) → call

Arguments

fn — Guard (fnsym-p fn).

args — Guard (svexlist-p args).

simp — Guard (svex-simpconfig-p simp).

Returns

call — Type (svex-p call).

Definitions and Theorems

Function: svex-call-simp

(defun svex-call-simp (fn args simp)
  (declare (xargs :guard (and (fnsym-p fn)
                              (svexlist-p args)
                              (svex-simpconfig-p simp))))
  (let ((__function__ 'svex-call-simp))
    (declare (ignorable __function__))
    (let ((simp (svex-simpconfig-fix simp)))
      (case simp
        ((t) (svex-call* fn args))
        ((nil) (svex-call fn args))
        (otherwise (svex-rewrite-fncall simp -1 fn args t t))))))

Theorem: svex-p-of-svex-call-simp

(defthm svex-p-of-svex-call-simp
  (b* ((call (svex-call-simp fn args simp)))
    (svex-p call))
  :rule-classes :rewrite)

Theorem: svex-call-simp-correct

(defthm svex-call-simp-correct
  (b* ((?call (svex-call-simp fn args simp)))
    (equal (svex-eval call env)
           (svex-eval (svex-call fn args) env))))

Theorem: svex-call-simp-vars

(defthm svex-call-simp-vars
  (b* ((?call (svex-call-simp fn args simp)))
    (implies (not (member v (svexlist-vars args)))
             (not (member v (svex-vars call))))))

Theorem: svex-call-simp-of-fnsym-fix-fn

(defthm svex-call-simp-of-fnsym-fix-fn
  (equal (svex-call-simp (fnsym-fix fn)
                         args simp)
         (svex-call-simp fn args simp)))

Theorem: svex-call-simp-fnsym-equiv-congruence-on-fn

(defthm svex-call-simp-fnsym-equiv-congruence-on-fn
  (implies (fnsym-equiv fn fn-equiv)
           (equal (svex-call-simp fn args simp)
                  (svex-call-simp fn-equiv args simp)))
  :rule-classes :congruence)

Theorem: svex-call-simp-of-svexlist-fix-args

(defthm svex-call-simp-of-svexlist-fix-args
  (equal (svex-call-simp fn (svexlist-fix args)
                         simp)
         (svex-call-simp fn args simp)))

Theorem: svex-call-simp-svexlist-equiv-congruence-on-args

(defthm svex-call-simp-svexlist-equiv-congruence-on-args
  (implies (svexlist-equiv args args-equiv)
           (equal (svex-call-simp fn args simp)
                  (svex-call-simp fn args-equiv simp)))
  :rule-classes :congruence)

Theorem: svex-call-simp-of-svex-simpconfig-fix-simp

(defthm svex-call-simp-of-svex-simpconfig-fix-simp
  (equal (svex-call-simp fn args (svex-simpconfig-fix simp))
         (svex-call-simp fn args simp)))

Theorem: svex-call-simp-svex-simpconfig-equiv-congruence-on-simp

(defthm svex-call-simp-svex-simpconfig-equiv-congruence-on-simp
  (implies (svex-simpconfig-equiv simp simp-equiv)
           (equal (svex-call-simp fn args simp)
                  (svex-call-simp fn args simp-equiv)))
  :rule-classes :congruence)