[SMT-LIB] How to submit benchmarks to smtlib
Martin Brain
martin.brain at cs.ox.ac.uk
Fri Apr 10 15:22:16 EDT 2015
On Fri, 2015-03-27 at 14:31 +0000, Christoph Wintersteiger wrote:
> I agree, that sounds like a good solution to the logic-naming problem, I'm in favor.
It sounds good to me as well. Although I will sound one note of
caution. Logics have not just been a combination of signatures, they
have also introduced syntactic sugar and restrictions on what sorts and
terms were well defined. The real challenge is how to handle
restrictions in a modular way. For this to be a serious proposal,
someone would need to look at the current logics and propose how the
restrictions in them could be handled.
HTH
Cheers,
- Martin
More information about the SMT-LIB
mailing list