[SMT-LIB] How to submit benchmarks to smtlib

[Christoph Wintersteiger]

I agree, that sounds like a good solution to the logic-naming problem, I'm in favor. 

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: Florian Schanda [mailto:florian.schanda at altran.com] 
Sent: 23 March 2015 15:10
To: smt-lib at cs.nyu.edu
Cc: Levent Erkok; David R. Cok; Christoph Wintersteiger; smt-comp at cs.nyu.edu
Subject: Re: [SMT-LIB] How to submit benchmarks to smtlib

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