[SMT-COMP] [mathsat] Re: QF_FP, min and zeros

[Alberto Griggio]

Hi all,

> 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
> 

[...]

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

Regarding MathSAT:

- there's a flag to enable the SMT-LIB semantics for fp.min and fp.max
  (-theory.fp.minmax_zero_mode=4), but it is not the default (which is
  to always return +0)

- fp.to_ubv and fp.to_sbv deviate from the SMT-LIB standard: if the
  input is NaN or infinity, zero is returned. If the input is out of
  range, it is simply truncated

- fp.to_real is currently unsupported

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

I don't think the above are reasons to exclude the benchmarks -- MathSAT
is not going to enter the competition (at least not volutarily :-)


Alberto