• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
      • Svex-simplify
        • Svexlist-simplify
        • 4vec-to-svex
      • Svl-flatten-design
      • Svl-run
      • Svl-run->svex-alist
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svex-simplify

Svexlist-simplify

Try to simplify an sv::svexlist structure with rp::RP-Rewriter using regular rewrite rules about 4vec functions.

Signature

(svexlist-simplify svexlist &key (state 'state) 
                   (rp-state 'rp-state) 
                   (context 'nil) 
                   (runes 'nil) 
                   (reload-rules 't) 
                   (linearize ':auto) 
                   (only-local 'nil) 
                   (vars-are-integer 'nil) 
                   (verbose 'nil)) 
 
  → 
(mv res rp::rp-state-res)

Arguments

svexlist — Guard (svexlist-p svexlist).

verbose — Guard (booleanp verbose).

Returns

res — Type (svexlist-p res).

rp::rp-state-res — Type (valid-rp-state-syntaxp rp::rp-state-res), given (if reload-rules (rp::rp-statep rp-state) (valid-rp-state-syntaxp rp-state)) .

Arguments of svexlist-simplify are the same as svex-simplify

Definitions and Theorems

Function: svexlist-simplify-fn

(defun svexlist-simplify-fn
       (svexlist state rp-state
                 context runes reload-rules linearize
                 only-local vars-are-integer verbose)
 (declare (xargs :stobjs (state rp-state)))
 (declare (xargs :guard (and (svexlist-p svexlist)
                             (booleanp verbose))))
 (declare
  (xargs
   :guard
   (and
    (or reload-rules
        (valid-rp-state-syntaxp rp-state))
    (or
     (rp::context-syntaxp context)
     (cw
      "ATTENTION!  Given context must satisfy rp::context-syntaxp ~%")))
   :stobjs (state rp-state)))
 (let ((acl2::__function__ 'svexlist-simplify))
  (declare (ignorable acl2::__function__))
  (b*
   ((linearize (if (eq linearize ':auto)
                   (zp (cons-count-compare svexlist 2048))
                 linearize))
    ((mv rw rp-state)
     (svexlist-simplify-to-4vec svexlist
                                :state state
                                :context context
                                :runes runes
                                :reload-rules reload-rules
                                :linearize linearize
                                :only-local only-local
                                :vars-are-integer vars-are-integer
                                :verbose verbose))
    ((mv err svexlist-res)
     (if only-local (locally-simplified-to-svexlist rw)
       (4vec-to-svex-termlist rw nil linearize)))
    (-
     (and
      err
      (hard-error
       'svexlist-simplify
       "There was a problem while converting the term below to its ~
svex equivalent. Read above for the printed messages. ~p0 ~%"
       (list (cons #\0 rw))))))
   (mv svexlist-res rp-state))))

Theorem: svexlist-p-of-svexlist-simplify.res

(defthm svexlist-p-of-svexlist-simplify.res
  (b* (((mv ?res rp::?rp-state-res)
        (svexlist-simplify-fn svexlist state rp-state
                              context runes reload-rules linearize
                              only-local vars-are-integer verbose)))
    (svexlist-p res))
  :rule-classes :rewrite)

Theorem: valid-rp-state-syntaxp-of-svexlist-simplify.rp-state-res

(defthm valid-rp-state-syntaxp-of-svexlist-simplify.rp-state-res
 (implies
  (if reload-rules (rp::rp-statep rp-state)
    (valid-rp-state-syntaxp rp-state))
  (b* (((mv ?res rp::?rp-state-res)
        (svexlist-simplify-fn svexlist state rp-state
                              context runes reload-rules linearize
                              only-local vars-are-integer verbose)))
    (valid-rp-state-syntaxp rp::rp-state-res)))
 :rule-classes :rewrite)