ACL2::always-equal
Alias for equal that has a special meaning in gl-bdd-mode.
- Signature
(acl2::always-equal x y) → *
Logically this is just equal, but gl treats
always-equal in a special way.
Suppose GL is asked to prove (equal spec impl) when this does not
actually hold. Sometimes, the symbolic objects for spec and impl can be
created, but the BDD representing their equality is too large to fit in memory.
This stops you from seeing any counterexamples, even though GL knows that the
two objects aren't equal.
To work around this, you may restate your theorem using always-equal
instead of equal as the final comparison. always-equal has a custom
symbolic counterpart that returns t when its arguments are equivalent, or
else produces a symbolic object that captures just one counterexample and is
indeterminate in all other cases.
Note that there is not really any reason to use always-equal if you are
using an AIG-based GL mode, such as gl-satlink-mode.
Definitions and Theorems
Function: always-equal
(defun acl2::always-equal (x y)
(declare (xargs :guard t))
(let ((__function__ 'acl2::always-equal))
(declare (ignorable __function__))
(equal x y)))
