smtcomp-discussion Mailing List for SMTCOMP (Page 4)
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
You can subscribe to this list here.
2014 |
Jan
(4) |
Feb
(11) |
Mar
|
Apr
(18) |
May
(104) |
Jun
(124) |
Jul
|
Aug
(2) |
Sep
|
Oct
|
Nov
(1) |
Dec
|
---|---|---|---|---|---|---|---|---|---|---|---|---|
2015 |
Jan
|
Feb
(4) |
Mar
(8) |
Apr
|
May
(4) |
Jun
(10) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2016 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2017 |
Jan
|
Feb
|
Mar
(8) |
Apr
|
May
|
Jun
(1) |
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
2018 |
Jan
|
Feb
|
Mar
(2) |
Apr
(2) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
From: David C. <dc...@gr...> - 2014-06-16 13:34:04
|
It is reasonable to compare against the last stable release anyway. Thanks, - David On 6/16/2014 9:21 AM, Tjark Weber wrote: > David, Aaron, > > I can run jobs now. The problem may have been caused by me specifying > invalid input for the seed value before. (If this is indeed the case, > http 500 is not the most helpful error message.) > > Aaron -- the seed value is disregarded by the "SMT-COMP 2014 Scrambler" > pre-processor. This is expected, as our current pre-processor script is > only passing $1 (i.e., the name of the benchmark file) to the actual > scrambler. How exactly is the job's seed value supplied to the > pre-processor? (The user manual appears silent about this, which is > understandable, of course.) > > Aaron -- it appears that the "solver summary" still counts > starexec-unknown as a wrong result. (I suppose this is a known issue. > In any case, it is not critical.) > > David -- I am afraid I failed to wrap the latest nightly build of Z3 > for StarExec. I tried to supply all needed libraries but only got to a > point where there is no output from the solver at all (rather than an > error message), which makes further debugging tricky. Since (1) Z3 is > running non-competitively anyway and (2) it appears that there has not > been an official (stable) release of Z3 since 2012, I suggest we simply > run the SMT-EVAL-2013 version of Z3 again for comparison. I have linked > this version to the Solvers-Preliminary space. > > Best, > Tjark > > |
From: David C. <dc...@gr...> - 2014-06-16 13:32:28
|
OK - we'll see if this can be sorted out today. - David On 6/16/2014 9:27 AM, Tjark Weber wrote: > David, > > On Mon, 2014-06-16 at 09:20 -0400, David Cok wrote: >> I successfully ran jobs using the scrambler and giving it a seed last >> night. Whether it did any scrambling or not I do not know, but the >> solvers did not complain. > It does scrambling, but using time(0) as its seed, rather than the job > seed that you supplied. > > Best, > Tjark > > |
From: Tjark W. <tja...@it...> - 2014-06-16 13:27:35
|
David, On Mon, 2014-06-16 at 09:20 -0400, David Cok wrote: > I successfully ran jobs using the scrambler and giving it a seed last > night. Whether it did any scrambling or not I do not know, but the > solvers did not complain. It does scrambling, but using time(0) as its seed, rather than the job seed that you supplied. Best, Tjark |
From: Tjark W. <tja...@it...> - 2014-06-16 13:21:51
|
David, Aaron, I can run jobs now. The problem may have been caused by me specifying invalid input for the seed value before. (If this is indeed the case, http 500 is not the most helpful error message.) Aaron -- the seed value is disregarded by the "SMT-COMP 2014 Scrambler" pre-processor. This is expected, as our current pre-processor script is only passing $1 (i.e., the name of the benchmark file) to the actual scrambler. How exactly is the job's seed value supplied to the pre-processor? (The user manual appears silent about this, which is understandable, of course.) Aaron -- it appears that the "solver summary" still counts starexec-unknown as a wrong result. (I suppose this is a known issue. In any case, it is not critical.) David -- I am afraid I failed to wrap the latest nightly build of Z3 for StarExec. I tried to supply all needed libraries but only got to a point where there is no output from the solver at all (rather than an error message), which makes further debugging tricky. Since (1) Z3 is running non-competitively anyway and (2) it appears that there has not been an official (stable) release of Z3 since 2012, I suggest we simply run the SMT-EVAL-2013 version of Z3 again for comparison. I have linked this version to the Solvers-Preliminary space. Best, Tjark |
From: David C. <dc...@gr...> - 2014-06-16 13:21:04
|
I successfully ran jobs using the scrambler and giving it a seed last night. Whether it did any scrambling or not I do not know, but the solvers did not complain. - David On 6/15/2014 4:13 PM, Tjark Weber wrote: > On Sun, 2014-06-15 at 07:28 -0400, David Cok wrote: >> PS: One more item >> Tjark - finish wrapping Z3 > I am afraid I still cannot create jobs on StarExec at the moment; I > only get "http 500 - internal server error" when I try. > > Alas, I cannot test the new seed feature or my latest attempt to wrap > Z3 until this has been fixed. > > Best, > Tjark > > |
From: David C. <dc...@gr...> - 2014-06-16 13:19:20
|
David, Tjark - Sorry I sent this unilaterally. I gave us some breathing room, and solver authors were worried that they had not been able to test. - David -------- Original Message -------- Subject: application track - deadline extended Date: Sun, 15 Jun 2014 22:36:45 -0400 From: David Cok <dc...@gr...> To: Clark Barrett <ba...@cs...>, Morgan Deters <md...@cs...>, Mohammad Abdul Aziz <moh...@gm...>, Armin Biere <bi...@jk...>, Ain...@jk..., Mat...@jk..., Juergen Christ <ch...@in...>, Florian Lapschies <fl...@in...>, Trevor Alexander HANSEN <th...@cs...>, Antti Hyvärinen <ant...@gm...>, Sharygina Natasha <nat...@us...>, Pascal Fontaine <pas...@lo...>, David Deharbe <dav...@lo...>, Bruno Dutertre <br...@cs...>, Hristina Palikareva <h.p...@im...>, cor...@cs..., rgo...@gm..., Mate Soos <soo...@gm...>, Alberto Griggio <gr...@fb...>, ma...@fb..., Carsten Fuhs <c....@cs...>, Cristian Cadar <c....@im...>, Jochen Hoenicke <hoe...@in...> We don't yet have the application track infrastructure ready, so no one has been able to test with it, so we will extend the deadline a week (to June 22) for the final solvers for the (demonstration) application track. - David, for the organizers |
From: Aaron S. <aar...@ui...> - 2014-06-16 02:24:10
|
Yes, we are going to do a system reset in the morning (GMT+5). Before that I hope Tjark can complete his tests. Please wait for my signal, hopefully just in the early afternoon. Aaron On Sun 15 Jun 2014 09:14:05 PM CDT, David Cok wrote: > Aaron - are you still planning to do system refresh in the morning? > Should we wit for your signal to start competition jobs? Or is any > time after 9am OK? > > - David > > On 6/15/2014 9:12 PM, Aaron Stump wrote: >> Hi, Tjark. I am not sure what the problem is but making sure you >> guys can get started ASAP (hopefully tomorrow as planned) will be my >> top priority tomorrow. Sorry for this problem. >> >> Aaron >> >> >> On Sun, Jun 15, 2014 at 3:13 PM, Tjark Weber <tja...@it... >> <mailto:tja...@it...>> wrote: >> >> On Sun, 2014-06-15 at 07:28 -0400, David Cok wrote: >> > PS: One more item >> > Tjark - finish wrapping Z3 >> >> I am afraid I still cannot create jobs on StarExec at the moment; I >> only get "http 500 - internal server error" when I try. >> >> Alas, I cannot test the new seed feature or my latest attempt to wrap >> Z3 until this has been fixed. >> >> Best, >> Tjark >> >> >> > |
From: David C. <dc...@gr...> - 2014-06-16 02:14:24
|
Aaron - are you still planning to do system refresh in the morning? Should we wit for your signal to start competition jobs? Or is any time after 9am OK? - David On 6/15/2014 9:12 PM, Aaron Stump wrote: > Hi, Tjark. I am not sure what the problem is but making sure you guys > can get started ASAP (hopefully tomorrow as planned) will be my top > priority tomorrow. Sorry for this problem. > > Aaron > > > On Sun, Jun 15, 2014 at 3:13 PM, Tjark Weber <tja...@it... > <mailto:tja...@it...>> wrote: > > On Sun, 2014-06-15 at 07:28 -0400, David Cok wrote: > > PS: One more item > > Tjark - finish wrapping Z3 > > I am afraid I still cannot create jobs on StarExec at the moment; I > only get "http 500 - internal server error" when I try. > > Alas, I cannot test the new seed feature or my latest attempt to wrap > Z3 until this has been fixed. > > Best, > Tjark > > > |
From: Aaron S. <aar...@gm...> - 2014-06-16 01:41:46
|
Hi, Tjark. I just tried creating a job on StarExec without a problem. Can you tell me more about the job you were trying to create where you got the error message? I have moved 10 nodes over to SMTCOMP.q from all.q for your testing, and will be moving a bunch more over tomorrow, of course. Cheers, Aaron On Sun 15 Jun 2014 08:12:47 PM CDT, Aaron Stump wrote: > Hi, Tjark. I am not sure what the problem is but making sure you guys > can get started ASAP (hopefully tomorrow as planned) will be my top > priority tomorrow. Sorry for this problem. > > Aaron > > > On Sun, Jun 15, 2014 at 3:13 PM, Tjark Weber <tja...@it... > <mailto:tja...@it...>> wrote: > > On Sun, 2014-06-15 at 07:28 -0400, David Cok wrote: > > PS: One more item > > Tjark - finish wrapping Z3 > > I am afraid I still cannot create jobs on StarExec at the moment; I > only get "http 500 - internal server error" when I try. > > Alas, I cannot test the new seed feature or my latest attempt to wrap > Z3 until this has been fixed. > > Best, > Tjark > > > |
From: Aaron S. <aar...@ui...> - 2014-06-16 01:12:56
|
Hi, Tjark. I am not sure what the problem is but making sure you guys can get started ASAP (hopefully tomorrow as planned) will be my top priority tomorrow. Sorry for this problem. Aaron On Sun, Jun 15, 2014 at 3:13 PM, Tjark Weber <tja...@it...> wrote: > On Sun, 2014-06-15 at 07:28 -0400, David Cok wrote: > > PS: One more item > > Tjark - finish wrapping Z3 > > I am afraid I still cannot create jobs on StarExec at the moment; I > only get "http 500 - internal server error" when I try. > > Alas, I cannot test the new seed feature or my latest attempt to wrap > Z3 until this has been fixed. > > Best, > Tjark > > > |
From: Tjark W. <tja...@it...> - 2014-06-15 20:13:53
|
On Sun, 2014-06-15 at 07:28 -0400, David Cok wrote: > PS: One more item > Tjark - finish wrapping Z3 I am afraid I still cannot create jobs on StarExec at the moment; I only get "http 500 - internal server error" when I try. Alas, I cannot test the new seed feature or my latest attempt to wrap Z3 until this has been fixed. Best, Tjark |
From: David C. <dc...@gr...> - 2014-06-15 12:14:35
|
PS: Even one more DCok - work out the BV benchmarks to exclude as a result of the discussion on div-by-zero On 6/15/2014 7:28 AM, David Cok wrote: > PS: One more item > > Tjark - finish wrapping Z3 > > On 6/14/2014 10:12 PM, David Cok wrote: >> David, Tjark, >> >> Thanks for all your work to date. >> - I created sample selections and spaces with David's programs >> - With Clark doing much of the work, I've validated that we have a >> working postprocessor >> - The SL community has their benchmarks and preprocessors ready >> >> We're almost ready: >> - Tjark - let me know as soon as you are confident the scramble is >> working as a preprocessor >> - David [as a competitor] I need from you the final set of logics in >> which you are participating and your final solver >> - I have a bit of work to finish on the difficulty computations >> - I will be accumulating the final solvers on Sunday as they are >> submitted >> - I will set up the spaces and jobs as soon as we get a seed on >> Monday morning >> - I have a bit of work to do on the display of results (accumulating >> across heaps) >> >> Then: >> - I will be monitoring the jobs and adding heats as time is available >> - Tjark: we'll have time then to complete the work on the application >> executor >> >> Later there will be some presentation and report preparation to do. >> >> - David >> > |
From: David C. <dc...@gr...> - 2014-06-15 11:29:00
|
PS: One more item Tjark - finish wrapping Z3 On 6/14/2014 10:12 PM, David Cok wrote: > David, Tjark, > > Thanks for all your work to date. > - I created sample selections and spaces with David's programs > - With Clark doing much of the work, I've validated that we have a > working postprocessor > - The SL community has their benchmarks and preprocessors ready > > We're almost ready: > - Tjark - let me know as soon as you are confident the scramble is > working as a preprocessor > - David [as a competitor] I need from you the final set of logics in > which you are participating and your final solver > - I have a bit of work to finish on the difficulty computations > - I will be accumulating the final solvers on Sunday as they are > submitted > - I will set up the spaces and jobs as soon as we get a seed on Monday > morning > - I have a bit of work to do on the display of results (accumulating > across heaps) > > Then: > - I will be monitoring the jobs and adding heats as time is available > - Tjark: we'll have time then to complete the work on the application > executor > > Later there will be some presentation and report preparation to do. > > - David > |
From: David D. <dav...@lo...> - 2014-06-15 09:53:54
|
On Jun 15, 2014, at 4:12 AM, David Cok <dc...@gr...> wrote: > - David [as a competitor] I need from you the final set of logics in > which you are participating and your final solver The final set of logics is: ALIA, AUFLIA, AUFLIRA, LIA, LRA, QF_AUFLIA, QF_IDL, QF_LIA, QF_LRA, QF_RDL, QF_UF, QF_UFIDL, QF_UFLIA, QF_UFLRA, UF, UFLIA, UFLRA. If you do not hear from us until the deadline, the solver id is 1188. But we are using the remaining available time to prepare a newer version so, unless the results are not satisfying, this is not the final solver. -- David. |
From: David C. <dc...@gr...> - 2014-06-15 02:12:54
|
David, Tjark, Thanks for all your work to date. - I created sample selections and spaces with David's programs - With Clark doing much of the work, I've validated that we have a working postprocessor - The SL community has their benchmarks and preprocessors ready We're almost ready: - Tjark - let me know as soon as you are confident the scramble is working as a preprocessor - David [as a competitor] I need from you the final set of logics in which you are participating and your final solver - I have a bit of work to finish on the difficulty computations - I will be accumulating the final solvers on Sunday as they are submitted - I will set up the spaces and jobs as soon as we get a seed on Monday morning - I have a bit of work to do on the display of results (accumulating across heaps) Then: - I will be monitoring the jobs and adding heats as time is available - Tjark: we'll have time then to complete the work on the application executor Later there will be some presentation and report preparation to do. - David |
From: David C. <dc...@gr...> - 2014-06-15 01:53:38
|
SL-COMP Competitors: There has been some debugging and correction (ongoing) of the postprocessors for SMT-COMP. We will be using the 'SMT2 results conserv new' postprocessor as it appears to be the most robust and correct of the postprocessors: it detects sat/unsat/unknown in the solver output and ignores success, producing a StarExec result of sat/unsat/starexec-unknown in the job-pairs. That matches the rules. It is also a bit more lenient in that it will ignore other output that does not contain sat/unsat/unknown. A caution however: if the postprocessor detects, say, both 'unsat' and 'sat' in the output, it will declare the result starexec-unknown. There still is a bug in the display of results in the job summaries. In particular starexec-unknown results are counted as wrong. That bug is expected to be fixed early this coming week and should not impede the beginning of competition. - David |
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-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: 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: 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: 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: 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: 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: 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: 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 |