Generating G-bindings from an SVTV in a particular way.
(svtv-easy-bindings svtv order) → *
(svtv-easy-bindings svtv order) is a macro for proving theorems about symbolic-test-vectors using gl. It returns a list of G-bindings for use with ACL2::def-gl-thm. That is, you can write something like:
(def-gl-thm foo ... :g-bindings (svtv-easy-bindings (my-svtv) '(opcode size special (:mix a b) c)))
This is probably only useful when:
As in gl::auto-bindings, you can also use
An especially nice feature of easy-bindings is that they automatically adjust when inputs to the SVTV are resized, when new inputs are added, and when irrelevant inputs are removed.
(defun svtv-easy-bindings (svtv order) (declare (xargs :guard (svtv-p svtv))) (let ((__function__ 'svtv-easy-bindings)) (declare (ignorable __function__)) (b* ((binds (svtv-easy-bindings-main order svtv)) (unbound (set-difference-equal (svtv->ins svtv) (svtv-easy-bindings-svtv-vars order)))) (gl::auto-bindings-fn (append binds (svtv-easy-bindings-main unbound svtv))))))