Re: [Smtcomp-discussion] benchmarks involving divide by zero
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Bruno D. <br...@cs...> - 2014-06-12 14:59:16
|
On 6/12/14, 5:59 AM, Armin Biere wrote: > Oh well, maybe I should repeat by previous message in another thread > (the one I forwarded to Bruno). I just copied an pasted what I wrote > 2 days ago: > > > > I do think the standard is broken here (and I discussed this many times). > In order to implement division by zero as defined by the standard one has > to add an uninterpreted function say 'zero_division' and define > > a smt-lib-unsigned-div b = b ? a internal-unsigned=div b : zero_division (a) > > which requires to use the theory of uninterpreted functions (or for Boolector > arrays without read) whenever there is a division operator in the input. > > The most natural way of making the division defined everywhere is to > have it return the largest number 11111...11111 if the divisor is zero. > This is what you would naturally get by bit-blasting using a division > circuit. > > This is for unsigned division. Signed division can be then defined > as in the standard using the unsigned division. > I totally agree with Armin. It's amazing that something that has been discussed so many times before is still here. I remember Robert Brummayer asking for the standard to be changed. That must have been 5 or 6 years ago. I believe it should be changed too. It sounds like almost everybody who has implemented a bitvector solver wants it to be changed. Yet, nothing ever gets done about it. It would be so simple to fix. Just fix the standard to adopt the semantics that most solvers implement. Armin makes a good case explaining why this is the simplest and most natural semantics. Bruno > Just for completeness here are the possible definitions for zero-division > I can think of: > > (1) a smt-lib-unsigned-div b = b ? a internal-unsigned=div b : zero_division (a) > (2) a smt-lib-unsigned-div b = b ? a internal-unsigned=div b : 0 > (3) a smt-lib-unsigned-div b = b ? a internal-unsigned=div b : global_constant > (4) a smt-lib-unsigned-div b = b ? a internal-unsigned=div b : local_constant > (5) a smt-lib-unsigned-div b = b ? a internal-unsigned=div b : ~0 > > I think (1) is over kill and will not work for many solvers that do not > support uninterpreted functions (note Boolector does, but I still think > it is overkill). > > (2) is not compatible with the most natural division circuit, but I can > imagine that this is something more compatible with other logics > (there is no maximal number / infinity for say integers or reals) > > (3) might be an approximation of (1) but it is not the same, since the standard > says (why?) that this zero_division should depend on the divisor, I would > still prefer (3) over (1), since it allows to eagerly bit-blast without > the need for an Ackermann reduction. > > (4) this might a natural way to encode it (introduce a new fresh constant > for every division), and is similar to what you would get internally when > doing uninterpreted functions anyhow, but otherwise I have no arguments > in favour of (4) > > (5) we should stick to this one .... > > Or as Morgan pointed out, remove benchmarks which depend on the > difference in these definitions ... > > > On Thu, Jun 12, 2014 at 2:55 PM, Tjark Weber <tja...@it...> wrote: >> Florian, >> >> On Thu, 2014-06-12 at 14:04 +0200, Florian Lapschies wrote: >>> Am I right to assume that the desired behavior is to allow all values in >>> the case of division by zero while ensuring that all instantiations of >>> bvudiv behave the same? >> >> (bvudiv s #b0) simply denotes an unknown value. Any interpretation is >> permitted, i.e., is a satisfying model (if there are no other >> constraints in the benchmark). Note that (bvudiv t #b0) may denote a >> different value if s <> t. >> >> Perhaps the note at the end of >> http://smtlib.cs.uiowa.edu/theories/FixedSizeBitVectors.smt2 >> explains this more clearly. >> >>> If yes, does this value have to be the same across all bitwidths? >> >> I believe there is no such constraint. >> >> Best, >> Tjark >> >> [Disclaimer: These comments are my own interpretation of the SMT-LIB >> standard and have not been coordinated with the other members of the >> SMT-COMP organizing committee.] >> > |