Calling ACL2 from another program
ACL2 is intended for interactive use. It is generally unrealistic to expect it to prove theorems fully automatically; see the-method, and see introduction-to-the-theorem-prover for a more detailed tutorial.
Nevertheless, here we describe an approach for how to call the ACL2 theorem prover noninteractively. These steps can of course be modified according to your needs. Here, we illustrate how to call ACL2 from another Lisp program (or an arbitrary program) to attempt to prove an arithmetic theorem.
See also interfacing-tools. In particular, if you want to make a command-line tool to ACL2 with options, you may be interested in oslib::argv, getopt, and especially getopt-demo::demo2. Alternately, if you want to develop a server application on top of ACL2, you might consider bridge.
Build a suitable ACL2 image by starting ACL2 and then executing the
following forms. In particular, these define a macro,
(include-book "arithmetic-5/top" :dir :system) (defmacro try-thm (&rest args) `(mv-let (erp val state) (with-prover-time-limit 3 (thm ,@args)) (declare (ignore val)) (prog2$ (if erp (exit 1) (exit 0)) state)))) (reset-prehistory) ; optional :q (save-exec "arith-acl2" "Included arithmetic-4/top")
If you prefer, above you can replace 3 by some other number of seconds as a time limit for the prover. Also, you can replace
(with-prover-time-limit 3 (thm ,@args))
(with-output :off :all (with-prover-time-limit 3 (thm ,@args)))
if you want to turn off output. It may be best to leave the output on, instead eliminating it in the calling program (see Step 3 below).
Try a little test. In that same directory try this:
echo '(try-thm (equal x x))' | ./arith-acl2 echo $?
The exit status should be 0, indicating success. Now try this:
echo '(try-thm (not (equal x x)))' | ./arith-acl2 echo $?
The exit status should be 1, indicating failure.
Create a shell script that automates Step 2, for example:
#!/bin/sh (echo "(try-thm $1)" | ./arith-acl2) >& /dev/null exit $?
Try your script from a Lisp program, if you like. Here is how you can do
it in SBCL, for example. (Different Lisps have different ways to do this, as
summarized in function
(defun provable? (x) (let ((status (process-exit-code (sb-ext:run-program "./try-thm.sh" (list (format nil "~s" x)) :output t :search t)))) (eql status 0)))
Then here is a log:
* (provable? '(equal x y)) NIL * (provable? '(equal x x)) T *
Certainly refinements are possible — for example the above doesn't distinguish between unprovable and ill-formed input. But it's a start.