FIND-BEST-MODE : TESTCMD

FIND-BEST-MODE is a test-top command.
This command effectively runs PUSH-UP until it finds
a mode that works, and then runs PRESS-DOWN until it finds the
best mode it can.
Before using this command, use the MODE command to
set up a mode in which the current theorem can not be proven. Also
check the value of the TEST-INCREASE-TIME flag (it should probably
not be zero).
Then PUSH-UP will systematically vary the values of the flags
listed in the TEST-EASIER-IF-* flags, using the PUSH-UP search
function (see the help message for TEST-NEXT-SEARCH-FN).
Once a correct mode is discovered, it will systematically vary
the values of the flags listed in the TEST-FASTER-IF-* flags,
using the PRESS-DOWN search function, until it finds as good a
mode as it can.
The values of TEST-REDUCE-TIME, TEST-NEXT-SEARCH-FN,
TEST-INCREASE-TIME and TEST-FIX-UNIF-DEPTHS will be permanently
changed.
 
The command format for FIND-BEST-MODE is:

<TEST>FIND-BEST-MODE MODENAME TESTWIN
"SYMBOL" "YESNO"

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage