Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category

[Christoph W. <cw...@mi...>]

Hi David,

The theory definitions is here:
http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2

There are no formal logic definitions yet, but for QF_FP and QF_BVFP it's straightforward (with the exception that FP uses bit-vector numerals, but no other BV operations). Solvers that support FP and that I know of are: Z3, MathSAT, Sonolar. AFAIK, CVC4 will have support soon, it would great to get them to participate in the demo track, but I don't know how much effort this will take on their end. CBMC is not an SMT solver, but it has a bit-blaster that can emit SMT2 formatted queries. 

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: David Deharbe [mailto:da...@di...] 
Sent: 06 May 2015 14:30
To: Christoph Wintersteiger
Cc: smt...@li...; Martin Brain
Subject: Re: [Smtcomp-discussion] SMT-COMP 2015, Floating-point category

Hi Christoph,

I was wondering if there exists a document that specifies this floating point logic? Also could you inform me some solvers that support them? Besides z3 I suppose…

Best regards,

— David.

> On Feb 11, 2015, at 11:20 AM, Christoph Wintersteiger <cw...@mi...> wrote:
> 
> Hi Sylvain, David, Tjark,
>  
> Martin Brain and I discussed the possibility of a category for floating-point arithmetic at this year’s SMT comp. We believe that there are enough solvers and sufficient interest, and the theory definition has recently been finalized. We are happy to collect benchmarks (we have a few ready) and to assist with the running of the competition if there are any issues of course. What would be the next steps for us to make this happen?
>  
> Thanks!
> Christoph
>  
>  
> Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: 
> +44 1223 479999 |research.microsoft.com/people/cwinter
>  
> <image001.jpg>
> 
> 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
>  
> ----------------------------------------------------------------------
> -------- Dive into the World of Parallel Programming. The Go Parallel 
> Website, sponsored by Intel and developed in partnership with Slashdot 
> Media, is your hub for all things parallel software development, from 
> weekly thought leadership blogs to news, videos, case studies, 
> tutorials and more. Take a look and join the conversation now. 
> http://goparallel.sourceforge.net/____________________________________
> ___________
> Smtcomp-discussion mailing list
> Smt...@li...
> https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion