Re: [Smtcomp-discussion] benchmarks involving divide by zero

[Bruno D. <br...@cs...>]

On 06/13/2014 09:13 AM, Tjark Weber wrote:
> On Fri, 2014-06-13 at 14:57 +0200, Armin Biere wrote:
>> I tend to disagree here, since why should 'undefined' mean that
>> it is defined to return always the same value?  For instance,
>> signed integer overflow gives undefined behaviour in C, but actually
>> 'undefined' means that the compiler can do what it wants (everytime
>> such an overflow occurs).  In order to make sure you meet the
>> specific semantics of your application, you have to change the
>> encoding anyhow.
>
> This is true for C, of course. I don't think it is very fortunate, and
> if anything, I think it is an argument for an even *weaker* semantics
> of bv_div. But as mentioned, the current semantics is the closest we
> can come to modeling undefinedness in the total logic of SMT-LIB.
>
> Best,
> Tjark
>

Whichever way we define the semantics of divide by zero. This will
always be a corner case and I doubt we can get a definition that
will immediately satisfy every user. Saying that (bvdiv x 0) should
be undefined may be convenient and familiar for people in the
Isabelle/HOL world but they are many other users outside this world.
Who is to say that (bvdiv x 0x000) = 0xfff is incorrect for them?

The best choice is to provide a basic semantics that is clear and
easy to support, so that the tools actually implement it. Users
who want something else can easily encode whatever they need on
top of that by using the (define-fun ..) commands of SMT-LIB.
It is straightforward to encode the 'div-by-zero is undefined'
semantics by moving to the QF_UFBV  or UFBV logics. These logics
are very appropriate for this purpose.

Bruno