[SMT-LIB] SMT solver's API

[Aaron Stump]

Hi, Kecheng.

No standard in-memory API for SMT solvers exists at this point,
unfortunately.  So at the moment, you can only use the SMT-LIB format to
communicate textually with an SMT solver.  I am not aware of any attempt to
create a universal wrapper around solvers' in-memory interfaces (which might
not be that easy, since many solvers are closed source).

Best wishes,
Aaron

On Thu, Dec 16, 2010 at 11:40 PM, Kecheng <kecheng at cecs.pdx.edu> wrote:

> 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
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>