[SMT-LIB] SMT solver's API

[Aaron Stump]

Hi, Kecheng.

On Tue, Jan 25, 2011 at 12:09 PM, <kecheng at cecs.pdx.edu> wrote:

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

No problem, I'm happy to try to help, although others on this list may have
more expertise.


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

Yes, this approach to connecting your tool to an SMT solver will work, and
is reasonable.  It will allow you to connect to any solver supporting the
SMT-LIB format, and using the features of SMT-LIB version 2.0, you can
interact in a more fine-grained way with the solver.

Of course, we could wish for a tighter integration of solvers with other
tools, via an in-memory functional interface, but there is no standard
definition of such an interface as part of SMT-LIB.  Some tools may provide
you such an interface, but then your ability to try different tools will be
limited (by the lack of a standard interface).

Good luck,
Aaron


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