[SMT-LIB] QF_BV and division by zero

[Bruno Dutertre]

On 04/03/2017 12:40 PM, Clark Barrett wrote:
> Yes, this thread is focused only on the partial operations in the theory of
> bitvectors.
>
> I do not think we will ever achieve consensus on this issue and there are
> valid viewpoints on all sides.  However, we do have a strong majority of
> developers in favor of the encoding that produces all 1's for bvudiv.
> Given that application users can encode their own semantics easily using
> define-fun and the if-then-else operator, we are inclined to go with the
> developer preference.
>
> However, I'd like to see some discussion in response to Trevor's claim, as
> he is also coming from a developer's point of view.  I'd also still like to
> see some opinions about the best way to handle bvurem.  If possible, let's
> try to have everyone weigh in by the end of this week and I'll plan to
> circulate a new version of the QF_BV logic early next week.
>

 From an implementation point of view, the simplest approach is one that
avoids special treatments for division by zero and makes things uniform.

The majority of implementers have chosen (bvudiv x 0) = 11...1 because
that's what you get from a long division algorithm or divider circuit
based on long division, and I guess that's how most of us implement division
in SMT solvers.

It is also reasonable to define:

     (bvurem x y) = x - (bvudiv x y) * y.

This equality is already required by SMT-LIB when y>0. If we require
the equality to also hold for y=0, we have  (bvurem x 0) = x no matter
how we define (bvudiv x 0). This is again consistent with what the
long-division algorithm produces.

For the rest, there's no reason to change the definitions of
bvsdiv, bvsmod, and bvsrem. They can be defined in terms of bvudiv
and bvurem as they currently are.


The alternative proposed by Trevor is to set (bvudiv x 0) = 0 and
(bvurem x 0) = 0, and keep the existing definitions of
bvsdiv/bvsmod/bvsrem.  This would introduce two special cases:

    (bvudiv x y) = IF y=0 THEN 0 ELSE (long-division x y)

    (bvurem x y) = IF y=0 THEN 0 ELSE x - (bvudiv x y) * y

I don't see why that's better.


Bruno



> Thanks,
>
> -Clark
>
> On Mon, Apr 3, 2017 at 8:23 AM, Martin Nyx Brain <martin.brain at cs.ox.ac.uk>
> wrote:
>
>> On Fri, 2017-03-31 at 23:07 -0700, Clark Barrett wrote:
>>> Hi everyone,
>>>
>>> Yes, this should have been finalized last year and it's my fault it
>> wasn't
>>> - I'm very sorry :(
>>> We have discussed this far too many times, but let's fix it finally.
>>
>> (Can I just clarify this is the discussion about bit-vector divide /
>> remainder by zero and not any of the other partially interpreted
>> functions?)
>>
>> <snip>
>>> The main reason to fix the interpretation is to make solver development
>> for
>>> QF_BV more clear and straightforward.
>>>
>>> Trevor, you are arguing for a value of 0, but do you disagree that a
>> vector
>>> of 1's is the most natural result from a circuit?  What do others think
>>> about his argument for 0?
>>
>> <unhelpful and can be ignored>
>> That rather depends on what kind of circuit you use.  For example, you
>> could reduce x = a/b  to  b * x + r == a  &&  0 <= r < x  which we've
>> tried with some performance benefit.
>> </unhelpful and can be ignored>
>>
>> Cheers,
>>  - Martin
>>
>>
>>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>


-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4049 bytes
Desc: S/MIME Cryptographic Signature
URL: </pipermail/smt-lib/attachments/20170403/5f5e9cae/attachment.p7s>