[SMT-LIB] QF_BV and division by zero

[Mathias Preiner]

I also agree with Bruno.

Mathias

On 04/04/2017 06:00 AM, Bruno Dutertre wrote:
> 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
>>
>
>
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>