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

Ofer Strichman ofers at ie.technion.ac.il
Fri Sep 12 12:45:57 EDT 2008


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
 


More information about the SMT-LIB mailing list