[SMT-LIB] SMT solver's API

[Tinelli, Cesare]

Hi Kecheng and all,

On 26 Jan 2011, at 11:24, Aaron Stump wrote:

> Hi, Kecheng.
> 
> On Tue, Jan 25, 2011 at 12:09 PM, <kecheng at cecs.pdx.edu> wrote:
> 
> 
[...]
> 
>> 
>> 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.
> 
That said, I'd like to clarify that there is no specific command in SMT-LIB 1 or 2 to send an expression to an solver and get back a simplified version of it.
If an SMT solver provides that functionality, you'll have to interact with it using the solver's native textual format. 

Best,


Cesare

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