Thread: [Smtcomp-discussion] benchmarks involving divide by zero
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: David C. <dc...@gr...> - 2014-06-12 04:17:18
|
There was some discussion among some participants and adjustment of benchmark results for some QF_BV benchmarks that had divide-by-zero. This email is to make sure that all participants for whom this is relevant are OK with the outcome. If not, please respond promptly with your concerns. - David ------------------------------ part of the email thread I've updated new versions with corrected status attributes for the QF_BV/spear/w_get benchmarks (corrected according to the current SMT-LIB standard). As mentioned in the discussion thread, the other benchmarks in question appear to be labeled correctly - it is just that some solvers do not give the right answer. -Clark On Mon, Jun 9, 2014 at 3:27 PM, Morgan Deters <md...@cs... <mailto:md...@cs...>> wrote: On Mon, Jun 9, 2014 at 2:39 PM, Morgan Deters <md...@cs... <mailto:md...@cs...>> wrote: A follow-up. A recent build of Z3 (checked out from their git repository) now agrees with the SMT-EVAL versions of Boolector and CVC4 on the asp/TravellingSalesperson cases (answering sat). Modern CVC4 also gives sat (and verifies its model internally). On the spear/wgets, there is still disagreement. Modern CVC4 continues to say sat; I'm investigating. Liana Hadarean was able to investigate this matter further. We believe that the spear/wget differing results are due to bitvector division. Z3 can be made to leave division-by-zero uninterpreted with the parameter HI_DIV0=true, and when it does so, it agrees with CVC4's result. When CVC4 is made to interpret division-by-zero as a constant, it agrees with Z3. This means that some of the spear/wgets appear to have an incorrect status. Liana also confirmed my determination of the asp/TravellingSalesperson ones, showing that (the outdated) Z3 was giving incorrect results. Morgan -- Morgan Deters Senior Research Scientist Courant Institute of Mathematical Sciences 251 Mercer St., New York, NY 10012 md...@cs... <mailto:md...@cs...> - http://cs.nyu.edu/~mdeters/ <http://cs.nyu.edu/%7Emdeters/> |
From: Bruno D. <br...@cs...> - 2014-06-12 05:06:20
|
On 6/11/14, 9:17 PM, David Cok wrote: > There was some discussion among some participants and adjustment of > benchmark results for some QF_BV benchmarks that had divide-by-zero. > This email is to make sure that all participants for whom this is > relevant are OK with the outcome. If not, please respond promptly with > your concerns. > > - David > There have always been issues with divide by zero. Unless things have changed recently, the standard just says that (bvdiv x 0b000...) is undefined and can be an arbitrary value, but one must still ensure that (bvdiv ...) is a function. Is this still the case? The problem with this semantics is that it can't be implemented easily in solvers that use a pure 'bit-blasting' approach. To ensure that bvdiv is a function, you need support for congruence closure or some ugly hack of some kind. It is much simpler to assign a fixed value to (bvdiv x 0b000 ...) as in BTOR. So what does 'labeled correctly' mean in Clark's message? Will solvers that assign a fixed value to (bvdiv x 0b000...) be penalized? Bruno > ------------------------------ part of the email thread > > I've updated new versions with corrected status attributes for the > QF_BV/spear/w_get benchmarks (corrected according to the current SMT-LIB > standard). As mentioned in the discussion thread, the other benchmarks > in question appear to be labeled correctly - it is just that some > solvers do not give the right answer. > -Clark > > > On Mon, Jun 9, 2014 at 3:27 PM, Morgan Deters <md...@cs... > <mailto:md...@cs...>> wrote: > > On Mon, Jun 9, 2014 at 2:39 PM, Morgan Deters <md...@cs... > <mailto:md...@cs...>> wrote: > > A follow-up. > > A recent build of Z3 (checked out from their git repository) now > agrees with the SMT-EVAL versions of Boolector and CVC4 on the > asp/TravellingSalesperson cases (answering sat). Modern CVC4 > also gives sat (and verifies its model internally). > > On the spear/wgets, there is still disagreement. Modern CVC4 > continues to say sat; I'm investigating. > > > Liana Hadarean was able to investigate this matter further. We > believe that the spear/wget differing results are due to bitvector > division. Z3 can be made to leave division-by-zero uninterpreted > with the parameter HI_DIV0=true, and when it does so, it agrees with > CVC4's result. When CVC4 is made to interpret division-by-zero as a > constant, it agrees with Z3. > > This means that some of the spear/wgets appear to have an incorrect > status. > > Liana also confirmed my determination of the > asp/TravellingSalesperson ones, showing that (the outdated) Z3 was > giving incorrect results. > > Morgan > -- > Morgan Deters > Senior Research Scientist > Courant Institute of Mathematical Sciences > 251 Mercer St., New York, NY 10012 > md...@cs... <mailto:md...@cs...> - > http://cs.nyu.edu/~mdeters/ <http://cs.nyu.edu/%7Emdeters/> > > |
From: Armin B. <bi...@jk...> - 2014-06-12 06:17:49
|
FYI, I forwarded our other discussion to Bruno ... Armin On Thu, Jun 12, 2014 at 6:49 AM, Bruno Dutertre <br...@cs...> wrote: > On 6/11/14, 9:17 PM, David Cok wrote: >> >> There was some discussion among some participants and adjustment of >> benchmark results for some QF_BV benchmarks that had divide-by-zero. >> This email is to make sure that all participants for whom this is >> relevant are OK with the outcome. If not, please respond promptly with >> your concerns. >> >> - David >> > > There have always been issues with divide by zero. Unless things have > changed recently, the standard just says that (bvdiv x 0b000...) > is undefined and can be an arbitrary value, but one must still > ensure that (bvdiv ...) is a function. Is this still the case? > > The problem with this semantics is that it can't be implemented > easily in solvers that use a pure 'bit-blasting' approach. To > ensure that bvdiv is a function, you need support for congruence > closure or some ugly hack of some kind. It is much simpler to > assign a fixed value to (bvdiv x 0b000 ...) as in BTOR. > > So what does 'labeled correctly' mean in Clark's message? > Will solvers that assign a fixed value to (bvdiv x 0b000...) > be penalized? > > Bruno > > > >> ------------------------------ part of the email thread >> >> I've updated new versions with corrected status attributes for the >> QF_BV/spear/w_get benchmarks (corrected according to the current SMT-LIB >> standard). As mentioned in the discussion thread, the other benchmarks >> in question appear to be labeled correctly - it is just that some >> solvers do not give the right answer. >> -Clark >> >> >> On Mon, Jun 9, 2014 at 3:27 PM, Morgan Deters <md...@cs... >> <mailto:md...@cs...>> wrote: >> >> On Mon, Jun 9, 2014 at 2:39 PM, Morgan Deters <md...@cs... >> <mailto:md...@cs...>> wrote: >> >> A follow-up. >> >> A recent build of Z3 (checked out from their git repository) now >> agrees with the SMT-EVAL versions of Boolector and CVC4 on the >> asp/TravellingSalesperson cases (answering sat). Modern CVC4 >> also gives sat (and verifies its model internally). >> >> On the spear/wgets, there is still disagreement. Modern CVC4 >> continues to say sat; I'm investigating. >> >> >> Liana Hadarean was able to investigate this matter further. We >> believe that the spear/wget differing results are due to bitvector >> division. Z3 can be made to leave division-by-zero uninterpreted >> with the parameter HI_DIV0=true, and when it does so, it agrees with >> CVC4's result. When CVC4 is made to interpret division-by-zero as a >> constant, it agrees with Z3. >> >> This means that some of the spear/wgets appear to have an incorrect >> status. >> >> Liana also confirmed my determination of the >> asp/TravellingSalesperson ones, showing that (the outdated) Z3 was >> giving incorrect results. >> >> Morgan >> -- >> Morgan Deters >> Senior Research Scientist >> Courant Institute of Mathematical Sciences >> 251 Mercer St., New York, NY 10012 >> md...@cs... <mailto:md...@cs...> - >> http://cs.nyu.edu/~mdeters/ <http://cs.nyu.edu/%7Emdeters/> >> >> > |
From: Florian L. <fl...@in...> - 2014-06-12 10:32:01
|
After changing the satisfiability numerous solvers return wrong verdicts. Take for QF_BV/spear/wget_v1.10.2/src_wget_vc18196.smt2: Wrong are: * MathSAT5 5.2.12 * Boolector 1.6.0 * SONOLAR * STP (master branch) * Z3 (master branch) Correct are: * CVC4 1.3 Our solver SONOLAR returns the constant #xFF for a term (bvudiv x (_ bv0 8)). Z3 (master branch) and Boolector 1.6.0 have the same behavior. I do not understand why this behavior should not be compliant. The logic description of QF_BV merely states that bvudiv is "undefined if divisor is 0". Best regards, Florian On 06/12/2014 06:49 AM, Bruno Dutertre wrote: > On 6/11/14, 9:17 PM, David Cok wrote: >> There was some discussion among some participants and adjustment of >> benchmark results for some QF_BV benchmarks that had divide-by-zero. >> This email is to make sure that all participants for whom this is >> relevant are OK with the outcome. If not, please respond promptly with >> your concerns. >> >> - David >> > > There have always been issues with divide by zero. Unless things have > changed recently, the standard just says that (bvdiv x 0b000...) > is undefined and can be an arbitrary value, but one must still > ensure that (bvdiv ...) is a function. Is this still the case? > > The problem with this semantics is that it can't be implemented > easily in solvers that use a pure 'bit-blasting' approach. To > ensure that bvdiv is a function, you need support for congruence > closure or some ugly hack of some kind. It is much simpler to > assign a fixed value to (bvdiv x 0b000 ...) as in BTOR. > > So what does 'labeled correctly' mean in Clark's message? > Will solvers that assign a fixed value to (bvdiv x 0b000...) > be penalized? > > Bruno > > > >> ------------------------------ part of the email thread >> >> I've updated new versions with corrected status attributes for the >> QF_BV/spear/w_get benchmarks (corrected according to the current SMT-LIB >> standard). As mentioned in the discussion thread, the other benchmarks >> in question appear to be labeled correctly - it is just that some >> solvers do not give the right answer. >> -Clark >> >> >> On Mon, Jun 9, 2014 at 3:27 PM, Morgan Deters <md...@cs... >> <mailto:md...@cs...>> wrote: >> >> On Mon, Jun 9, 2014 at 2:39 PM, Morgan Deters <md...@cs... >> <mailto:md...@cs...>> wrote: >> >> A follow-up. >> >> A recent build of Z3 (checked out from their git repository) now >> agrees with the SMT-EVAL versions of Boolector and CVC4 on the >> asp/TravellingSalesperson cases (answering sat). Modern CVC4 >> also gives sat (and verifies its model internally). >> >> On the spear/wgets, there is still disagreement. Modern CVC4 >> continues to say sat; I'm investigating. >> >> >> Liana Hadarean was able to investigate this matter further. We >> believe that the spear/wget differing results are due to bitvector >> division. Z3 can be made to leave division-by-zero uninterpreted >> with the parameter HI_DIV0=true, and when it does so, it agrees with >> CVC4's result. When CVC4 is made to interpret division-by-zero as a >> constant, it agrees with Z3. >> >> This means that some of the spear/wgets appear to have an incorrect >> status. >> >> Liana also confirmed my determination of the >> asp/TravellingSalesperson ones, showing that (the outdated) Z3 was >> giving incorrect results. >> >> Morgan >> -- >> Morgan Deters >> Senior Research Scientist >> Courant Institute of Mathematical Sciences >> 251 Mercer St., New York, NY 10012 >> md...@cs... <mailto:md...@cs...> - >> http://cs.nyu.edu/~mdeters/ <http://cs.nyu.edu/%7Emdeters/> >> >> > > |
From: Tjark W. <tja...@it...> - 2014-06-12 11:42:16
|
Florian, On Thu, 2014-06-12 at 12:31 +0200, Florian Lapschies wrote: > Our solver SONOLAR returns the constant #xFF for a term (bvudiv x (_ bv0 > 8)). Z3 (master branch) and Boolector 1.6.0 have the same behavior. > I do not understand why this behavior should not be compliant. The logic > description of QF_BV merely states that bvudiv is "undefined if divisor > is 0". Clearly, undefined does not imply that its value is #xFF. Hence, making that assumption in your solver is unsound. Best, Tjark |
From: Florian L. <fl...@in...> - 2014-06-12 12:05:50
|
On 06/12/2014 01:42 PM, Tjark Weber wrote: > Florian, > > On Thu, 2014-06-12 at 12:31 +0200, Florian Lapschies wrote: >> Our solver SONOLAR returns the constant #xFF for a term (bvudiv x (_ bv0 >> 8)). Z3 (master branch) and Boolector 1.6.0 have the same behavior. >> I do not understand why this behavior should not be compliant. The logic >> description of QF_BV merely states that bvudiv is "undefined if divisor >> is 0". > Clearly, undefined does not imply that its value is #xFF. Hence, making > that assumption in your solver is unsound. > > Best, > Tjark 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? If yes, does this value have to be the same across all bitwidths? I fear that this is not easily fixed until the deadline. Without having inspected the benchmarks in question, if a benchmark's status depends on division by zero is this not most likely a modeling error? Best, Florian |
From: Tjark W. <tja...@it...> - 2014-06-12 12:55:28
|
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.] |
From: Armin B. <arm...@gm...> - 2014-06-12 12:59:24
|
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. 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.] > |
From: Trevor H. <tre...@ya...> - 2014-06-13 00:31:38
|
To make more explicit a point that Armin alludes to, because of the definition of the signed division-like operations in the current semantics, it's necessary to enforce constraints between the signed/unsigned division-like functions. For instance between signed and unsigned division, so this is unsatisfiable: (assert (not (= (bvudiv #x0 #x0) (bvsdiv #x0 #x0)))) ;Signed division and unsigned division must return the same result whenever the values are positive. Likewise it's necessary to enforce constraints between the same function with different operands. For example, (-5/0) must evaluate to the negative of (5/0), so this is unsatisfiable: (assert (and (= (bvsdiv #x5 #x0) #x1) (= (bvsdiv #xb #x0) #x1))) Personally, I find the current semantics onerous because they limit my choices for implementing modulus,remainder and signed division - so ignore them. Trevor On Thursday, 12 June 2014 10:59 PM, Armin Biere <arm...@gm...> 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. > >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.] >> > > > |
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.] >> > |
From: Alberto G. <gr...@fb...> - 2014-06-12 15:44:51
|
Hi all, > 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. If more support is needed for this to be approved, count me in. A. |
From: Alberto G. <gr...@fb...> - 2014-06-12 12:03:20
|
> After changing the satisfiability numerous solvers return wrong verdicts. > Take for QF_BV/spear/wget_v1.10.2/src_wget_vc18196.smt2: > Wrong are: > * MathSAT5 5.2.12 > * Boolector 1.6.0 > * SONOLAR > * STP (master branch) > * Z3 (master branch) > Correct are: > * CVC4 1.3 > > Our solver SONOLAR returns the constant #xFF for a term (bvudiv x (_ bv0 > 8)). Z3 (master branch) and Boolector 1.6.0 have the same behavior. MathSAT too, FWIW. > I do not understand why this behavior should not be compliant. The logic > description of QF_BV merely states that bvudiv is "undefined if divisor > is 0". Agreed (although MathSAT is not competing this year, but the division by zero issue is annoying regardless of SMT-COMP...) Alberto |
From: Mate S. <soo...@gm...> - 2014-06-12 12:33:23
Attachments:
signature.asc
|
Dear All, On 06/12/2014 01:36 PM, Alberto Griggio wrote: >> After changing the satisfiability numerous solvers return wrong verdicts. >> Take for QF_BV/spear/wget_v1.10.2/src_wget_vc18196.smt2: >> Wrong are: >> * MathSAT5 5.2.12 >> * Boolector 1.6.0 >> * SONOLAR >> * STP (master branch) >> * Z3 (master branch) >> Correct are: >> * CVC4 1.3 >> >> Our solver SONOLAR returns the constant #xFF for a term (bvudiv x (_ bv0 >> 8)). Z3 (master branch) and Boolector 1.6.0 have the same behavior. > > MathSAT too, FWIW. > >> I do not understand why this behavior should not be compliant. The logic >> description of QF_BV merely states that bvudiv is "undefined if divisor >> is 0". STP can even crash on this: https://github.com/stp/stp/issues/106 due to the undefinedness. The issue can be easily fixed, but as the discussion there shows, nobody really knows what to do. Would be nice to know what is the 'correct' behaviour where the SMT community defines what is correct. Cheers, Mate |
From: Florian L. <fl...@in...> - 2014-06-12 12:27:18
|
> > I've updated new versions with corrected status attributes for the > QF_BV/spear/w_get benchmarks (corrected according to the current > SMT-LIB standard). As mentioned in the discussion thread, the other > benchmarks in question appear to be labeled correctly - it is just > that some solvers do not give the right answer. > -Clark > I searched my SMT-COMP mails that I received the last couple of days and can't find any information about these other benchmarks. Have the authors of these solvers been contacted? Best regards, Florian |
From: David C. <dc...@gr...> - 2014-06-12 14:57:12
|
Florian - you are correct that some of the email on this topic in the last few days did not go to all participants. That is why I sent my email last evening to be sure there were no surprises to anyone. I discovered the problem in running some preliminary runs with historical solvers over the past week and Clark and Morgan did some detailed work to understand what the issue was. It appears to me that (a) SMT-LIB is well-defined on this point, (b) there is still some theoretical discussion happening, (c) not all solvers have adapted to the specific definitions in SMT-LIB, and (d) we are just three days away from the deadline, so it is unreasonable to expect major changes in existing tools. Thus, as lead organizer, I am inclined to propose that the benchmarks at issue be recused from the competition. - I'm willing to hear discussion pro and con on that point. - I also need to know which benchmarks are the ones at issue. David On 6/12/2014 8:26 AM, Florian Lapschies wrote: > > >> >> I've updated new versions with corrected status attributes for the >> QF_BV/spear/w_get benchmarks (corrected according to the current >> SMT-LIB standard). As mentioned in the discussion thread, the other >> benchmarks in question appear to be labeled correctly - it is just >> that some solvers do not give the right answer. >> -Clark >> > > I searched my SMT-COMP mails that I received the last couple of days > and can't find any information about these other benchmarks. Have the > authors of these solvers been contacted? > > Best regards, > Florian |
From: Clark B. <ba...@cs...> - 2014-06-12 16:03:57
|
Hi all, I agree with David that the best thing to do is to remove the offending benchmarks. For a subset of the benchmarks, I believe we already have a list from previous competitions (Morgan?). For newer benchmarks, we will have to find a way to determine this. As for changing the standard, I suggest this be brought up at the SMT workshop during the SMT-LIB discussion. As there seems to be some consensus, this will make a strong case for change. -Clark On Thu, Jun 12, 2014 at 7:57 AM, David Cok <dc...@gr...> wrote: > Florian - you are correct that some of the email on this topic in the > last few days did not go to all participants. That is why I sent my email > last evening to be sure there were no surprises to anyone. I discovered the > problem in running some preliminary runs with historical solvers over the > past week and Clark and Morgan did some detailed work to understand what > the issue was. > > It appears to me that (a) SMT-LIB is well-defined on this point, (b) there > is still some theoretical discussion happening, (c) not all solvers have > adapted to the specific definitions in SMT-LIB, and (d) we are just three > days away from the deadline, so it is unreasonable to expect major changes > in existing tools. > > Thus, as lead organizer, I am inclined to propose that the benchmarks at > issue be recused from the competition. > - I'm willing to hear discussion pro and con on that point. > - I also need to know which benchmarks are the ones at issue. > > David > > > > On 6/12/2014 8:26 AM, Florian Lapschies wrote: > > > > > I've updated new versions with corrected status attributes for the > QF_BV/spear/w_get benchmarks (corrected according to the current SMT-LIB > standard). As mentioned in the discussion thread, the other benchmarks in > question appear to be labeled correctly - it is just that some solvers do > not give the right answer. > -Clark > > > I searched my SMT-COMP mails that I received the last couple of days and > can't find any information about these other benchmarks. Have the authors > of these solvers been contacted? > > Best regards, > Florian > > > |
From: Tjark W. <tja...@it...> - 2014-06-12 20:42:21
|
On Thu, 2014-06-12 at 09:03 -0700, Clark Barrett wrote: > As for changing the standard, I suggest this be brought up at the SMT > workshop during the SMT-LIB discussion. As there seems to be some > consensus, this will make a strong case for change. The discussion so far was very much from a solver developer's point of view. The user perspective is a bit different. In application contexts, bit-vector division by 0 may have undefined results. The current semantics is the closest we can come to modeling this in the total logic of SMT-LIB. Defining, e.g., bv_div x x00 = xFF turns this equation into an assumption that the application context must satisfy. Otherwise, any unsatisfiability result (e.g., any SMT-based verification of some algorithm) may be unsound. If even solver developers are sometimes not aware of the precise semantics of bit-vector division (as this thread has shown), we should not expect most users of SMT solvers to be aware of such an assumption. Thus, for every solver developer whose life would be easier with such an assumption, there will be n users who are unaware that they are building unsound models. This will cause pain (rejected papers, crashing rockets, ...) sooner or later. Just my two cents. Best, Tjark |
From: Armin B. <arm...@gm...> - 2014-06-13 12:57:50
|
I tend to disagree here, since why should 'undefined' mean that it is defined to return always the same value? For instance, signed integer overflow gives undefined behaviour in C, but actually 'undefined' means that the compiler can do what it wants (everytime such an overflow occurs). In order to make sure you meet the specific semantics of your application, you have to change the encoding anyhow. Armin On Thu, Jun 12, 2014 at 10:42 PM, Tjark Weber <tja...@it...> wrote: > On Thu, 2014-06-12 at 09:03 -0700, Clark Barrett wrote: > >> As for changing the standard, I suggest this be brought up at the SMT >> workshop during the SMT-LIB discussion. As there seems to be some >> consensus, this will make a strong case for change. > > The discussion so far was very much from a solver developer's point of > view. The user perspective is a bit different. > > In application contexts, bit-vector division by 0 may have undefined > results. The current semantics is the closest we can come to modeling > this in the total logic of SMT-LIB. > > Defining, e.g., bv_div x x00 = xFF turns this equation into an > assumption that the application context must satisfy. Otherwise, any > unsatisfiability result (e.g., any SMT-based verification of some > algorithm) may be unsound. > > If even solver developers are sometimes not aware of the precise > semantics of bit-vector division (as this thread has shown), we should > not expect most users of SMT solvers to be aware of such an assumption. > > Thus, for every solver developer whose life would be easier with such > an assumption, there will be n users who are unaware that they are > building unsound models. This will cause pain (rejected papers, > crashing rockets, ...) sooner or later. > > Just my two cents. > > Best, > Tjark > > |
From: Tjark W. <tja...@it...> - 2014-06-13 16:13:35
|
On Fri, 2014-06-13 at 14:57 +0200, Armin Biere wrote: > I tend to disagree here, since why should 'undefined' mean that > it is defined to return always the same value? For instance, > signed integer overflow gives undefined behaviour in C, but actually > 'undefined' means that the compiler can do what it wants (everytime > such an overflow occurs). In order to make sure you meet the > specific semantics of your application, you have to change the > encoding anyhow. This is true for C, of course. I don't think it is very fortunate, and if anything, I think it is an argument for an even *weaker* semantics of bv_div. But as mentioned, the current semantics is the closest we can come to modeling undefinedness in the total logic of SMT-LIB. Best, Tjark |
From: Bruno D. <br...@cs...> - 2014-06-13 17:34:55
|
On 06/13/2014 09:13 AM, Tjark Weber wrote: > On Fri, 2014-06-13 at 14:57 +0200, Armin Biere wrote: >> I tend to disagree here, since why should 'undefined' mean that >> it is defined to return always the same value? For instance, >> signed integer overflow gives undefined behaviour in C, but actually >> 'undefined' means that the compiler can do what it wants (everytime >> such an overflow occurs). In order to make sure you meet the >> specific semantics of your application, you have to change the >> encoding anyhow. > > This is true for C, of course. I don't think it is very fortunate, and > if anything, I think it is an argument for an even *weaker* semantics > of bv_div. But as mentioned, the current semantics is the closest we > can come to modeling undefinedness in the total logic of SMT-LIB. > > Best, > Tjark > 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. 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? 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. Bruno |
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 |