Even for simplest arithmetic SMT problems the existential quantifier is required to declare symbolic variables. And ∀ quantifier can be turned into ∃ by inverting the constraint. So, I can use both of them in QF_* logics and it works.
I take it, "quantifier free" means something else for such SMT logics, but what exactly?
The claim is that
∀quantifier can be turned into∃by inverting the constraint
AFAIK, the following two relations hold:
∀x.φ(x) <=> ¬∃x.¬φ(x)
¬∀x.φ(x) <=> ∃x.¬φ(x)
Since a quantifier-free SMT formula φ(x) is equisatisfiable to its existential closure ∃x.φ(x), we can use the quantifier-free fragment of an SMT Theory to express a (simple) negated occurrence of universal quantification, and [AFAIK] also a (simple) positive occurrence of universal quantification over trivial formulas (e.g. if [∃x.]φ(x) is unsat then ∀x.¬φ(x)¹).
¹: assuming φ(x) is quantifier-free; As @Levent Erkok points out in his answer, this approach is inconclusive when both φ(x) and ¬φ(x) are satisfiable
However, we cannot, for example, find a model for the following quantified formula using the quantifier-free fragment of SMT:
[∃y.]((∀x.y <= f(x)) and (∃z.y = f(z)))
For the records, this is an encoding of the OMT problem min(y), y=f(x) as a quantified SMT formula. [related paper]
A term
tis quantifier-free ifftsyntactically contains no quantifiers. A quantifier-free formulaφis equisatisfiable with its existential closure(∃x1. (∃x2 . . .(∃xn.φ ). . .))where
x1, x2, . . . , xnis any enumeration offree(φ), the free variables inφ.
The set of free variables of a term
t,free(t), is defined inductively as:
free(x) = {x}ifxis a variable,free((f t1 t2 . . . tk)) = \cup_{i∈[1,k]} free(ti)for function applications,free(∀x.φ) = free(φ) \ {x}, andfree(∃x.φ) = free(φ) \ {x}.