Are existential quantifiers nested under foralls skolemised once? What do quantifier instantiation statistics mean for these quantifiers?

2
votes

In a (rather large) Z3 problem, we have a few axioms of the shape:

forall xs :: ( (P(xs) ==> (exists ys :: Q(xs,ys))) && ((exists zs :: Q(xs,zs)) ==> P(xs)) )

All three quantifiers (including the existentials) have explicit triggers provided (omitted here). When running the problem and gathering quantifier statistics, we observed the following data (amongst many other instantiations):

[quantifier_instances] k!244 : 804 : 3 : 4 [quantifier_instances] k!232 : 10760 : 29 : 30

Here, line 244 corresponds to the end of the outer forall quantifier, and line 232 to the end of the first inner exists. Furthermore, there are no reported instantiations of the second inner exists (which I believe Z3 will pull out into a forall); given the triggers this is surprising.

My understanding is that existentials in this inner position should be skolemised by a function (depending on the outer quantifier). It's not clear to me what quantifier statistics mean for such existentials.

Here are my specific questions:

  1. Are quantifier statistics meaningful for existential quantifiers (those which remain as existentials - i.e. in positive positions)? If so, what do they mean?
  2. Does skolemisation of such an existential happen once and for all, or each time the outer quantifier is instantiated? Why is a substantially higher number reported for this quantifier than for the outer forall?
  3. Does Z3 apply some internal rewriting of this kind of (A==>B)&&(B==>A) assertion? If so, how does that affect quantifier statistics for quantifiers in A and B?

From our point of view, understanding question 2 is most urgent, since we are trying to investigate how the generated existentials affect the performance of the overall problem.

The original smt file is available here: https://gist.github.com/anonymous/16e489ce5c513e8c4bc6 and a summary of the statistics generated (with Z3 4.4.0, but we observed the same with 4.3.2) is here: https://gist.github.com/anonymous/ce7b96acf712ac16299e

1
z3

1 Answers

0
votes

The answer to all these questions is 'it depends', mainly on what else appears in the problem and what options are set. For instance, if there are only bit-vector variables, then Skolemization will indeed be performed during preprocessing, once and forall, but this is not the case for all other theories or theory combinations.

Briefly looking at your SMT2 file, it seems to me that all existentials appear in the left hand side of implications, i.e., they are in fact negated (and actually rewritten into universals somewhere along the line), so those statistics do make sense for the existentials appearing in this particular problem.