SMT-LIB v2.0 support

39 views
Skip to first unread message

Marko Dimjašević

unread,
Sep 16, 2012, 2:39:29 AM9/16/12
to ope...@googlegroups.com
Greetings,

At the Wikipedia article about SMTs [1] there is a table with SMT
solvers, and OpenSMT is listed there:

https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories#SMT_solvers_2

Under the SMT-LIB column of the table, OpenSMT reads "partial
v2.0". Does that mean that it doesn't fully support SMT-LIB v2.0?

I was thinking of contributing to the OpenSMT by writing source
code. What do you think, how much of work there is to be done so that it
fully supports SMT-LIB v2.0?


Cheers,
Marko Dimjašević


[1] https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories
signature.asc

Roberto Bruttomesso

unread,
Sep 16, 2012, 4:54:43 AM9/16/12
to ope...@googlegroups.com
On Sun, Sep 16, 2012 at 8:39 AM, Marko Dimjašević <ma...@cs.utah.edu> wrote:
> Greetings,
>
> At the Wikipedia article about SMTs [1] there is a table with SMT
> solvers, and OpenSMT is listed there:
>
> https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories#SMT_solvers_2
>
> Under the SMT-LIB column of the table, OpenSMT reads "partial
> v2.0". Does that mean that it doesn't fully support SMT-LIB v2.0?

It is a bit an ambiguous statement. For the logics it solves it
support the standard.
But other logics that you can write in smtlib are not supported:
for instance it does not support quantifiers, or the theory of arrays

>
> I was thinking of contributing to the OpenSMT by writing source
> code. What do you think, how much of work there is to be done so that it
> fully supports SMT-LIB v2.0?

to support all the theories it's a lot of work

R

>
>
> Cheers,
> Marko Dimjašević
>
>
> [1] https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories



--
Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70

Marko Dimjašević

unread,
Sep 16, 2012, 4:51:24 AM9/16/12
to ope...@googlegroups.com
Greetings,

At the Wikipedia article about SMTs [1] there is a table with SMT
solvers, and OpenSMT is listed there:

https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories#SMT_solvers_2

Under the SMT-LIB column of the table, OpenSMT reads "partial
v2.0". Does that mean that it doesn't fully support SMT-LIB v2.0?

I was thinking of contributing to the OpenSMT by writing source
code. What do you think, how much of work there is to be done so that it
fully supports SMT-LIB v2.0?


signature.asc
Reply all
Reply to author
Forward
0 new messages