		Search-engine friendly clone of the ACL2 documentation.

Advanced-equivalence-checking-with-fgl

Top-level-equal

An alias for EQUAL. Useful if you want to prove an equality in FGL using a particular strategy.

Signature
(top-level-equal x y) → *

Sometimes if you're proving an equivalence of two objects using FGL/SAT/bitblasting, it's advantageous to use a strategy other than just checking satisfiability of the negation of the top-level equivalence. For example, in proving the correctness of SIMD implementations where you're proving equivalence of two wide integers composed of packed arithmetic results, you might want to instead prove each of the lanes separately. We can use an FGL rewrite rule to rewrite the top-lvel equal call to an alias that has a rewriting strategy to solve it with this scheme. But we don't want to rewrite all calls of equal this way! Instead, we suggest an alternate strategy:

Locally introduce a rule rewriting (top-level-equal x y) to the function implementing your special solving strategy -- solve-lane-by-lane, for example.
Add a hint to your def-fgl-thm: :hints ('(:clause-processor replace-equal-with-top-level-equal))

The hint will replace only the equal call at the top level of your theorem with top-level-equal.

Definitions and Theorems

Function: top-level-equal

(defun top-level-equal (x y)
  (declare (xargs :guard t))
  (equal x y))

Subtopics

Replace-equal-with-top-level-equal: Clause processor that replaces the final call of equal in a theorem conclusion with top-level-equal.