Set-termination-method
Set the default means of proving termination.
Examples:
(set-termination-method :ccg)
(set-termination-method :measure)
Introduced by the CCG analysis book, this macro sets the default means by
which ACL2 will prove termination. Note: This is an event! It does not print
the usual event summary but nevertheless changes the ACL2 logical world
and is so recorded.
General Form:
(set-termination-method tm)
where tm is :CCG or :MEASURE. The default is :MEASURE
(chosen to assure compatibility with books created without CCG). The
recommended setting is :CCG. This macro is equivalent to (table
acl2-defaults-table :termination-method 'tm), and hence is local to
any books and encapsulate events in which it occurs; see
ACL2-defaults-table.
When the termination-method is set to :CCG, a termination proof is
attempted using the the hierarchical CCG algorithm CCG-hierarchy.
When the termination-method is set to :MEASURE, ACL2 attempts to prove
termination using its default measure-based method. Thus, in this setting,
ACL2's behavior is identical to that when the CCG book is not included at
all.
To see what the current termination method setting is, use get-termination-method.
