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

[Yeting Ge]

Hi Ofer,

In terms of building a new expression, CVC3 can do this by calling some 
interface function that will return existentially quantified or 
universally quantified exprs.  For CVC3, bound variables are of a special 
kind and some modifications of the original exprs may be needed.  I would 
guess that Z3 can do this too.


Thank you,
Yeting

On Fri, 12 Sep 2008, 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 ?
>
> Thanks,
> Ofer
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>