|
|
|---|
|
|
|
|---|
Try to simplify an sv::svex structure with ACL2::rp-rewriter using regular rewrite rules about 4vec functions.
(svex-simplify svex &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)A given sv::svex is converted to its equivalent representation with 4vec functions, and they are rewrittern with existing rewrite rules using RP-Rewrtier. Finally, the resulting term is converted back to its equivalent SVEX form. Including this book already comes with a library of rewrite rules to simplify 4vec-functions. Users may choose to change this rewriting scheme by adding or disabling rewrite rules. The arguments of svex-simplify are:
context: a list of known facts. The terms should be tanslated. The variables in the given svex will appear in the term as (svl::svex-env-fastlookup-wog 'var svl::svex-env).
runes: List of rune names that will be used to rewrite 4vec functions. If nil, RP-Rewriter's rule-set will be used.
linearize: It can be either t, nil or :auto (default value). For very big SVEX structures with a lot of shared structures, we may use this linearize option to prevent repeated rewriting of the same structure. Linearize uses svexl structure to convert svexes to svexl, and rewrite this smaller structure. It also performs local simplification of the nodes in svexl that may also prove additional performance benefits for some aggressive rules. The :auto setting will enable linearize if SVEX is bigger than a certain size.
only-local: this option is only relevant when SVEX is linearized. Only the local nodes in SVEXL will be simplified.
Example Use:
(defconst *test-svex* '(sv::partsel 0 3 (sv::zerox 4 (sv::concat 3 (sv::concat 2 (sv::concat 1 x y) z) k)))) ;; This call will return an equivalent expression for *test-svex* (svl::svex-simplify *test-svex*) ;; Returned value: '(CONCAT 1 (PARTSEL 0 1 X) (CONCAT 1 (PARTSEL 0 1 Y) (PARTSEL 0 1 Z))) ;; If you would like to see from what 4vec term this SVEX is generated, you may ;; also run svl::svex-simplify-to-4vec (svl::svex-simplify-to-4vec *test-svex*) ;; Returned value '(4VEC-CONCAT$ '1 (BITS (SVEX-ENV-FASTLOOKUP-WOG 'X (RP 'SVEX-ENV-P SVEX-ENV)) '0 '1) (4VEC-CONCAT$ '1 (BITS (SVEX-ENV-FASTLOOKUP-WOG 'Y (RP 'SVEX-ENV-P SVEX-ENV)) '0 '1) (BITS (SVEX-ENV-FASTLOOKUP-WOG 'Z (RP 'SVEX-ENV-P SVEX-ENV)) '0 '1)))
Function:
(defun svex-simplify-fn (svex state rp-state context runes reload-rules linearize only-local vars-are-integer verbose) (declare (xargs :stobjs (state rp-state))) (declare (xargs :guard (and (svex-p svex) (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__ 'svex-simplify)) (declare (ignorable acl2::__function__)) (b* ((linearize (if (eq linearize ':auto) (zp (cons-count-compare svex 2048)) linearize)) ((mv rw rp-state) (svex-simplify-to-4vec svex :state state :context context :runes runes :reload-rules reload-rules :linearize linearize :only-local only-local :vars-are-integer vars-are-integer :verbose verbose)) (- (clear-memoize-table '4vec-to-svex)) ((mv err svex-res) (if only-local (locally-simplified-to-svex rw) (4vec-to-svex rw nil linearize))) (- (and err (hard-error 'svex-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 svex-res rp-state))))
Theorem:
(defthm svex-p-of-svex-simplify.res (b* (((mv ?res rp::?rp-state-res) (svex-simplify-fn svex state rp-state context runes reload-rules linearize only-local vars-are-integer verbose))) (svex-p res)) :rule-classes :rewrite)
Theorem:
(defthm valid-rp-state-syntaxp-of-svex-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) (svex-simplify-fn svex 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)