		Search-engine friendly clone of the ACL2 documentation.

Smtlink

Tutorial

A tutorial to walk you through how to use Smtlink to prove ACL2 theorems.

Prerequisites

Following instructions in :doc Smtlink, one should have setup the configuration in file smtlink-config and have certified the Smtlink book afterwards to bake in the configurations.

Then the header of the ACL2 script should look like:

(in-package "ACL2")
(include-book "projects/smtlink/top" :dir :system)
(tshell-ensure)

Smtlink uses a sequence of computed hints and clause processors to perform different stages. 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.

The rest of this document contains four pieces of arithmetic examples to show what one can do with Smtlink and how. The first one shows a regular example, the second one is proved using the extended version called smtlink-custom, the third one is a theorem that does not pass Smtlink, and the fourth is a list of examples for FTY types.

Subtopics

Fty-examples: A list of FTY examples
Example-2: Example 2: something wild
Example-1: Example 1: the basics
Maybe-integer: Option type; ACL2::int or nil.
Example-3: Example 3: defense against evil