[SMT-LIB] SMT solver's API

[kecheng@cecs.pdx.edu]

Hi Aaron,

I'm sorry to bring to old topic to discuss with you. I have one more  
question about the communication with SMT solver via SMT-Lib.

To invoke the SMT solver textually, that means I need some  
Inter-process communication (IPC) between my program and the solver,  
right? In my project, I want to do the symbolic simulation. For  
example, I want to use the SMT solver to simplify/rewrite an  
expression. What should I do? In my program, I will have my only  
format to represent an expression. To make a query with the SMT  
solver, I have to convert my format to the SMT-Lib format, then invoke  
the solver. The SMT solver will return a simplified expression, but in  
STM-Lib format. Now I should have a parser to parse it into our format  
again. Do it make sense? Or do you have any better suggestion?

Best,

Kecheng

> 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
>