Question about the current state of SMT-LIB 3

[Kristoffer Norrman]

Dear SMT-LIB community,

I am PhD student at Uppsala University and is currently working on floating-point verification. Part of the project is focused on the SMT-LIB 3 proposal that came out a few years ago; specifically the introduction to dependent and polymorphic types in version 3. Since there has not been any update since 2021-12-31 on the SMT-LIB website, two main questions have come up:

1. Are there any updates on the SMT-LIB 3 that I might have missed? The only thing I have been able to dig up are some talks that has mentioned it in their abstract.

2. Do any of you know of any SMT-solvers that might have some experimental version (a git branch for example) that implements (part of) the SMT-LIB 3 standard? 

I, of course, may not have been digging deep enough or looking in the wrong direction, but any help is welcome!

It might also be worth mentioning that my supervisor and I have been working on an (unpolished) theory of floating-point numbers for SMT-LIB 3. 

Cheers,
Kristoffer 

[Cesare Tinelli]

Dear Kristoffer,

Thanks for your interest in SMT-lIB 3. Lamentably, there is no official reference on it yet. However, we have made substantial progress at this point and expect to publish an initial version of the reference documents in the next few months. 

In the meantime, you can consult the proposal on the web at https://smt-lib.org/version3.shtml, which has just been updated. While the updated webpage is not exhaustive, it now reflects the main aspects of SMT-LIB 3 pretty accurately.

The web page contains a couple of theory definitions in the new syntax (as modules) but FPA is not there yet. We expect to add it soon, together with the theory of bit vectors. All theories will follow closely those in Version 2.7. The main differences will be the addition more operators and the elimination of indexed symbols, although the indexed syntax will be retained for backward compatibility.

In the FPA case, this means that (_ FloatingPoint eb sb) will become (FloatingPoint eb sb) and all indexed function symbols will become regular symbols with two additional, possibly implicit, arguments. So, for instance, the indexed constant (_ +oo eb sb), now of sort (_ FloatingPoint eb sb), will become a regular function symbol +oo of dependent type (eb:Int) -> (sb:Int) -> FloatingPoint(eb, sb) or, in SMT-LIB 3 syntax, (-> (! Int :var eb) (! Int :var sb) (FloatingPoint eb sb)). Similarly, the indexed symbol to_fp_unsigned, say, will become a regular function symbol of type  (-> (! Int :var eb) (! Int :var sb) RoundingMode (BitVec (+ eb sb)) (FloatingPoint eb sb)). In contrast, a non-indexed symbol like fp.neg will get the type (-> (! Int :var eb :implicit) (! Int :var sb :implicit) (FloatingPoint eb sb) (FloatingPoint eb sb)). This means that applications of those symbols will look like: (+oo eb sb), (to_fp_unsigned eb sb rm bv), (fp.neg x). (To be precise, the types will be a bit more complicated as they will include restrictions on eb and sb. See the webpage.) 

Please feel free to let us know if you have any questions.

 

Best,

Cesare, also for Clark and Pascal

[Nicola Gigante]

Hi Cesare,

is there a reference implementation of the new SMT-LIB language?

Maybe a parser or a validator for solutions?

Best,

Nicola

[Haniel Barbosa]

Hi Nicola,

AFAIK there is no official reference, but Dolmen can serve as one (it
is for example what is used for model validation at SMT-COMP):

https://github.com/Gbury/dolmen

This gets tricker if what you are interested in is in validating
proofs of unsatisfiability though. :)

Best,

--
Haniel Barbosa
https://hanielbarbosa.com/

[Guillaume Bury]

Hi all,

Just jumping on the question about a reference implementation: I plan to work on adding support for version 3 of SMT-LIB to Dolmen (which is currently used to check validity of new benchmarks proposed for the SMT-LIB, as well as for the model track of SMT-COMP) as soon as a somewhat stabilized proposal is ready (not necessarily final, but at least with the major changes not subject to further changes).

The next release of Dolmen (which should happen in the next few weeks) will have support for version 2.7 (coming a bit late this time, the work was done some time ago, but I forgot to cut a release then).

Best,
Guillaume

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/smt-lib/87eclivbvh.fsf%40gmail.com.

--

Guillaume Bury

[Cesare Tinelli]

Hi all,

To clarify, there is no official reference implementation of SMT-LIB. This is on purpose as we (the SMT-LIB coordinators) want the reference document to be the only source of truth. That said, Guillaume has strived for Dolmen to be a fully compliant front-end/validator for the versions it supports. In particular, it has been used successfully for the last few years to validate benchmarks submitted to the library. Furthermore, Dolmen is open source and has a VS Code extension, also developed by Guillaume. So it is a highly-recommended reference.

We plan to work closely with Guillaume so that Dolmen can play the same role in SMT-LIB 3 once the reference document is out.

Best,

Cesare