Describes the hints interface for Smtlink.
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
The argument to :functions is a list of functions. For each of the
function, for example,
(my-expt :formals ((r rationalp)
:returns ((ex rationalp :hints (:in-theory (enable my-expt))))
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
: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 specifies a list of FTY types to be used in this
: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.
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 provides a user specified file name for the generated
Z3 problem, instead of the default one.
:smt-dir provides a user specified directory for the generated Z3
file, instead of the default one in /tmp.
:rm-file specified whether one wants the generated Z3 file to be
preserved, in default case, it is removed.