Consider I have a formula with the shape: ∃a.∀b.∃c.∀d. Phi, where a,b,c,d belong to some first-order theory T that admits quantifier elimination.
If I would like to get a model of this formula in Z3, I would only get an assignment for a (the outermost existential variable) or, as the answer in What does a model in ∃x∀y∃z∀u . F[x, y, z, u] mean? suggests, a and some function G(a) that represents the value of c. However, imagine I am really interested in getting an 'assignment' for c and I cannot afford to leave it up to Z3.
To achieve this, my idea is to perform quantifier elimination (QE) in order to get the valuation of c depending on the valuation of a (which is the assignment in the model). So:
∃a.∀b.∃c.∀d. Phi produces ∃a.∀b.∃c. Phi', where there is no d (i.e., we substituted d depending on the other variables) in Phi'.∃a.∀b.∃c. Phi' produces ∃a. ∀b. Phi'',
where there is no c (i.e., we substituted c depending on the other variables) in Phi''.∃a. ∀b. Phi'' produces ∃a. Phi''',
where there is no b (i.e., we substituted b depending on the other variable) in Phi'''.Thus, when we solve ∃a. Phi''' and get a model for a, then we have a valuation for b. I mean, QE methods such as Cooper usually imply substituting an innermost variable with an outermost one (this is the variable -and quantifier- elimination part); e.g., if Cooper says b=2a, then we get rid of b by writing 2a in each appearance of b. Then, since the value of c depends on a and b (and b depends on a), we can get c from a.
My question: is this reasoning correct? I mean, if I store value b depending on a, and value c depending on a and b, is it sufficient to get assignment (model) for a in order to get the corresponding c for that assignment? Or am I missing something?
Unfortunately, this is not a valid line of reasoning. The trouble is with your 1st and 3rd sentences; which is similar, so I'll look at the first one:
How do you eliminate d? It's a universally quantified variable. So, when you eliminate it, it'll disappear. There's no value for d that you can write in terms of the other variables in your formula.
When you eliminate an existential, you come up with a value for it in terms of the others. (This is the skolem function we discussed before.) But not when you eliminate a universal. And this makes intuitive sense: The formula is true for all such d: You can't expect to just reduce it to one value: It's true for all such d.
Here's a concrete example that can clarify the issue. Let's consider the theory of bit-vectors, say 8-bits wide, unsigned. Clearly this is a decidable theory, since it's finite. It does admit quantifier elimination in the obvious way: Replace exists with a disjunction over values 0..255, and forall with conjunction over the same.
Now consider the formula:
∃x.∀y. x >= y
This is satisfiable: Pick x to be 255, it's the largest value in the domain, so it's greater than all y. A simple minded solver can go about establishing this by eliminating the quantifiers in a trivial (but not at all efficient!) way as follows. Let's eliminate the universal quantifier. (This is your step 1 above):
∃x. x >= 0 /\ x >= 1 /\ x >= 2 /\ ... /\ x >= 255
Look what happened: We got rid of the quantifier (i.e., y has disappeared), but we don't really have a formula for y in terms of x. (This was the invalid inference you had.)
We can now eliminate the exists quantifier by turning it into a series of disjunctions:
(x = 0 /\ (x >= 0 /\ x >= 1 /\ .... /\ x >= 255))
\/ (x = 1 /\ (x >= 0 /\ x >= 1 /\ .... /\ x >= 255))
\/ (x = 2 /\ (x >= 0 /\ x >= 1 /\ .... /\ x >= 255))
...
\/ (x = 255 /\ (x >= 0 /\ x >= 1 /\ .... /\ x >= 255))
Now we have simple boolean reasoning with equality, letting us substitute
(x = 0 /\ 0 >= 0 /\ 0 >= 1 /\ .... /\ 0 >= 255)
\/ (x = 1 /\ 1 >= 0 /\ 1 >= 1 /\ .... /\ 1 >= 255)
...
\/ (x = 255 /\ 255 >= 0 /\ 255 >= 1 /\ ... /\ 255 >= 255)
Each disjunct above except the last reduces to false, and the last simplifies all by simple bit-vector equality to:
x = 255
And there you go: You found a satisfying model with x = 255, and for all values of y. There is no value of y defined in terms of x. (I should emphasize that a real solver wouldn’t eliminate quantifiers this way, it’d use much more performant methods. This is merely for illustration purposes.)
If we had your original formula ∃a.∀b.∃c.∀d. Phi and did the above procedure, we'd end up with a value of a, a value of c in terms of b; i.e., a skolem function; but b and d would disappear. (Assuming the formula is satisfiable to start with.)
As an illuminating exercise, again consider the theory of bit-vectors; but let's limit it to mere 1-bit just for ease, and apply the above procedure to the formula:
∀a.∃b. a >= b
Let's eliminate the inner b with a disjunction:
∀a. (b = 0 /\ a >= b) \/ (b = 1 /\ a >= b)
Now eliminate the a with conjunction:
((a = 0) /\ ( (b = 0 /\ a >= b) \/ (b = 1 /\ a >= b) ))
/\ ((a = 1) /\ ( (b = 0 /\ a >= b) \/ (b = 1 /\ a >= b) ))
With simple boolean reasoning, this reduces to:
((a = 0) /\ (b = 0))
/\ ((a = 1) /\ ((b = 0) \/ (b = 1))
And now you can see where this is going. The choice of b depends on what the choice for a is; we cannot independently fix a simple b in general. (Well, in this case b = 0 works for both, but in general b will be a function of a.) This is what skolemization gives us. Let's skolemize the formula:
∀a.∃b. a >= b is equisatisfiable with ∀a. a >= B(a)
where B is a function symbol. Now eliminate the quantifier with conjunction:
(0 >= B(0)) /\ (1 >= B(1))
We have to demonstrate a B that has this property. Since our model is finite, it's easy to come up with it:
B(a) = 0
i.e., the constant function that maps everything to 0. Or:
B(0) = 0
B(1) = 1
i.e., the identity function; that works as well; picking different b's depending on the value of a. In general there could be any number of skolem functions; all the solver has to do is to demonstrate one.
An SMT solver can find such a B if it is finitely valued. (And for bit-vectors, that'll always be the case), but not for infinite domains. But that's a different discussion. The point is that this is done internally by the solver and not shown to the user, but there are tricks to have the solver display it. (By essentially manually doing the skolemization yourself, as we discussed before.)
I hope that clears things up. I find thinking about bit-vectors is the simplest when it comes to quantifier elimination, since the algorithm is really simple in that case. Existentials become disjunction and universals become conjunction. By keeping equalities around, you can extract model values. But the value of any existentially quantified variable that appears in the scope of a bunch of universals will be a function of those universals. If the existential is at the top (i.e., no universals to scope over it), then we get a domain constant. And those are the constants that the SMT solver displays for us, unless we manually skolemize ourselves.