		Search-engine friendly clone of the ACL2 documentation.

Advanced-equivalence-checking-with-fgl

Solve-lane-by-lane

Equality check that, in FGL, splits an equivalence of SIMD packed integers into lane-by-lane equivalence checks.

Signature
(solve-lane-by-lane x y width) → *

The equivalence check of each of the lanes is done using the FGL SAT config object (solve-lane-by-lane-config), which is an attachable function. Its default attachment uses SATLINK in the default configuration with transforms.

Definitions and Theorems

Function: solve-lane-by-lane

(defun solve-lane-by-lane (x y width)
  (declare (xargs :guard t))
  (let ((__function__ 'solve-lane-by-lane))
    (declare (ignorable __function__))
    (equal x y)))

Theorem: solve-lane-by-lane-impl

(defthm solve-lane-by-lane-impl
 (implies
  (and (syntaxp (posp width))
       (check-integerp xintp x)
       (check-integerp yintp y))
  (equal
   (solve-lane-by-lane x y width)
   (if (and (check-int-endp x-endp x)
            (check-int-endp y-endp y))
       (equal x y)
     (b*
      ((config
            (syntax-bind config
                         (g-concrete (solve-lane-by-lane-config)))))
      (and* (fgl-validity-check config
                                (equal (loghead width x)
                                       (loghead width y)))
            (solve-lane-by-lane (logtail width x)
                                (logtail width y)
                                width)))))))