		Search-engine friendly clone of the ACL2 documentation.

Satlink

Satlink-extra-hook

An attachable hook for performing extra actions after successful calls of the SAT solver.

This is an advanced feature for Satlink hackers.

(satlink-extra-hook cnf filename status env$ state) is an attachable function (see defattach) that is called by satlink-run-impl after successful invocations of the SAT solver.

The default hook does nothing, but you may be able to implement custom hooks that do useful things. For instance, the gather-benchmarks hook can be used to automatically collect up the DIMACS files for Satlink problems. These kinds of hooks might require additional trust tags, so it is nice to keep them out of Satlink itself.

A hook can access several arguments:

cnf is the formula we were trying to solve.
filename is the name of the temporary input file that was given to the SAT solver. At the time the hook is invoked, the file should still exist, even when we are removing temporary files.
status says whether the SAT solver returned :sat or :unsat. Note that you don't have to consider :failed because the hook does not get invoked in that case.
env$ is the satisfying assignment in case of :sat answers.
state is the usual ACL2 state, which might be useful for sending some extra information to your hook, e.g., state globals or similar.

Definitions and Theorems

Theorem: state-p1-of-satlink-extra-hook

(defthm state-p1-of-satlink-extra-hook
 (implies
    (state-p1 state)
    (state-p1 (satlink-extra-hook cnf filename status env$ state))))

Function: default-satlink-hook

(defun default-satlink-hook (cnf filename status env$ state)
  (declare (xargs :stobjs (env$ state)))
  (declare (xargs :guard (and (lit-list-listp cnf)
                              (stringp filename)
                              (or (eq status :sat)
                                  (eq status :unsat)))))
  (declare (ignorable cnf filename status env$ state))
  (let ((__function__ 'default-satlink-hook))
    (declare (ignorable __function__))
    state))

Theorem: state-p1-of-default-satlink-hook

(defthm state-p1-of-default-satlink-hook
 (implies
   (state-p1 state)
   (b*
     ((state (default-satlink-hook cnf filename status env$ state)))
     (state-p1 state)))
 :rule-classes :rewrite)