Connection between the implementation and the logical story.
In the logic, this function does nothing more than call
satlink-run-fn, the constrained function that is the basis of our logical-story.
Under the hood, through a trust tag, we smash its definition and have it
invoke satlink-run-impl, which actually calls the SAT solver.
Definitions and Theorems
(defun satlink-run (config formula env$)
"Returns (MV STATUS ENV$ LRAT-PROOF)"
(declare (xargs :stobjs env$
:guard (and (config-p config)
(satlink-run-fn config formula env$))