Smtlink
Tutorial and documentation for the ACL2 book, Smtlink.
Introduction
A framework for integrating external SMT solvers into ACL2 based on the
ACL2::clause-processor and the ACL2::computed-hints
mechanism.
Overview
Smtlink is a framework for representing suitable ACL2 theorems as a SMT
(Satisfiability Modulo Theories) formula, and calling SMT solvers from within
ACL2.
SMT solvers combine domain-specific techniques together into a SAT
(Satisfiability) Solver and solves domain-specific satisfiability problems.
Typical domain specific procedures include procedures in integer and real,
linear and non-linear arithmetic, array theory, and uninterpreted function
theory. Modern SMT solvers benefit from the development of both the SAT
solvers and the domain-specific techniques and have become very fast at solving
some relatively large problems.
In the 2018 Workshop version, we call it smtlink 2.0, we make major
improvements over the initial version with respect to soundness, extensibility,
ease-of-use, and the range of types and associated theory-solvers supported.
Most theorems that one would want to prove using an SMT solver must first be
translated to use only the primitive operations supported by the SMT solver --
this translation includes function expansion and type inference. Smtlink
2.0 performs this translation using sequence of steps performed by verified
clause processors and computed hints. These steps are ensured to be sound.
The final transliteration from ACL2 to Z3's Python interface requires a trusted
clause processor. This is a great improvement in soundness and extensibility
over the the original Smtlink which was implemented as a single,
monolithic, trusted clause processor. Smtlink 2.0 provides support for
ACL2::fty, defprod, deflist, defalist, and defoption types by using Z3's arrays and user
defined data types.
Smtlink can be used both in ACL2 and ACL2(r). The macro Real/rationalp should make one's proof portable between ACL2 and ACL2(r). It
is also compatible with both Python 2 and Python 3.
Smtlink currently only supports Z3. We hope to add an interface
to include the SMT-LIB in near
future.
Using Smtlink
Requirements
- Python 2/3 is properly installed.
- Z3 is properly installed.
One needs to build Z3 on one's own instead of using the binary release.
Also, since we are using the Python interface, please follow the "python"
section in the "z3 bindings" section in README of Z3.
I've also wrote a small piece of z3-installation document about how
to install Z3 and its Python API.
To check if Z3 is properly installed, run Python, which will put you in an
interactive loop. Then run:
from z3 import *
x = Real('x')
y = Real('y')
s = Solver()
s.add(x + y > 5, x > 1, y > 1)
print(s.check())
print(s.model())
quit()
One should expect some results like:
>>> print(s.check())
sat
>>> print(s.model())
[y = 4, x = 2]
- ACL2 and the system books are properly installed.
- Smtlink uses Unix commands.
Build Smtlink
- Setup smtlink configuration in file smtlink-config in either a user
specified directory $SMT_HOME or in directory $HOME. When both
environment variables are set, $SMT_HOME is used. The configuration takes
below format:
smt-cmd=...
NOTE:
It used to be four options, we simplified it into just one smt-cmd.
smt-cmd is the command for running Z3, which is the Python command
since we are using the Python interface. The Z3 library is imported into Python
in the scripts written out by Smtlink like is shown in the example script in
"Requirements".
- Certify the book top.lisp in the Smtlink directory, to bake setup into
certified books.
This took about 8 mins on my 4-core mac with hyperthreading -j 2.
NOTE:
A complete recertification of Smtlink is required if one changes the
configuration in smtlink-config.
Load and Setup Smtlink
To use Smtlink, one needs to include book:
(include-book "projects/smtlink/top" :dir :system)
Then one needs to enable ACL2::tshell by doing:
(value-triple (tshell-ensure))
value-triple makes sure the form (tshell-ensure) can be
submitted in an event context and therefore is certifiable.
In order to install the computed-hint, one needs to
add-default-hints.
(add-default-hints '((SMT::SMT-computed-hint clause)))
NOTE:
The computed-hint used to be called SMT::SMT-process-hint, we find this name
doesn't represent what it does. We changed the name to
SMT::SMT-computed-hint.
For a detail description of how to setup and get started using Smtlink,
see tutorial and SMT-hint.
Reference
Smtlink has experienced a great interface and infrastructure change
since its first publication at ACL2 workshop 2015. But you may still find below
paper useful in understanding basics of Smtlink:
Yan Peng and Mark R. Greenstreet. Extending ACL2 with SMT SolversIn
ACL2 Workshop 2015. October 2015. EPTCS 192. Pages 61-77.
Subtopics
- Z3-installation
- How to install Z3
- Smt-hint
- Describes the hints interface for Smtlink.
- Tutorial
- A tutorial to walk you through how to use Smtlink to prove ACL2 theorems.
- Status
- A discussion of what theories are supported in Smtlink and what we
intend to support in the future.
- Developer
- The developer's reference to Smtlink.
