|
|
|---|
|
|
|
|---|
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 't)
(vars-are-integer 't)
(verbose 'nil)
(svex-env-is-var '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. Variables should correspond to the svex variable names.
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. It is recommended to use this option for slow simplify operations. This can be nil, t, or a natural number. When a number is given, it will dive deeper into that many levels of repeated nodes. The higher the number, the better simplification. However, the program might slow down a lot with a high number.
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 (RP 'INTEGERP X) '0 '1) (4VEC-CONCAT$ '1 (BITS (RP 'INTEGERP Y) '0 '1) (BITS (RP 'INTEGERP Z) '0 '1))) <rp-state>)
Users also might add rewrite rules to help simplification. For example:
(progn (defthm 4vec-bitand-of-4vec-?-with-shared-var (implies (integerp x) (equal (sv::4vec-bitand x (sv::4vec-? x y z)) (sv::4vec-bitand x y)))) (svl::add-svex-simplify-rule 4vec-bitand-of-4vec-?-with-shared-var))
Function:
(defun svex-simplify-fn (svex state rp-state context runes reload-rules linearize only-local vars-are-integer verbose svex-env-is-var) (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. Make sure you are giving a translated term ~%"))) :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)) (rp-state (rp::update-rw-stack nil rp-state)) ((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 :svex-env-is-var svex-env-is-var)) (- (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-env-is-var))) (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 svex-env-is-var))) (valid-rp-state-syntaxp rp::rp-state-res))) :rule-classes :rewrite)