Re: [Smtcomp-discussion] benchmarks involving divide by zero
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Tjark W. <tja...@it...> - 2014-06-23 11:41:08
|
Bruno, On Fri, 2014-06-13 at 10:33 -0700, Bruno Dutertre wrote: > 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. I agree. > 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? Nobody, of course. At present, users who want (bvdiv x 0x000) = 0xfff can easily assert this. But it makes little sense, other than for implementation reasons, to impose this equality on every user. > 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. This -- users who want something else can easily encode it -- is true no matter how bvdiv is defined. But for users to provide their own encoding, they must be aware of the issue in the first place. For the soundness of models that unwary users build, it is much safer to have a weak semantics by default than to have one that makes potentially surprising assumptions about a corner case. Of course, I fully understand your argument that the current semantics is awkward to implement and basically requires UF support. Best, Tjark |