search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

the translator from Btor2 to VMT #163

Closed chucq closed 3 years ago

chucq commented 3 years ago

Hello，

I compiled and installed boolector, it's a very nice tool to use, and I tried to translate btor2 files to VMT files with it, however, I did not find any function or script that can support this need. And I noticed that in the conclusion part of your paper "BTOR2 , BtorMC and Boolector 3.0", it is mentioned that you plan to provide such a translator. So I am wondering if this translator is already included in the latest version of boolector. If yes, could you please provide some necessary information about it?

Thanks

arminbiere commented 3 years ago

I do not recall any work on this (at least within Boolector).

chucq commented 3 years ago

got it, thank you for your quick reply.

I do not recall any work on this (at least within Boolector).

aniemetz commented 3 years ago

Yes, I don't either. And we (team Boolector) did not work on such a translator (yet).