[SMT-LIB] Looking for a tool that can existentialy quantify a single variable

[Jim Saxe]

Ofer Strichman wrote:

 >Hello there,
 >Is anyone aware of a solver that its interface allows to existentially 
 >quantify a single variable from a linear arithmetic formula ?
 >In other words, given a boolean combination of linear predicates \phi, 
and a >single numeric variable x, returns \exists x. \phi, i.e. \phi 
after >existentially quantifying x ?

I don't have an answer, but just to make sure everyone understands
the question, are you asking for a solver that can take the formula
(\exists x . \phi), and return an equivalent quantifier-free
expression in the variables other than x?

For example, if \phi were simply a conjunction of linear inequalities,
then you could remove the existentially quantified variable "x" by
Fourier-Motzkin elimination at the cost of up to quadratic increase
in the size of the formula.  For \phi an arbitrary boolean combination
of linear predicates you could first rewrite \phi as a disjunction
of conjunctions (with potential exponential blow-up in formula size),
then apply Fourier-Motzkin elimination to eliminate x from each
conjunction separately.  I understand you to be looking for a tool
that produces logically equivalent results while (at least sometimes)
achieving less blow-up in formula size, and perhaps preserving more
of the original structure of the formula.  Is this right?

--Jim