		Search-engine friendly clone of the ACL2 documentation.

Gl-mbe

Gl-mbe-fast

Like gl-mbe, but faster and without error checking during execution.

See gl-mbe for background. (gl-mbe-fast spec exec) is logically identical to gl-mbe and should have exactly the same effect during symbolic execution. However, gl-mbe-fast may run more quickly during concrete execution, at the cost of some error checking.

In particular, for ordinary, concrete execution, a (gl-mbe spec impl) form requires both the spec and impl forms to be evaluated and checked for equality. In contrast, gl-mbe-fast is essentially a macro that expands to:

(mbe :logic (gl-mbe spec exec)
     :exec spec)

The guard proof you will incur should be trivial because gl-mbe always just logically returns spec.

Aside from performance, this behaves differently than gl-mbe in the degenerate case where your spec and exec forms produce different results. For example:

(defun test1 (x y) (declare (xargs :guard t)) (gl-mbe x y))
(defun test2 (x y) (declare (xargs :guard t)) (gl-mbe-fast x y))

(test1 3 7)   --> causes a hard error
(test2 3 7)   --> no error, returns 3