[SMT-LIB] SMT solver's API

[Kecheng]

Hi all,

I'm developing a checker to check the equivalenc between C and RTL implement. SMT solver is our decision procedure, particularly CVC3. I'm using CVC3 through its API directly. Now I want to find a way to easily plugin any other SMT solver, like MathSAT or Yices. Can I use SMT-lib? My understanding of SMT-lib is that it's a standard format, any SMT solver can take it as input. But it cannot be done through solver's API, is it correct? Is there any existing wrapper for all the solver's API? Thanks.

Best,

Kecheng
2010-12-16