MS91-INTERLEAVE : FLAGMS91-INTERLEAVE is a flag or parameter.
In MS91-*, primitive substitutions are generated by NAME-PRIM,
and they are applied to the master eproof before the search mechanism
chooses particular parts of that eproof (and hence particular
substitutions) to try and prove.
If MS91-INTERLEAVE is NIL, all of the substitutions generated by NAME-PRIM
are applied at once, and then the search mechanism chooses among them, probably
in the order in which they were generated. The process of applying them to
the eproof can take a very long time.
If MS91-INTERLEAVE is an integer n, we take n primsubs at a time for each
variable which has primsubs, and apply only those to the eproof. Once we
have searched through those (to be specific, once we decide to generate new
options), we take the next n primsubs for each variable and apply them,
and so on. This is much quicker, and has the advantage of not having to
work through every primsub for the first variable before starting work on
the next variable.
If MS91-INTERLEAVE is non-NIL, and NEW-OPTION-SET-LIMIT is greater than
MS91-INTERLEAVE * (# of vars that have primsubs), then TPS will reduce
NEW-OPTION-SET-LIMIT. This ensures that single substitutions are
generated before multiple substitutions.
MS91-INTERLEAVE takes values of type NULL-OR-POSINTEGER.
It belongs to subjects PRIMSUBS MS91-7 MS91-6 .
Its default value is 5
Its current value is 5.
TPS documentation homepage