		Search-engine friendly clone of the ACL2 documentation.

Set-ccg-time-limit

Set a global time limit for CCG-based termination proofs.

Examples:
(set-ccg-time-limit 120)  ; limits termination proofs to 120 seconds.
(set-ccg-time-limit 53/2) ; limits termination proofs to 53/2 seconds.
(set-ccg-time-limit nil)  ; removes any time limit for termination proofs.

Introduced by the CCG analysis book, this macro sets a global time limit for the completion of the CCG analysis. The time limit is given as a rational number, signifying the number of seconds to which the CCG analysis should be limited, or nil, signifying that there should be no such time limit. If CCG has not completed its attempt to prove termination in the number of seconds specified, it will immediately throw an error and the definition attempt will fail. 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-ccg-time-limit tl)

where tl is a positive rational number or nil. The default is nil. If the time limit is nil, the CCG analysis will work as long as it needs to in order to complete the analysis. If the tl is a positive rational number, all CCG analyses will be limited to tl seconds.

To see what the current time limit is, see get-ccg-time-limit.