# 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.