Abs-diff
(abs-diff a b) is just (abs (- (ifix a) (ifix b))), but
optimized for ACL2::gl.
- Signature
(abs-diff a b) → ans
- Arguments
- a — Guard (integerp a).
- b — Guard (integerp b).
- Returns
- ans — Type (natp ans).
abs-diff is similar to (abs (- a b)) but has better
performance for symbolic simulations with GL: it decides whether the
subtraction will be necessary by looking at the arguments, which tend to be
simple and perhaps nicely interleaved, instead of by looking at the result,
which tend to be complex since they are the combined arguments.
For an aig-cert-mode proof of the 64-bit PSADBW instruction, using
abs-diff instead of (abs (- a b)) reduced the proof time from 56.2
seconds to 37.44 seconds.
We disable this function, but we leave enabled the following theorem:
Theorem: abs-diff-correct
(defthm abs-diff-correct
(equal (abs-diff a b)
(abs (- (ifix a) (ifix b)))))
We therefore would not expect to ever need to reason about abs-diff
directly.
Definitions and Theorems
Function: abs-diff
(defun abs-diff (a b)
(declare (xargs :guard (and (integerp a) (integerp b))))
(let ((__function__ 'abs-diff))
(declare (ignorable __function__))
(mbe :logic
(let ((a (ifix a)) (b (ifix b)))
(if (<= b a) (- a b) (- b a)))
:exec (if (<= b a) (- a b) (- b a)))))
Theorem: natp-of-abs-diff
(defthm acl2::natp-of-abs-diff
(b* ((ans (abs-diff a b))) (natp ans))
:rule-classes :type-prescription)
Theorem: abs-diff-correct
(defthm abs-diff-correct
(equal (abs-diff a b)
(abs (- (ifix a) (ifix b)))))
