Ccg-xargs
Giving hints to CCG analysis via See xargs
In addition to the xargs provided by ACL2 for passing hints to function definitions, the CCG analysis enables several others for
guiding the CCG termination analysis for a given function definition. The
following example is nonsensical but illustrates all of these xargs:
(declare (xargs :termination-method :ccg
:consider-ccms ((foo x) (bar y z))
:consider-only-ccms ((foo x) (bar y z))
:ccg-print-proofs nil
:time-limit 120
:ccg-hierarchy *ccg-hierarchy-hybrid*))
General Form:
(xargs :key1 val1 ... :keyn valn)
Where the keywords and their respective values are as shown below.
Note that the :TERMINATION-METHOD xarg is always valid, but the other
xargs listed above are only valid if the termination method being used
for the given function is :CCG.
:TERMINATION-METHOD value
Value here is either :CCG or :MEASURE. For details on the
meaning of these settings, see the documentation for set-termination-method. If this xarg is given, it overrides the global
setting for the current definition. If the current definition is part of a
mutual-recursion, and a :termination-method is provided, it must
match that provided by all other functions in the mutual-recursion.
:CONSIDER-CCMS value or :CONSIDER-ONLY-CCMS value
Value is a list of terms involving only the formals of the function being
defined. Both suggest measures for the current function to the CCG
analysis. ACL2 must be able to prove that each of these terms always evaluate
to an ordinal see ordinals. ACL2 will attempt to prove this before
beginning the CCG analysis. The difference between :consider-ccms and
:consider-only-ccms is that if :consider-ccms is used, the CCG
analysis will attempt to guess additional measures that it thinks might be
useful for proving termination, whereas if :consider-only-ccms is used,
only the measures given will be used for the given function in the CCG
analysis. These two xargs may not be used together, and attempting to do
so will result in an error.
:CCG-PRINT-PROOFS value
Value is either t or nil. This is a local override of the
set-ccg-print-proofs setting. See this documentation topic for
details.
:TIME-LIMIT value
Value is either a positive rational number or nil. This is a local
override of the set-ccg-time-limit setting. See this documentation
topic for details.
:CCG-HIERARCHY value
Value is a CCG hierarchy. This is a local override of the set-ccg-hierarchy setting. See this documentation topic for details.
