[SMT-COMP] QF_FP, min and zeros

[Christoph Wintersteiger]

Hi all,

Z3 implements those semantics and the QF_FP/wintersteiger benchmarks were updated to reflect those semantics (at least in the develop branch in the git). Z3 implements those semantics, but it also has a flag to switch it to non-UF/BV-only semantics. 

Cheers,
Christoph


Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/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: 21 April 2017 13:05
To: smt-comp at cs.nyu.edu
Cc: Christoph Wintersteiger <cwinter at microsoft.com>; mathsat at fbk.eu
Subject: Re: [SMT-COMP] QF_FP, min and zeros

On a related note, I am wondering about the status of benchmarks and solver implementations regarding

  fp.min, fp.max, fp.to_ubv, fp.to_sbv, fp.to_real

In 2016, benchmarks containing any of these functions where excluded from the competition.

Based on https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fsmtlib.cs.uiowa.edu%2Ftheories-FloatingPoint.shtml&data=02%7C01%7Ccwinter%40microsoft.com%7C7866986eed37456e3a6608d488aea167%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636283730994951776&sdata=vETCAA6RaVtcFAemyFyW9M6ALali4vSfK9vO4iSqSRU%3D&reserved=0 my understanding is that these functions are underspecified (i.e., they have more than one possible interpretation).

1) Is the status of benchmarks in QF_FP/QF_BVFP (if known) correct with respect to this semantics?

2) Do solvers that support floating-point logics (e.g., MathSAT, Z3) implement this semantics?

3) Are there (other) reasons to again exclude these functions from the competition in 2017?

Best,
Tjark