[SMT-COMP] Contribution of QF_FPBV and QF_FPABV benchmarks

[Delcypher]

Hi,

On 24 March 2017 at 17:21, Christoph Wintersteiger
<cwinter at microsoft.com> wrote:
> Hi Dan, Clark, all,
>
> Thanks Clark for the detailed answer!
>
> In addition to what Clark said, it may be helpful to know that benchmarks without status annotation won't be used in the SMT competition (afaik), so if you are reasonably confident of the status, please do add it.
>
> Regarding Z3's fp.to_ieee_bv, here is what the FP theory definition says:
>
> :note
>  "There is no function for converting from (_ FloatingPoint eb sb) to the
>   corresponding IEEE 754-2008 binary format, as a bit vector (_ BitVec m) with
>   m = eb + sb, because (_ NaN eb sb) has multiple, well-defined representations.
>   Instead, an encoding of the kind below is recommended, where f is a term
>   of sort (_ FloatingPoint eb sb):
>
>    (declare-fun b () (_ BitVec m))
>    (assert (= ((_ to_fp eb sb) b) f))
>  "
>
> So, a quick dirty hack is to simply replace all occurrrences of fp.to_ieee_bv with new, uninterpreted functions. If your infrastructure makes it easy to add the additional assertions/constraints on them you could add those too. Of course, semantics for NaNs may be different, but that may not be important in the context of SMTLIB.

I'm analysing the queries I collected now.

If there are a lot that use `fp.to_ieee_bv` I may modify my tool to
issue the queries to Z3 in a different way. I thought this would be a
pain because I would need to avoid creating new variables with
non-conflicting names but it looks like Z3's C API has
`Z3_mk_fresh_const()` which will make my life much easier :D

Thanks,
Dan.