		Search-engine friendly clone of the ACL2 documentation.

Logical-story

Satlink-run

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

Function: satlink-run

(defun satlink-run (config formula env$)
  "Returns (MV STATUS ENV$ LRAT-PROOF)"
  (declare (xargs :stobjs env$
                  :guard (and (config-p config)
                              (lit-list-listp formula))))
  (satlink-run-fn config formula env$))