[SMT-LIB] [Smtcomp-discussion] FP demo track at SMT-COMP

[Christoph Wintersteiger]

There's about an equal number of arguments for both sides in this discussion. 

My suggestion is to implement whichever is easiest to implement in your solver. 

We can then add a mandatory command line parameter. If that parameter is not set to any value, we will issue a warning about which semantics are being used and that the user has to set the option even if the default is the right choice. This way, we force the user to explicitly choose the semantics they want (and obviously if they don’t chose anything, they don't care), and we can throw an error if they chose an unsupported option.

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: Tjark Weber [mailto:tjark.weber at it.uu.se] 
Sent: 11 June 2015 09:15
To: Martin Brain
Cc: Alberto Griggio; smtcomp-discussion at lists.sourceforge.net; smt-lib (smt-lib at cs.nyu.edu); Christoph Wintersteiger; Florian Lapschies; wahl at ccs.neu.edu; Pascal.Fontaine at inria.fr; Schanda Florian; Philipp Ruemmer (philipp.ruemmer at it.uu.se)
Subject: Re: [Smtcomp-discussion] FP demo track at SMT-COMP

On Thu, 2015-06-11 at 08:34 +0100, Martin Brain wrote:
> On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote:
> > Fixing one return value while existing IEEE-compliant 
> > implementations return different values would be actively harmful in 
> > my opinion. It is foreseeable then that users will use fp.min to 
> > model IEEE min, that some (if not most) will be unaware of the 
> > subtle semantic difference, and that they will ultimately believe 
> > they've verified their code when it may well break on some architectures.
> 
> I agree with you but note that there is a counter-argument that in the 
> situation you give, the current semantics will give spurious 
> counter-examples that cannot be executed on the target platform.  I 
> guess it is personal taste depending on whether you feel it is better 
> to under or over approximate the behaviour of the system.  My 
> reasoning was that all IEEE-754 compliant systems should be model of the theory.

You are right. Do I prefer spurious counter-examples (which users will then look into, and which they can easily rule out with additional assumptions if they want to verify their code against a specific IEEE
implementation) over unsound proofs (which users won't notice as unsound until their programs break in production)? Absolutely.

Best,
Tjark