[SMT-LIB] How to submit benchmarks to smtlib

[Florian Schanda]

On Tuesday 17 Mar 2015 16:16:43 Levent Erkok wrote:
> To that end, I think we can look to the programming language community for
> a proper solution. From a tool perspective, setting the logic is really
> about what set of names are brought into the scope. In that sense, it's
> akin to import statements of regular languages. So, perhaps a better
> approach would be to allow multiple import statements in a benchmark to
> determine what logical constants are available:
> 
>       (import Quantifiers)
>       (import BitVectors)
>       (import LinearIntegerArithmetic)

I agree that something like that would be a natural way to do it, but I might 
be missing something. The current situation is a somewhat annoying and more 
often than not I resort to ALL_SUPPORTED in CVC4.


I think declaring all these at the top of the file sounds like a good idea, I 
don't think allowing these to appear randomly is very helpful...


	Florian