[SMT-LIB] QF_BV and division by zero

[Clark Barrett]

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.

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