I think Z3 is not performing quantifier elimination in a sequence instance

Consider the following Z3 definition of an array average function:

IntSeqSort = SeqSort(IntSort())

sumArray    = RecFunction('sumArray', IntSeqSort, IntSort())
sumArrayArg = FreshConst(IntSeqSort)

RecAddDefinition( sumArray
                , [sumArrayArg]
                , If(Length(sumArrayArg) == 0
                    , 0
                    , sumArrayArg[0] + sumArray(SubSeq(sumArrayArg, 1, Length(sumArrayArg) - 1))
                    )
                )

def avgArray(arr):
    return ToReal(sumArray(arr)) / ToReal(Length(arr))

Also, consider the following formula φ = (2<t<10) /\ ∃i. [(0 <= i <= |seq|) /\ (t+avg<seq[i])], which means that there is a position i in the sequence seq, such that seq[i] is greater than the average avg of seq plus a certain threshold t.

I translated this to Z3 as follows:

seq = Const('seq', SeqSort(IntSort()))
avg_seq = avgArray(seq)

t = Int('t')
y = Int('y')
x = Int('x')
i = Int('i') #Has to be declared, even if it is only used in the Existential

phi_0 = And(2<t, t<10)
phi_1 = And(0 <= i, i< Length(seq))
phi_2 = (t+avg_seq<seq[i])

phi_aux1 = And(phi_1, phi_2)

phi_aux2 = And(phi_0, Exists(i, phi_aux1))

Now, I want to know whether ∃[seq]∀[t].φ holds, so I model this in Z3 as follows:

phi = Exists([seq], ForAll([t],phi_aux2))

It responds no solution None. Which makes sense.

However, I decide to do quantifier elimination to check how is the resulting formula:

ta = Tactic("qe")
to_elim = Goal()
to_elim.add(phi)

phi_qe = ta(to_elim)
print(phi_qe)

Which responds as follows (it allocates different numbers when called several times):

[[Exists(x!746,
         Not(Exists(x!747,
                    Not(And(And(x!747 > 2, x!747 < 10),
                            Exists(x!748,
                                   And(And(x!748 >= 0,
                                        x!748 <
                                        Length(x!746)),
                                       ToReal(x!747) +
                                       ToReal(sumArray(x!746))/
                                       ToReal(Length(x!746)) <
                                       ToReal(Nth(x!746,
                                        x!748)))))))))]]

It is easy to identify that all the elements in this elimination are the same as the original element of φ: 746 is seq, 747 is t... So this has not performed QE!

My question is: why does this call not perform QE? Is this a bug? I mean, it should output a formula where the universally quantified t does not appear.

z3 tactics are a set of heuristics, and they perform a certain number of transformations on the goal. Tactics do not guarantee that they'll manage to do anything; different approaches lead to different outcomes. Consequently, z3 provides a bunch of quantifier-elimination tactics. You can run the (help-tactic) command using the SMTLib interface and see several options. For quantifier elimination, it has:

- qe-light apply light-weight quantifier elimination.
- qe apply quantifier elimination.
- qe2 apply a QSAT based quantifier elimination.
- qe_rec apply a QSAT based quantifier elimination recursively.

For your example, I found that qe2 works just fine. Give that a try!

Regarding why z3 doesn't provide a combined tactic: Use of tactics in theorem proving is still more of an art than science. Knowing what tactic works the best still requires human ingenuity, though of course the tools have come really far. So, instead of providing heavy-weight tactics, most theorem provers (and z3) provide a set of basic tactics and means of combining them. This allows the end-user to try these tactics, if one fails try another, try them for a fixed amount of time, etc., to find a winning strategy. z3 also provides probes to further enable tactic programming. So, the idea is that you can yourself code whatever tactic you'd like and develop your own tools on top of the basic infrastructure provided by z3.