Fgl-vacuity-check
Check that the given object is satisfiable and report an error if not.
- Signature
(fgl-vacuity-check params x) → *
- Arguments
- params — Parameters for the SAT check -- depending on the
attachment for the pluggable checker.
- x — Object to check for vacuity.
Logically, (fgl-vacuity-check params x) just returns x fixed to a
Boolean value. But when FGL symbolic execution encounters an
fgl-vacuity-check term, it checks Boolean satisfiability of x and if
it is able to prove that all evaluations of x are NIL, then it produces an
error; otherwise, it returns x unchanged. This is useful for checking that
the hypotheses of a conjecture aren't contradictory.
Definitions and Theorems
Function: fgl-vacuity-check
(defun fgl-vacuity-check (params x)
(declare (ignore params))
(declare (xargs :guard t))
(let ((__function__ 'fgl-vacuity-check))
(declare (ignorable __function__))
(if x t nil)))
