		Search-engine friendly clone of the ACL2 documentation.

Smt-hint

Describes the hints interface for Smtlink.

Examples:

:smtlink(-custom)
(:functions ((my-expt :formals ((r rationalp)
                                (i rationalp))
                      :returns ((ex rationalp :hints (:in-theory (enable my-expt))))
                      :level 0)
             ...)
 :hypotheses (((< (my-expt z n) (my-expt z m))
               :hints (:use ((:instance hypo1-hint (x x)))))
              ((< 0 (expt z m)))
              ((< 0 (expt z n)))
              ...)
 :fty (acl2::integer-list)
 :main-hint (:use ((:instance main-hint (n n) (x x))))
 :int-to-rat t
 :smt-fname "my-smt-problem.lisp"
 :smt-dir "/home/tmp"
 :rm-file t)

:smtlink is a customized argument option to ACL2::hints. smtlink-custom is used when one wants to use the customized version of Smtlink. The next argument to :smtlink we call smt-hint. These are the hints one wants to provide to Smtlink so that it can figure out the proof easily. Let's take a look at each one of them:

:functions

functions are for dealing with recursive functions. Smtlink translate a basic set of ACL2 functions (See smt-basics) into SMT functions. Non-recursive functions defined with the basic functions are automatically expanded in the verified clause processor. Recursive functions can be specified to expand to a given level. The innermost function call is translated into an uninterpreted function. When level equals 0, no expansion is done.

The argument to :functions is a list of functions. For each of the function, for example,

(my-expt :formals ((r rationalp)
                   (i rationalp))
         :returns ((ex rationalp :hints (:in-theory (enable my-expt))))
         :level 0)

my-expt is function that has already been defined. It has two formals, named as r with type rationalp and i with type rationalp. It returns an argument called ex with type rationalp. Return types of functions are proved as one of the clauses returned by the verified clause processor. One can give hints to the proof. The hints uses a similar form as in ACL2::hints. The only difference is that the hints will only go to a specific subgoal, therefore no goal specifier is needed. level is the expansion level.

:hypotheses

:hypotheses are "facts" that the user believes to be true and should help with the proof. The facts will be returned as auxiliary clauses to be proved from the verified clause processor. One can provide hints for proving any of the hypotheses. It follows the format of the ACL2::hints, except that no goal specifier is needed.

:fty

:fty specifies a list of FTY types to be used in this theorem

:main-hint

:main-hint provides a hint to the main returned auxiliary theorem. This theorem proves the expanded clause implies the original clause. The format of the hint follows that of the ACL2::hints, except that no goal specifier is needed.

:int-to-rat

Z3 has a limited solver for mixed Integer and Real number theories, but have a better solver for solving pure Real number problems. Sometimes one might want to try raising all Integers to Reals to prove a theorem.

:smt-fname

:smt-fname provides a user specified file name for the generated Z3 problem, instead of the default one.

:smt-dir

:smt-dir provides a user specified directory for the generated Z3 file, instead of the default one in /tmp.

:rm-file

:rm-file specified whether one wants the generated Z3 file to be preserved, in default case, it is removed.