		Search-engine friendly clone of the ACL2 documentation.

Symbolic-test-vectors

Stv-easy-bindings

Generating G-bindings from an STV in a particular way.

Signature
(stv-easy-bindings stv order) → *
Arguments: stv — The STV you are dealing with.
Guard (processed-stv-p stv).; order — The variable order you want to use.

(stv-easy-bindings stv order) is a macro for proving theorems about symbolic-test-vectors using gl. It returns a list of G-bindings for use with def-gl-thm. That is, you can write something like:

(def-gl-thm foo
   ...
   :g-bindings
   (stv-easy-bindings (my-stv) '(opcode size special (:mix a b) c)))

This is probably only useful when:

You are using GL in BDD mode, not some AIG or SAT based mode.
You are running into performance problems when using the default -autobinds from the defstv.
You want to see if a different variable order performs better.

To use stv-easy-bindings, you just list (a subset of) the STV inputs in priority order. For instance, in the above example, the opcode will get the smallest indices, then size next, etc. You do not have to list all of the STV variables. Any unmentioned variables will be assigned indices after mentioned variables.

As in gl::auto-bindings, you can also use (:mix a b c ...) to interleave the bits of a, b, c, ...; note that for this to work these variables must all share the same width. This is generally useful for data buses that are going to be combined together.

An especially nice feature of easy-bindings is that they automatically adjust when inputs to the STV are resized, when new inputs are added, and when irrelevant inputs are removed.

Definitions and Theorems

Function: stv-easy-bindings

(defun stv-easy-bindings (stv order)
  (declare (xargs :guard (processed-stv-p stv)))
  (let ((__function__ 'stv-easy-bindings))
    (declare (ignorable __function__))
    (b* ((binds (stv-easy-bindings-main order stv))
         (unbound (set-difference-equal (stv->ins stv)
                                        (pat-flatten1 binds))))
      (gl::auto-bindings-fn
           (append binds
                   (stv-easy-bindings-inside-mix unbound stv))))))

Subtopics

Stv-easy-bindings-inside-mix