Binary--
(binary-- x y) is the same as (- x y), but may symbolically
simulate more efficiently in gl.
- Signature
(binary-- x y) → *
- Arguments
- x — Guard (acl2-numberp x).
- y — Guard (acl2-numberp y).
This is an alias for (- x y). It should always be left
enabled and you should never prove any theorems about it.
In ACL2, - is a macro and (- x y) expands to (+ x (unary--
y)). This form is often not particularly good for symbolic simulation with
gl: GL first has to negate y and then carry out the addition.
In contrast, binary-- has a custom symbolic counterpart that avoids
this intermediate negation. This may result in fewer BDD computations or AIG
nodes. In the context of hardware-verification, it may also help your
spec functions to better match the real implementation of subtraction circuits
in the hardware being analyzed.
Definitions and Theorems
Function: binary--$inline
(defun binary--$inline (x y)
(declare (xargs :guard (and (acl2-numberp x)
(acl2-numberp y))))
(let ((__function__ 'binary--))
(declare (ignorable __function__))
(mbe :logic (binary-minus-for-gl x y)
:exec (- x y))))
Subtopics
- Binary-minus-for-gl
- Hack for implementing binary--. Don't use this.
