An ACL2s Interface to Z3

TL;DR

Lisp-Z3 is an extension that enables Common Lisp programs to seamlessly interact with the Z3 SMT solver, enhancing theorem proving and solving capabilities within the ACL2s framework.

Contribution

It introduces Lisp-Z3, a novel interface allowing integration of Z3 with Common Lisp and ACL2s, supporting diverse applications without dependency on ACL2s availability.

Findings

Lisp-Z3 successfully integrated Z3 with ACL2s and Common Lisp.

Applications demonstrated include a Sudoku solver, a string solver, and hardware-in-the-loop fuzzing.

Lisp-Z3 improved problem-solving efficiency and enabled new automated reasoning capabilities.

Abstract

We present Lisp-Z3, an extension to the ACL2s systems programming framework (ASPF) that supports the use of the Z3 satisfiability modulo theories (SMT) solver. Lisp-Z3 allows one to develop tools written using the full feature set of Common Lisp that can use both ACL2/s (either ACL2 or ACL2s) and Z3 as services, combining the power of SMT and interactive theorem proving. Lisp-Z3 is usable by anyone who would like to interact with Z3 from Common Lisp, as it does not depend on the availability of ACL2/s. We discuss the use of Lisp-Z3 in three applications. The first is a Sudoku solver. The second is SeqSolve, a string solver which solved a larger number of benchmark problems more quickly than any other existing solver at the time of its publishing. Finally, Lisp-Z3 was also used in the context of hardware-in-the-loop fuzzing of wireless routers, where low latency was an important goal. The latter two applications leveraged the ability of Lisp-Z3 to integrate Z3 with ACL2s code. We have further plans to use Lisp-Z3 inside of ACL2s to provide more powerful automated support for dependent types, and in particular more efficient generation of counterexamples to properties involving dependent types. This paper describes the usage and implementation of Lisp-Z3, as well as an evaluation of its use in the aforementioned applications.