Minimum depth at which primsubs with quantifiers are generated.

The types of the quantified variables range over the values in PRIM-BDTYPES.

With PRIMSUB-METHOD PR89 :

This flag is ignored. Primsubs of the form "exists x . literal" and

"forall x . literal" will be generated.

With PRIMSUB-METHOD PR93 :

At depth 1, a single quantifier is introduced, as in PR89.

At depth N>1, we have (N-1) quantifiers ranging over a formula

containing (N-1) conjunctions {disjunctions} of (N-2)

disjunctions {conjunctions}.

With PRIMSUB-METHOD PR95 :

At depth 1, as in PR89.

At depth N>1, we have (N-1) quantifiers ranging over a formula

with between MIN-PRIM-LITS and MAX-PRIM-LITS literals, with

all combinations of connectives between them.

With PRIMSUB-METHOD PR97 :

At depth N>0, we have (N-1) quantifiers ranging over each

subformula taken from the etree which contains between

MIN-PRIM-LITS and MAX-PRIM-LITS literals. You can see these

subformulas by doing NAME-PRIM from the MATE top level.

With PRIMSUB-METHOD PR97A :

As in PR97, but all substitutions are in negation normal form.

With PRIMSUB-METHOD PR97B :

The substitutions from PR97A and PR95 are interleaved. The order

is determined firstly by the number of literals, then by the number of

quantifiers, and lastly with PR97 substs taking precedence over PR95.

With PRIMSUB-METHOD PR97C :

If set to N, the number of quantifiers in any primsub will be >= N-1.

MIN-PRIM-DEPTH takes values of type POSINTEGER.

It belongs to subjects IMPORTANT MS93-1 MS92-9 MS91-7 MS91-6 MS90-9 MS90-3 MS89 MS88 PRIMSUBS .

Its default value is 1

Its current value is 1.

© 1988-99, Carnegie Mellon University.