search

ths-rwth / smtrat

http://smtrat.github.io/
Other
52 stars 12 forks source link

Request: Add example model files #101

Open rpgoldman opened 2 years ago

rpgoldman commented 2 years ago

The SMT-RAT docs are quite helpful to the C++ programmer, but for those of us who wish to just use the SMT-RAT program on model files, it would be nice to have some example smtlib files. It's easy to find examples of smtlib files in general, but not to find those that exercise SMT-RAT's polynomial solving capabilities.

I understand it might be a lot of work to do that, so I thought it might be a good start to collect up the models you used in your SAT-2015 paper experiments, so that novices like me can play with SMT-RAT before trying to build models for our own research.

rpgoldman commented 2 years ago

Looking a little further, I imagine that pointers into the SMTLIB benchmark set would probably be sufficient. Just a list of logics to experiment with would be enough -- from there one can find model files on that site.