smtcomp-discussion Mailing List for SMTCOMP
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: Tjark W. <tja...@it...> - 2018-04-07 11:36:27
|
Dear Ahmed and Alberto, On Wed, 2018-04-04 at 15:06 +0200, Ahmed Irfan wrote: > Let us know how to proceed with the submission of the transcendental benchmarks. Detailed instructions for benchmark submission to SMT-LIB may be found here: https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-tmp/benchmarks-pending/blob/master/README.md Best, Tjark |
From: Ahmed I. <ir...@fb...> - 2018-04-04 13:28:21
|
Dear SMT-COMP Organizers, We are planning to submit MathSAT to SMT-COMP'18 for competing in the divisions of quantifier-free nonlinear theories and their combination with other quantifier-free theories. Moreover, we are also interested in the new theory of the reals with transcendental functions. To this extent, we have the transcendental benchmarks that we used in our CADE'17 paper "Satisfiability Modulo Transcendental Functions via Incremental Linearization". In addition to those, we can also generate some more transcendental benchmarks from the paper "SMT-based Analysis of Switching Multi-Domain Linear Kirchhoff Networks". Let us know how to proceed with the submission of the transcendental benchmarks. Best Regards, Ahmed and Alberto. -- -- Le informazioni contenute nella presente comunicazione sono di natura privata e come tali sono da considerarsi riservate ed indirizzate esclusivamente ai destinatari indicati e per le finalità strettamente legate al relativo contenuto. Se avete ricevuto questo messaggio per errore, vi preghiamo di eliminarlo e di inviare una comunicazione all’indirizzo e-mail del mittente. -- The information transmitted is intended only for the person or entity to which it is addressed and may contain confidential and/or privileged material. If you received this in error, please contact the sender and delete the material. |
From: Carsten F. <ca...@dc...> - 2018-03-16 17:24:24
|
Dear SMT-COMP'18 organisers, First of all, many thanks for running the competition! Tool competitions like this (and the I/O format standardisation that they necessitate) really make the corresponding research and tools more accessible to external users. I have a comment on the following: > - Certificates, trophies, awards: Past competitions have been > somewhat unceremonious. What would be good ways to increase > ceremony and recognition for winning solvers? How should > trophies or other prizes be funded? Even awarding certificates that are printed on paper (at negligible cost) may be beneficial. Imagine that you are a postdoc developing an SMT solver, and you are preparing a job talk for an academic position. In that situation, it can be very handy if you have a visual way to communicate your achievements, say via a slide with an official certificate stating that your SMT solver scored highest at the recent SMT-COMP. The academics in the audience (who come from backgrounds all over computer science) may have no idea of what this strange "SMT" thing is, but they will recognise an award from a tool competition when they see one ... This may actually also benefit the SMT community as a whole. As far as I recall, such certificates were handed out to category winners at SMT-COMP 2014, when SMT-COMP was part of the FLoC Olympic Games 2014. I think that this was a great idea, and I would like to encourage doing so also at SMT-COMP 2018! (This suggestion is independent from having further ceremony e.g. at the SMT workshop, where such awards could be handed over to the authors of the winning tools.) Best regards, Carsten On 16.03.2018 16:30, Tjark Weber wrote: > ====================================================================== > > 13th International Satisfiability Modulo Theories Competition > (SMT-COMP'18) > > July 12-13, 2018 > Oxford, UK > > CALL FOR COMMENTS > CALL FOR BENCHMARKS > PRELIMINARY CALL FOR SOLVERS > > ====================================================================== > > SMT-COMP is the annual competition among Satisfiability Modulo Theories > (SMT) solvers. The goals of SMT-COMP are to spur solver advances, > collect benchmarks, and encourage adoption of the SMT-LIB standard, > through friendly competition. > > SMT-COMP'18 will end in time to be described and the results announced > at the SMT Workshop (July 12-13), which is affiliated with the > International Joint Conference on Automated Reasoning (IJCAR 2018), > part of the Federated Logic Conference (FLoC 2018). > > SMT-COMP'18 is organized under the direction of the SMT Steering > committee. The organizing team for SMT-COMP'18 is > > . Matthias Heizmann - University of Freiburg, Germany > . Aina Niemetz - Stanford University, USA > . Giles Reger - University of Manchester, UK > . Tjark Weber - Uppsala University, Sweden > > This is a call for three things: > > > CALL FOR COMMENTS: > > The organizing team is preparing the schedule and rules for 2018. Any > comments you may have to improve the competition over past years or to > redirect its focus are welcome and will be considered by the team. We > particularly appreciate comments received until April 8, 2018. > > For SMT-COMP'18, we are especially interested in comments regarding: > > - Certificates, trophies, awards: Past competitions have been > somewhat unceremonious. What would be good ways to increase > ceremony and recognition for winning solvers? How should > trophies or other prizes be funded? > > - Scope: New SMT-LIB theories for strings and for reals with > transcendental functions are currently in preparation. Are > corresponding benchmarks and sufficiently stable solver > implementations available for SMT-COMP to feature these as > (experimental) divisions in 2018? Should the scope or emphasis > of the competition be adapted in other ways? > > > CALL FOR BENCHMARKS: > > The competition is enhanced by new sets of benchmarks to add to those > already in use (and used in past competitions). A selection of > benchmarks in various categories is used for the competition. > > If you have benchmarks that you think would be useful to SMT-LIB and > SMT-COMP (and may be made public), please let us know as soon as > possible, even if the material is not quite ready. We will work in > close cooperation with the SMT-LIB maintainers to integrate such > benchmarks into the SMT-LIB. The deadline for submission of new > benchmarks to be used in the 2018 competition is > > *** April 8, 2018. *** > > > PRELIMINARY CALL FOR SOLVERS: > > A submission deadline for solvers will be announced along with the > rules. However, it is useful to the organizing team to know in advance > which and how many solvers may be entering. If you have not submitted > a solver before, or if you think there may be unusual circumstances, > we request that you let us know at your earliest convenience if you > think you may be submitting one or more solvers to SMT-COMP'18. > > > COMMUNICATION: > > The competition website will be at www.smtcomp.org. > > Public email regarding the competition may be sent to > smt...@cs.... > > Announcements will be sent to both smt...@cs... and > smt...@go.... > > Non-confidential email to the organizers may be sent to > smt...@li.... > > Sincerely, > The organizing team > > > _______________________________________________ > SMT-COMP mailing list > SMT...@cs... > https://cs.nyu.edu/mailman/listinfo/smt-comp > -- Carsten Fuhs Birkbeck, University of London Department of Computer Science and Information Systems http://www.dcs.bbk.ac.uk/~carsten/ |
From: Tjark W. <tja...@it...> - 2018-03-16 16:30:23
|
====================================================================== 13th International Satisfiability Modulo Theories Competition (SMT-COMP'18) July 12-13, 2018 Oxford, UK CALL FOR COMMENTS CALL FOR BENCHMARKS PRELIMINARY CALL FOR SOLVERS ====================================================================== SMT-COMP is the annual competition among Satisfiability Modulo Theories (SMT) solvers. The goals of SMT-COMP are to spur solver advances, collect benchmarks, and encourage adoption of the SMT-LIB standard, through friendly competition. SMT-COMP'18 will end in time to be described and the results announced at the SMT Workshop (July 12-13), which is affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2018), part of the Federated Logic Conference (FLoC 2018). SMT-COMP'18 is organized under the direction of the SMT Steering committee. The organizing team for SMT-COMP'18 is . Matthias Heizmann - University of Freiburg, Germany . Aina Niemetz - Stanford University, USA . Giles Reger - University of Manchester, UK . Tjark Weber - Uppsala University, Sweden This is a call for three things: CALL FOR COMMENTS: The organizing team is preparing the schedule and rules for 2018. Any comments you may have to improve the competition over past years or to redirect its focus are welcome and will be considered by the team. We particularly appreciate comments received until April 8, 2018. For SMT-COMP'18, we are especially interested in comments regarding: - Certificates, trophies, awards: Past competitions have been somewhat unceremonious. What would be good ways to increase ceremony and recognition for winning solvers? How should trophies or other prizes be funded? - Scope: New SMT-LIB theories for strings and for reals with transcendental functions are currently in preparation. Are corresponding benchmarks and sufficiently stable solver implementations available for SMT-COMP to feature these as (experimental) divisions in 2018? Should the scope or emphasis of the competition be adapted in other ways? CALL FOR BENCHMARKS: The competition is enhanced by new sets of benchmarks to add to those already in use (and used in past competitions). A selection of benchmarks in various categories is used for the competition. If you have benchmarks that you think would be useful to SMT-LIB and SMT-COMP (and may be made public), please let us know as soon as possible, even if the material is not quite ready. We will work in close cooperation with the SMT-LIB maintainers to integrate such benchmarks into the SMT-LIB. The deadline for submission of new benchmarks to be used in the 2018 competition is *** April 8, 2018. *** PRELIMINARY CALL FOR SOLVERS: A submission deadline for solvers will be announced along with the rules. However, it is useful to the organizing team to know in advance which and how many solvers may be entering. If you have not submitted a solver before, or if you think there may be unusual circumstances, we request that you let us know at your earliest convenience if you think you may be submitting one or more solvers to SMT-COMP'18. COMMUNICATION: The competition website will be at www.smtcomp.org. Public email regarding the competition may be sent to smt...@cs.... Announcements will be sent to both smt...@cs... and smt...@go.... Non-confidential email to the organizers may be sent to smt...@li.... Sincerely, The organizing team |
From: Tjark W. <tja...@it...> - 2017-06-05 09:06:17
|
Dear all, To allow as many teams as possible to participate, we are extending the deadline for submission of (first versions of) solvers to SMT-COMP 2017 until *** Wednesday, June 7 *** (anywhere on earth). This deadline is strict. However, submitted solvers may be updated until June 18, 2017. Solvers must be made available on StarExec, and additional information must be provided to the competition organizers via the web form at https://goo.gl/forms/HL6rbOywqW4sFo1D2 Please see the competition rules at http://smtcomp.sourceforge.net/2017/rules17.pdf for further details. Thank you to everyone who submitted their solver(s) already! Best, Tjark |
From: Tjark W. <tja...@it...> - 2017-03-31 13:08:47
|
Andrew, On Thu, 2017-03-30 at 12:21 -0500, Andrew Reynolds wrote: > One point here is that the competition should encourage innovation. > So > if there is a difficult new logic (e.g. floating points or strings), > and I'd like to enter, but I'm not 100% confident in my solver for > that > logic, it still would be nice for me to be able to enter without > having > to risk the score for the logics where I am sure my solver is correct. Of course, I see your point. If you are only concerned about one or two logics, there is (usually) the option to enter the solver into these logics as non-competing. But in general, I think it makes sense that solver developers need to commit to a set of logics in advance. > The use case of randomly selecting a benchmark in any logic isn't very > interesting, in my opinion. The random choice is merely intended to model some real-world application that generates problems in logics A and B. (This is based on the assumption that SMT-LIB benchmarks in some sense approximate real-world problems, which is certainly debatable.) > Another option would be to multiply by something like -( #wrong / ( 1 > + #wrong ))*(weight of logic), where you'd get a factor -1/2, -2/3, > -3/4, ... as number of wrong benchmarks increase, but this is limited > by -1. In principle, other functions to compute the factor could perhaps also be considered, as long as they are (i) monotonic and (ii) take values between 0 and 1 (or -1, as the case may be). For instance, the function to compute the factor for correct answers is (#correct/#total)^2. Your proposals seem more appropriate though: they give a greater (negative) factor as soon as there is at least one incorrect answer, in line with the view that a solver shouldn't be used for a logic for which it isn't sound. I wonder how the "value" of a correct answer compares to the "cost" of an incorrect answer in a typical application of SMT solvers. It is hard to make this precise, of course, but my hunch is that the latter is typically far greater. Your original motivation to encourage innovation notwithstanding, to me this would suggest another factor (some constant > 1) to place more emphasis on negative scores for incorrect answers. I would also like to caution that the competition-wide ranking is in a sense comparing apples and oranges. As this discussion shows, mapping the performance of solvers that support very different logics to a single number necessarily comes with some challenges. Anyone interested in specific logics should probably look at the competition's results for those logics instead. Best, Tjark |
From: Andrew R. <and...@gm...> - 2017-03-30 17:21:53
|
Hi Tjark, On Mon, Mar 27, 2017 at 7:53 AM, Tjark Weber <tja...@it...> wrote: > Andrew, > > On Sun, 2017-03-26 at 18:03 -0500, Andrew Reynolds wrote: > > > On Fri, Mar 24, 2017 at 6:13 PM, Tjark Weber <tja...@it...> > > wrote: > > On the other hand, one might argue that an unsound solver > > should not be trusted in any division. [...] > > > > Here, I would argue that the implementation of SMT solvers tends to be > > fairly modular, meaning that if an SMT solver gets a wrong answer for > > logic A, then the bug is very likely in the component that > > specifically handles A, and the solver is likely still sound for > > everything besides A. [...] > > I agree with your point about modularity. But note that the solver's > (likely) soundness for everything besides A is only established in > hindsight, through the results of the competition. The issue, of > course, is that the solver was originally advertised as sound for > everything including A. > > Once the competition results are known, it is easy to turn a partially > unsound solver into a useful tool by restricting it to appropriate > logics. But it is hard to know in advance for which logics a solver is > (likely) sound if the developer's claims cannot be relied on. > > One point here is that the competition should encourage innovation. So if there is a difficult new logic (e.g. floating points or strings), and I'd like to enter, but I'm not 100% confident in my solver for that logic, it still would be nice for me to be able to enter without having to risk the score for the logics where I am sure my solver is correct. > > Let's consider another case: > > > Logic A, B with weights 1,1. > > Solver X gets 1 wrong answer in both A and B, it's total score is -1*1 > > + -1*1 = -2 > > Solver Y solves all benchmarks in A, but gets 4 wrong answers in B, > > its total score is 1 + -4*1 = -3 > > > Here, I would argue that Solver Y is the better solver: it is (likely) > > sound for logic A, whereas Solver X is definitely unsound for both A > > and B. > > Note that one could also argue the opposite point of view: suppose you > are asked to solve a benchmark that will be chosen at random from > SMT-LIB (including logics A and B) by applying one of these solvers. > (You'll have to take the solver's answer at face value.) Which solver > would you rather use, X or Y? > > The use case of randomly selecting a benchmark in any logic isn't very interesting, in my opinion. In practice, I should be able to select a solver based on the logic. So in this case I would be confident in solver Y for A, and if I had a problem in logic B, neither solver would be a good option. I wouldn't even necessarily say that Solver X is much better than Solver Y for logic B, despite the 4 vs 1 wrong answers, I wouldn't use either one. > > I do think it is very important, and I do believe that an unsound > > solver is worse than a solver that solves no benchmarks. My opposition > > is to multiplying by the #wrong benchmarks, since this skews the > > results unfairly. A punishment of -1*(weight of logic) is still very > > severe, but is more appropriate for overall score, in my opinion. > > I tend to agree that simply multiplying by #wrong benchmarks is > awkward: we already have a weight for each logic that takes the number > of benchmarks in that logic into account. > > I suspect the original motivation was to punish solvers that get many > benchmarks wrong more severely than solvers that get only a few > benchmarks wrong. This is easy to achieve for the division rankings, > but I am not sure whether this property is worth retaining for the > competition-wide ranking. Arguably, any solver that is unsound in some > division shouldn't be used to solve benchmarks from that division. > > Right, this is my point. Another option would be to multiply by something like -( #wrong / ( 1 + #wrong ))*(weight of logic), where you'd get a factor -1/2, -2/3, -3/4, ... as number of wrong benchmarks increase, but this is limited by -1. Let me know what you think. Cheers, Andy > Best, > Tjark > > > |
From: Tjark W. <tja...@it...> - 2017-03-27 12:53:14
|
Andrew, On Sun, 2017-03-26 at 18:03 -0500, Andrew Reynolds wrote: > On Fri, Mar 24, 2017 at 6:13 PM, Tjark Weber <tja...@it...> > wrote: > On the other hand, one might argue that an unsound solver > should not be trusted in any division. [...] > > Here, I would argue that the implementation of SMT solvers tends to be > fairly modular, meaning that if an SMT solver gets a wrong answer for > logic A, then the bug is very likely in the component that > specifically handles A, and the solver is likely still sound for > everything besides A. [...] I agree with your point about modularity. But note that the solver's (likely) soundness for everything besides A is only established in hindsight, through the results of the competition. The issue, of course, is that the solver was originally advertised as sound for everything including A. Once the competition results are known, it is easy to turn a partially unsound solver into a useful tool by restricting it to appropriate logics. But it is hard to know in advance for which logics a solver is (likely) sound if the developer's claims cannot be relied on. > Let's consider another case: > Logic A, B with weights 1,1. > Solver X gets 1 wrong answer in both A and B, it's total score is -1*1 > + -1*1 = -2 > Solver Y solves all benchmarks in A, but gets 4 wrong answers in B, > its total score is 1 + -4*1 = -3 > Here, I would argue that Solver Y is the better solver: it is (likely) > sound for logic A, whereas Solver X is definitely unsound for both A > and B. Note that one could also argue the opposite point of view: suppose you are asked to solve a benchmark that will be chosen at random from SMT-LIB (including logics A and B) by applying one of these solvers. (You'll have to take the solver's answer at face value.) Which solver would you rather use, X or Y? > I do think it is very important, and I do believe that an unsound > solver is worse than a solver that solves no benchmarks. My opposition > is to multiplying by the #wrong benchmarks, since this skews the > results unfairly. A punishment of -1*(weight of logic) is still very > severe, but is more appropriate for overall score, in my opinion. I tend to agree that simply multiplying by #wrong benchmarks is awkward: we already have a weight for each logic that takes the number of benchmarks in that logic into account. I suspect the original motivation was to punish solvers that get many benchmarks wrong more severely than solvers that get only a few benchmarks wrong. This is easy to achieve for the division rankings, but I am not sure whether this property is worth retaining for the competition-wide ranking. Arguably, any solver that is unsound in some division shouldn't be used to solve benchmarks from that division. Best, Tjark |
From: Mate S. <soo...@gm...> - 2017-03-26 23:35:00
|
Maybe I shouldn't interject here, but I think we could use a bit of fuzzing on SMT solvers. The year when STP had a bug, we learned our lesson and started using fuzzsmt (http://fmv.jku.at/fuzzsmt/). It generated a small instance that exposed the bug within about 3 minutes. It now runs on every push to the repo. Of course fuzzsmt doesn't expose all bugs, but it's a start. I personally also AFL-fuzz the underlying SAT solver, it catches some more. Running the fuzzsmt instances under valgrind (or clang's sanitizers) also helps, especially when it catches undefined behaviour (typically uninitialized var used to make a decision). There is probably some work missing on SMT fuzzers, though, maybe that could be encouraged? (Special track maybe?) It's actually hard to write them, see csmith ( https://embed.cs.utah.edu/csmith/ -- note, one of the authors, John Regehr was at CAV in 2016), and the number of papers that came out of that. C is a complicated language, though, but frankly, the SMT spec isn't exactly for the faint of heart, either. In the long run, I'd be good to make the solvers usable in the industry, and that means trust is really important, so maybe building tools&possibly also infrastructure for this could be interesting. There is already infrastructure for checking speed (starexec), so doing something similar for validity checking is not unimaginable. I guess what I'm saying is, instead of only punishing solvers that do the wrong thing, we could encourage to build tools and systems to make it easier to do the right thing. Just my 2 cents, Mate On 27 March 2017 at 00:03, Andrew Reynolds <and...@gm...> wrote: > Hi Tjark, > > On Fri, Mar 24, 2017 at 6:13 PM, Tjark Weber <tja...@it...> wrote: > >> Andrew, >> >> Thank you for your feedback! >> >> On Thu, 2017-03-16 at 10:38 -0500, Andrew Reynolds wrote: >> >> > Regarding disagreements between solvers, last year, as I recall, there >> > was a separate discussion period where most (or all) disagreements >> > between solvers were resolved e.g. a developer would say "my solver >> > was wrong for this one", etc. Perhaps the competition should: >> >> > - Run all benchmarks/solvers, note the set of unknown status >> > benchmarks D that two solvers disagree on. >> > - Have a rebuttal period where solver developers can justify their >> > answers for benchmarks in D. >> > - Based on discussion, set the status on benchmarks in D, and then >> > compute the final scores. >> >> I am concerned about some of the practical implications of this >> suggestion. Preliminary results would have to be available probably 1-2 >> weeks earlier than in the past (to allow sufficient time for the steps >> above); the competition would depend on status updates by the SMT-LIB >> maintainers in a time-critical fashion; and solvers would be run >> against one SMT-LIB release but scored against another. >> >> It's not impossible, of course. But given the size of the competition >> (with more than 200,000 benchmarks and 1.5 M job pairs in 2016), these >> issues have the potential to cause some headache. I would much prefer a >> simpler scoring solution that doesn't involve manual review. >> >> Right, I understand this would be a challenge. The proposal I mentioned > is more of a wish than a suggestion. :) > > >> > (4) Scoring: >> >> > One thing that has bothered me in previous competitions is how overall >> > scoring is computed with respect to wrong benchmarks. >> >> > Say I have logics A, B, C, D with weights 1, and I solve all >> > benchmarks in A,B,C, but I get 3 wrong benchmarks in D. Then my >> > overall score is: >> >> > 1 + 1 + 1 + -3*1 = 0 >> >> > I would prefer if wrong benchmarks were punished slightly less, so >> > that if a solver gets *any* number of wrong benchmarks in a logic, >> > then its overall score is negative of the weight of that logic, so >> > instead I'd have: >> >> > 1 + 1 + 1 + -1*1 = 2 >> >> On the other hand, one might argue that an unsound solver should not be >> trusted in any division. There is an even harsher alternative to the >> current scoring rule that has been considered before: to disqualify >> unsound solvers entirely. In other words, the current scoring rule >> already is a compromise. >> >> Here, I would argue that the implementation of SMT solvers tends to be > fairly modular, meaning that if an SMT solver gets a wrong answer for logic > A, then the bug is very likely in the component that specifically handles > A, and the solver is likely still sound for everything besides A. > Historically, this has been the case for CVC4. In my recollection: > > SMT comp 2012 CVC4 had a wrong answer in QF_BV related to an unsound > bit-vector rewrite, > SMT comp 2012 CVC4 had a wrong answer in QF_LIA related to a bug the > arithmetic theory solver, > SMT comp 2016 CVC4 had a wrong answer in QF_NIA related to the encoding of > QF_NIA constraints as QF_BV ones. > > In each of these cases, CVC4 was still (to my knowledge) sound for > everything besides the logics that had the bug. Of course this is not > guaranteed to be the case, there could be a solver with a bug that effects > all logics, but this is much less likely. > > Let's consider another case: > > Logic A, B with weights 1,1. > Solver X gets 1 wrong answer in both A and B, it's total score is -1*1 + > -1*1 = -2 > Solver Y solves all benchmarks in A, but gets 4 wrong answers in B, its > total score is 1 + -4*1 = -3 > > Here, I would argue that Solver Y is the better solver: it is (likely) > sound for logic A, whereas Solver X is definitely unsound for both A and > B. However, Solver X wins because it got lucky that only 1 benchmark > exercised its unsoundness in A and B, whereas Solver Y was unlucky and had > 4. > If instead we used a punishment of ( -1*weight ) for the logic regardless > of #wrong benchmarks, Solver Y would have a total score of 0, and Solver X > would still have -2, which I believe would be more appropriate. > > I would be interested to hear further opinions on this issue. How much >> emphasis should the competition place on soundness of solvers? >> >> > I do think it is very important, and I do believe that an unsound solver > is worse than a solver that solves no benchmarks. My opposition is to > multiplying by the #wrong benchmarks, since this skews the results > unfairly. A punishment of -1*(weight of logic) is still very severe, but is > more appropriate for overall score, in my opinion. > > Let me know what you think, > Andy > > > > >> Best, >> Tjark >> >> >> > > ------------------------------------------------------------ > ------------------ > Check out the vibrant tech community on one of the world's most > engaging tech sites, Slashdot.org! http://sdm.link/slashdot > _______________________________________________ > Smtcomp-discussion mailing list > Smt...@li... > https://lists.sourceforge.net/lists/listinfo/smtcomp-discussion > > |
From: Andrew R. <and...@gm...> - 2017-03-26 23:03:40
|
Hi Tjark, On Fri, Mar 24, 2017 at 6:13 PM, Tjark Weber <tja...@it...> wrote: > Andrew, > > Thank you for your feedback! > > On Thu, 2017-03-16 at 10:38 -0500, Andrew Reynolds wrote: > > > Regarding disagreements between solvers, last year, as I recall, there > > was a separate discussion period where most (or all) disagreements > > between solvers were resolved e.g. a developer would say "my solver > > was wrong for this one", etc. Perhaps the competition should: > > > - Run all benchmarks/solvers, note the set of unknown status > > benchmarks D that two solvers disagree on. > > - Have a rebuttal period where solver developers can justify their > > answers for benchmarks in D. > > - Based on discussion, set the status on benchmarks in D, and then > > compute the final scores. > > I am concerned about some of the practical implications of this > suggestion. Preliminary results would have to be available probably 1-2 > weeks earlier than in the past (to allow sufficient time for the steps > above); the competition would depend on status updates by the SMT-LIB > maintainers in a time-critical fashion; and solvers would be run > against one SMT-LIB release but scored against another. > > It's not impossible, of course. But given the size of the competition > (with more than 200,000 benchmarks and 1.5 M job pairs in 2016), these > issues have the potential to cause some headache. I would much prefer a > simpler scoring solution that doesn't involve manual review. > > Right, I understand this would be a challenge. The proposal I mentioned is more of a wish than a suggestion. :) > > (4) Scoring: > > > One thing that has bothered me in previous competitions is how overall > > scoring is computed with respect to wrong benchmarks. > > > Say I have logics A, B, C, D with weights 1, and I solve all > > benchmarks in A,B,C, but I get 3 wrong benchmarks in D. Then my > > overall score is: > > > 1 + 1 + 1 + -3*1 = 0 > > > I would prefer if wrong benchmarks were punished slightly less, so > > that if a solver gets *any* number of wrong benchmarks in a logic, > > then its overall score is negative of the weight of that logic, so > > instead I'd have: > > > 1 + 1 + 1 + -1*1 = 2 > > On the other hand, one might argue that an unsound solver should not be > trusted in any division. There is an even harsher alternative to the > current scoring rule that has been considered before: to disqualify > unsound solvers entirely. In other words, the current scoring rule > already is a compromise. > > Here, I would argue that the implementation of SMT solvers tends to be fairly modular, meaning that if an SMT solver gets a wrong answer for logic A, then the bug is very likely in the component that specifically handles A, and the solver is likely still sound for everything besides A. Historically, this has been the case for CVC4. In my recollection: SMT comp 2012 CVC4 had a wrong answer in QF_BV related to an unsound bit-vector rewrite, SMT comp 2012 CVC4 had a wrong answer in QF_LIA related to a bug the arithmetic theory solver, SMT comp 2016 CVC4 had a wrong answer in QF_NIA related to the encoding of QF_NIA constraints as QF_BV ones. In each of these cases, CVC4 was still (to my knowledge) sound for everything besides the logics that had the bug. Of course this is not guaranteed to be the case, there could be a solver with a bug that effects all logics, but this is much less likely. Let's consider another case: Logic A, B with weights 1,1. Solver X gets 1 wrong answer in both A and B, it's total score is -1*1 + -1*1 = -2 Solver Y solves all benchmarks in A, but gets 4 wrong answers in B, its total score is 1 + -4*1 = -3 Here, I would argue that Solver Y is the better solver: it is (likely) sound for logic A, whereas Solver X is definitely unsound for both A and B. However, Solver X wins because it got lucky that only 1 benchmark exercised its unsoundness in A and B, whereas Solver Y was unlucky and had 4. If instead we used a punishment of ( -1*weight ) for the logic regardless of #wrong benchmarks, Solver Y would have a total score of 0, and Solver X would still have -2, which I believe would be more appropriate. I would be interested to hear further opinions on this issue. How much > emphasis should the competition place on soundness of solvers? > > I do think it is very important, and I do believe that an unsound solver is worse than a solver that solves no benchmarks. My opposition is to multiplying by the #wrong benchmarks, since this skews the results unfairly. A punishment of -1*(weight of logic) is still very severe, but is more appropriate for overall score, in my opinion. Let me know what you think, Andy > Best, > Tjark > > > |
From: Tjark W. <tja...@it...> - 2017-03-24 23:13:26
|
Andrew, Thank you for your feedback! On Thu, 2017-03-16 at 10:38 -0500, Andrew Reynolds wrote: > Regarding disagreements between solvers, last year, as I recall, there > was a separate discussion period where most (or all) disagreements > between solvers were resolved e.g. a developer would say "my solver > was wrong for this one", etc. Perhaps the competition should: > - Run all benchmarks/solvers, note the set of unknown status > benchmarks D that two solvers disagree on. > - Have a rebuttal period where solver developers can justify their > answers for benchmarks in D. > - Based on discussion, set the status on benchmarks in D, and then > compute the final scores. I am concerned about some of the practical implications of this suggestion. Preliminary results would have to be available probably 1-2 weeks earlier than in the past (to allow sufficient time for the steps above); the competition would depend on status updates by the SMT-LIB maintainers in a time-critical fashion; and solvers would be run against one SMT-LIB release but scored against another. It's not impossible, of course. But given the size of the competition (with more than 200,000 benchmarks and 1.5 M job pairs in 2016), these issues have the potential to cause some headache. I would much prefer a simpler scoring solution that doesn't involve manual review. > (4) Scoring: > One thing that has bothered me in previous competitions is how overall > scoring is computed with respect to wrong benchmarks. > Say I have logics A, B, C, D with weights 1, and I solve all > benchmarks in A,B,C, but I get 3 wrong benchmarks in D. Then my > overall score is: > 1 + 1 + 1 + -3*1 = 0 > I would prefer if wrong benchmarks were punished slightly less, so > that if a solver gets *any* number of wrong benchmarks in a logic, > then its overall score is negative of the weight of that logic, so > instead I'd have: > 1 + 1 + 1 + -1*1 = 2 On the other hand, one might argue that an unsound solver should not be trusted in any division. There is an even harsher alternative to the current scoring rule that has been considered before: to disqualify unsound solvers entirely. In other words, the current scoring rule already is a compromise. I would be interested to hear further opinions on this issue. How much emphasis should the competition place on soundness of solvers? Best, Tjark |
From: Andrew R. <and...@gm...> - 2017-03-16 15:38:47
|
Hello organizers, I have the following opinions about the competition this year: (1) Unknown benchmarks I am in favor of including "unknown" status benchmarks in the competition. Regarding disagreements between solvers, last year, as I recall, there was a separate discussion period where most (or all) disagreements between solvers were resolved e.g. a developer would say "my solver was wrong for this one", etc. Perhaps the competition should: - Run all benchmarks/solvers, note the set of unknown status benchmarks D that two solvers disagree on. - Have a rebuttal period where solver developers can justify their answers for benchmarks in D. - Based on discussion, set the status on benchmarks in D, and then compute the final scores. There are a number of ways to determine which solver is correct, e.g. if A says "sat" and B says "unsat", then check if A also says "sat" for B's unsat core, B also says "unsat" for the benchmark + A's model. If the status cannot be resolved even after discussion, then the benchmark's status remains "unknown" and is not counted in the scoring. (2) Benchmark weighting The benchmark weighting scheme is fine, but I'd like if #solved benchmarks was also shown in the results tables e.g. on the pages http://smtcomp.sourceforge.net/2016/results-AUFLIRA.shtml?v=1467876482 in addition to "Correctly solved score". (3) Datatypes I am highly in favor of including datatypes in SMT LIB and SMT COMP. CVC4 has full support for datatypes in combination with all of its other theories. I have numerous benchmark sets involving datatypes that I've accumulated over the years that involve datatypes that I have been unable to add to SMT LIB due to lack of a standard. I can provide these if you want. (4) Scoring: One thing that has bothered me in previous competitions is how overall scoring is computed with respect to wrong benchmarks. Say I have logics A, B, C, D with weights 1, and I solve all benchmarks in A,B,C, but I get 3 wrong benchmarks in D. Then my overall score is: 1 + 1 + 1 + -3*1 = 0 I would prefer if wrong benchmarks were punished slightly less, so that if a solver gets *any* number of wrong benchmarks in a logic, then its overall score is negative of the weight of that logic, so instead I'd have: 1 + 1 + 1 + -1*1 = 2 I think this is better since it still punishes heavily for wrong benchmarks, but doesn't skew the results so that a solver's overall score can be entirely ruined by one logic. (Here, my solver was correct for A,B,C so I should be rewarded for that). I would also argue that a solver that gets 1 wrong benchmark is not much better than one that gets 3 wrong benchmarks, since both are unsound. I believe this would encourage more participation in logics. For instance, CVC4 may in the future get support for floating points, but we would be discouraged from entering QF_FP since there is a chance that a handful of wrong answers there could single-handedly negate our overall score. Cheers, Andrew Reynolds On Wed, Mar 15, 2017 at 9:46 AM, Tjark Weber <tja...@it...> wrote: > ====================================================================== > > 12th International Satisfiability Modulo Theories Competition > (SMT-COMP'17) > > July 23, 2017 > Heidelberg, Germany > > CALL FOR COMMENTS > CALL FOR BENCHMARKS > PRELIMINARY CALL FOR SOLVERS > > ====================================================================== > > SMT-COMP is the annual competition among Satisfiability Modulo Theories > (SMT) solvers. The goals of SMT-COMP are to spur solver advances, > collect benchmarks, and encourage adoption of the SMT-LIB standard, > through friendly competition. > > SMT-COMP'17 will end in time to be described and the results announced > at the SMT Workshop (July 22-23), which is affiliated with the > International Conference on Computer-Aided Verification (CAV 2017). > > SMT-COMP'17 is organized under the direction of the SMT Steering > committee. The organizing team for SMT-COMP'17 is > > . Matthias Heizmann - University of Freiburg, Germany > . Giles Reger - University of Manchester, UK > . Tjark Weber - Uppsala University, Sweden > > This is a call for three things: > > > CALL FOR COMMENTS: > > The organizing team is preparing the schedule and rules for 2017. > Any comments you may have to improve the competition over past years > or to redirect its focus are welcome and will be considered by the > team. We particularly appreciate comments received until > > *** March 31, 2017. *** > > For SMT-COMP'17, we are especially interested in comments regarding: > > - Benchmarks with unknown status: Previous SMT-COMPs have only used > benchmarks whose status (sat/unsat) was known. One might argue that > this favors imitation of existing solvers over innovation. Should > benchmarks with unknown status be used in the competition? If so, > how should answers for such benchmarks be scored? Can scoring for > one solver remain independent of the answers given by other solvers, > or should disagreements between solvers lead to negative scores for > a solver? > > - Benchmark weighting: To avoid over-representation of certain (large) > benchmark families, a weighting scheme for benchmarks was introduced > in 2016. This causes division scores to be real numbers rather than > simply an integer indicating the number of benchmarks solved, and > the winning solver in a division is (intentionally) no longer > necessarily the solver that solved the largest number of benchmarks. > Do the methodological benefits of this weighting scheme justify the > increased complexity in interpreting division scores? > > - Scope: The new (draft) version 2.6 of the SMT-LIB standard includes > support for algebraic datatypes. Are corresponding benchmarks and > sufficiently stable solver implementations available for SMT-COMP to > feature an (experimental) datatype division in 2017? Should the > scope or emphasis of the competition be adapted in other ways? > > > CALL FOR BENCHMARKS: > > The competition is enhanced by new sets of benchmarks to add to those > already in use (and used in past competitions). A selection of > benchmarks in various categories is used for the competition (according > to rules that are currently being revised). > > If you have benchmarks that you think would be useful to SMT-LIB and > SMT-COMP (and may be made public), please let us know as soon as > possible, even if the material is not quite ready. We will work in > close cooperation with the SMT-LIB maintainers to integrate such > benchmarks into the SMT-LIB in time to be taken into account for the > competition. The deadline for benchmarks to be used in the 2017 > competition will be announced when the schedule and rules are > finalized. > > > PRELIMINARY CALL FOR SOLVERS: > > A submission deadline for solvers will be announced along with the > rules. However, it is useful to the organizing team to know in advance > which and how many solvers may be entering. Thus we request that you > let us know at your earliest convenience if you think you may be > submitting one or more solvers to SMT-COMP'17; particularly if you > have not submitted a solver before, or if you think there may be > unusual circumstances. > > > COMMUNICATION: > > The competition web-site will be at www.smtcomp.org. > > Public email regarding the competition may be sent to > smt...@cs.... > > Announcements will be sent on both smt...@cs... and > sm...@cs.... > > Non-confidential email to the organizers may be sent to > smt...@li.... > > Sincerely, > The organizing team > > > _______________________________________________ > SMT-COMP mailing list > SMT...@cs... > http://cs.nyu.edu/mailman/listinfo/smt-comp > |
From: Tjark W. <tja...@it...> - 2017-03-15 15:06:01
|
====================================================================== 12th International Satisfiability Modulo Theories Competition (SMT-COMP'17) July 23, 2017 Heidelberg, Germany CALL FOR COMMENTS CALL FOR BENCHMARKS PRELIMINARY CALL FOR SOLVERS ====================================================================== SMT-COMP is the annual competition among Satisfiability Modulo Theories (SMT) solvers. The goals of SMT-COMP are to spur solver advances, collect benchmarks, and encourage adoption of the SMT-LIB standard, through friendly competition. SMT-COMP'17 will end in time to be described and the results announced at the SMT Workshop (July 22-23), which is affiliated with the International Conference on Computer-Aided Verification (CAV 2017). SMT-COMP'17 is organized under the direction of the SMT Steering committee. The organizing team for SMT-COMP'17 is . Matthias Heizmann - University of Freiburg, Germany . Giles Reger - University of Manchester, UK . Tjark Weber - Uppsala University, Sweden This is a call for three things: CALL FOR COMMENTS: The organizing team is preparing the schedule and rules for 2017. Any comments you may have to improve the competition over past years or to redirect its focus are welcome and will be considered by the team. We particularly appreciate comments received until *** March 31, 2017. *** For SMT-COMP'17, we are especially interested in comments regarding: - Benchmarks with unknown status: Previous SMT-COMPs have only used benchmarks whose status (sat/unsat) was known. One might argue that this favors imitation of existing solvers over innovation. Should benchmarks with unknown status be used in the competition? If so, how should answers for such benchmarks be scored? Can scoring for one solver remain independent of the answers given by other solvers, or should disagreements between solvers lead to negative scores for a solver? - Benchmark weighting: To avoid over-representation of certain (large) benchmark families, a weighting scheme for benchmarks was introduced in 2016. This causes division scores to be real numbers rather than simply an integer indicating the number of benchmarks solved, and the winning solver in a division is (intentionally) no longer necessarily the solver that solved the largest number of benchmarks. Do the methodological benefits of this weighting scheme justify the increased complexity in interpreting division scores? - Scope: The new (draft) version 2.6 of the SMT-LIB standard includes support for algebraic datatypes. Are corresponding benchmarks and sufficiently stable solver implementations available for SMT-COMP to feature an (experimental) datatype division in 2017? Should the scope or emphasis of the competition be adapted in other ways? CALL FOR BENCHMARKS: The competition is enhanced by new sets of benchmarks to add to those already in use (and used in past competitions). A selection of benchmarks in various categories is used for the competition (according to rules that are currently being revised). If you have benchmarks that you think would be useful to SMT-LIB and SMT-COMP (and may be made public), please let us know as soon as possible, even if the material is not quite ready. We will work in close cooperation with the SMT-LIB maintainers to integrate such benchmarks into the SMT-LIB in time to be taken into account for the competition. The deadline for benchmarks to be used in the 2017 competition will be announced when the schedule and rules are finalized. PRELIMINARY CALL FOR SOLVERS: A submission deadline for solvers will be announced along with the rules. However, it is useful to the organizing team to know in advance which and how many solvers may be entering. Thus we request that you let us know at your earliest convenience if you think you may be submitting one or more solvers to SMT-COMP'17; particularly if you have not submitted a solver before, or if you think there may be unusual circumstances. COMMUNICATION: The competition web-site will be at www.smtcomp.org. Public email regarding the competition may be sent to smt...@cs.... Announcements will be sent on both smt...@cs... and sm...@cs.... Non-confidential email to the organizers may be sent to smt...@li.... Sincerely, The organizing team |
From: Tjark W. <tja...@it...> - 2016-05-12 12:32:39
|
Dear all, Please remember that the deadline for submission of (first versions of) solvers to SMT-COMP 2016 is *** Sunday, May 15 *** (anywhere on earth). This deadline is strict. However, submitted solvers may be updated until May 29, 2016. Solvers must be made available on StarExec, and additional information must be provided to the competition organizers by email. In particular, we need to know in which tracks (main, application, unsat-core) and divisions (i.e., logics) the solver is competing. Please see the competition rules at http://smtcomp.sourceforge.net/2016/rules16.pdf for further details. Best, Tjark |
From: Tjark W. <tja...@it...> - 2016-02-16 14:45:16
|
====================================================================== 11th International Satisfiability Modulo Theories Competition (SMT-COMP'16) July 2, 2016 Coimbra, Portugal CALL FOR COMMENTS CALL FOR BENCHMARKS PRELIMINARY CALL FOR SOLVERS ====================================================================== SMT-COMP is the annual competition among Satisfiability Modulo Theories (SMT) solvers. The goals of SMT-COMP are to spur solver advances, collect benchmarks, and encourage adoption of the SMT-LIB standard, through friendly competition. SMT-COMP'16 will end in time to be described and the results announced at the SMT Workshop (July 1-2), which is affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016). SMT-COMP'16 is organized under the direction of the SMT Steering committee. The organizing team for SMT-COMP'16 is . Sylvain Conchon - Paris-Sud University, France . David Deharbe - Clearsy, France & Federal University of Rio Grande do Norte, Brazil . Tjark Weber - Uppsala University, Sweden This is a call for three things: CALL FOR COMMENTS: The organizing team is preparing the schedule and rules for 2016. Any comments you may have to improve the competition over past years or to redirect its focus are welcome and will be considered by the team. We particularly appreciate comments received until *** February 29, 2016. *** For SMT-COMP'16, we are especially interested in comments regarding: - Sequential vs. parallel performance: As in 2015, we plan to measure both CPU time and wall time. Solver developers are encouraged to prepare both sequential and parallel versions of their solvers. - Benchmark selection: We will likely have sufficient computational resources to run all solvers on all eligible benchmarks. Therefore, we are interested in proposals for weighing the results so as to avoid over-representation of certain (large) benchmark families. - Scope: We are considering to broaden the scope of SMT-COMP again. We might reinstate additional tracks, e.g., for unsat core extraction and proof-producing solvers. We are also considering a track that emphasizes fast answers, and would appreciate related scoring suggestions. CALL FOR BENCHMARKS: The competition is enhanced by new sets of benchmarks to add to those already in use (and used in past competitions). A selection of benchmarks in various categories is used for the competition (according to rules that are currently being revised). If you have benchmarks that you think would be useful to SMT-LIB and SMT-COMP (and may be made public), please let us know as soon as possible, even if the material is not quite ready. We will work in close cooperation with the SMT-LIB maintainers to include such benchmarks in the SMT-LIB in time to be taken into account for the competition. The deadline for benchmarks to be used in the 2016 competition will be announced when the schedule and rules are finalized. PRELIMINARY CALL FOR SOLVERS: A submission deadline for solvers will be announced along with the rules. However, it is useful to the organizing team to know in advance which and how many solvers may be entering. Thus we request that you let us know at your earliest convenience if you think you may be submitting one or more solvers to SMT-COMP'16, particularly if you think there may be unusual circumstances. COMMUNICATION: The competition web-site will be at www.smtcomp.org. Public email regarding the competition may be sent to smt...@cs.... Announcements will be sent on both smt...@cs... and sm...@cs.... Non-confidential email to the organizers may be sent to smt...@li.... Sincerely, The organizing team |
From: Christoph W. <cw...@mi...> - 2015-06-11 12:31:56
|
There's about an equal number of arguments for both sides in this discussion. My suggestion is to implement whichever is easiest to implement in your solver. We can then add a mandatory command line parameter. If that parameter is not set to any value, we will issue a warning about which semantics are being used and that the user has to set the option even if the default is the right choice. This way, we force the user to explicitly choose the semantics they want (and obviously if they don’t chose anything, they don't care), and we can throw an error if they chose an unsupported option. Cheers, Christoph Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB -----Original Message----- From: Tjark Weber [mailto:tja...@it...] Sent: 11 June 2015 09:15 To: Martin Brain Cc: Alberto Griggio; smt...@li...; smt-lib (sm...@cs...); Christoph Wintersteiger; Florian Lapschies; wa...@cc...; Pas...@in...; Schanda Florian; Philipp Ruemmer (phi...@it...) Subject: Re: [Smtcomp-discussion] FP demo track at SMT-COMP On Thu, 2015-06-11 at 08:34 +0100, Martin Brain wrote: > On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote: > > Fixing one return value while existing IEEE-compliant > > implementations return different values would be actively harmful in > > my opinion. It is foreseeable then that users will use fp.min to > > model IEEE min, that some (if not most) will be unaware of the > > subtle semantic difference, and that they will ultimately believe > > they've verified their code when it may well break on some architectures. > > I agree with you but note that there is a counter-argument that in the > situation you give, the current semantics will give spurious > counter-examples that cannot be executed on the target platform. I > guess it is personal taste depending on whether you feel it is better > to under or over approximate the behaviour of the system. My > reasoning was that all IEEE-754 compliant systems should be model of the theory. You are right. Do I prefer spurious counter-examples (which users will then look into, and which they can easily rule out with additional assumptions if they want to verify their code against a specific IEEE implementation) over unsound proofs (which users won't notice as unsound until their programs break in production)? Absolutely. Best, Tjark |
From: Tjark W. <tja...@it...> - 2015-06-11 08:15:28
|
On Thu, 2015-06-11 at 08:34 +0100, Martin Brain wrote: > On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote: > > Fixing one return value while existing IEEE-compliant implementations > > return different values would be actively harmful in my opinion. It is > > foreseeable then that users will use fp.min to model IEEE min, that > > some (if not most) will be unaware of the subtle semantic difference, > > and that they will ultimately believe they've verified their code when > > it may well break on some architectures. > > I agree with you but note that there is a counter-argument that in the > situation you give, the current semantics will give spurious > counter-examples that cannot be executed on the target platform. I > guess it is personal taste depending on whether you feel it is better to > under or over approximate the behaviour of the system. My reasoning was > that all IEEE-754 compliant systems should be model of the theory. You are right. Do I prefer spurious counter-examples (which users will then look into, and which they can easily rule out with additional assumptions if they want to verify their code against a specific IEEE implementation) over unsound proofs (which users won't notice as unsound until their programs break in production)? Absolutely. Best, Tjark |
From: Schanda F. <flo...@al...> - 2015-06-11 07:48:42
|
> On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > > Is it too late to ask for a change in the FP standard? Fixing one > return > > value for e.g. (fp.min -0 +0) would make life simpler without losing > > much IMHO, given that the underspecified semantics can still be > encoded > > if someone really wants that. What do people think? > > Fixing one return value while existing IEEE-compliant implementations > return different values would be actively harmful in my opinion. Yes, to add my "industry" voice to this, please keep it as is, that is unspecified. ;) This leaves it up to the tool vendor to specify it, if they happen to know. For example - if I remember right the intel manuals also do not specify what the hardware does. Although, if I remember right, it seems to behave consistently in that it always returns the second (or first?) argument. But fp.min returning -0 and fp.max returning +0 seems an equally likely implementation choice. In fact, I will add some benchmarks to my own testsuite to make sure this behaviour exists. It might all sound a bit silly, but it would be easy enough to construct a program that exploits this behaviour (convert floats to array of bytes) and we would get unsound proofs because of it! Florian |
From: Martin B. <mar...@cs...> - 2015-06-11 07:34:19
|
On Wed, 2015-06-10 at 21:09 +0200, Tjark Weber wrote: > On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > > Is it too late to ask for a change in the FP standard? Fixing one return > > value for e.g. (fp.min -0 +0) would make life simpler without losing > > much IMHO, given that the underspecified semantics can still be encoded > > if someone really wants that. What do people think? > > Fixing one return value while existing IEEE-compliant implementations > return different values would be actively harmful in my opinion. It is > foreseeable then that users will use fp.min to model IEEE min, that > some (if not most) will be unaware of the subtle semantic difference, > and that they will ultimately believe they've verified their code when > it may well break on some architectures. I agree with you but note that there is a counter-argument that in the situation you give, the current semantics will give spurious counter-examples that cannot be executed on the target platform. I guess it is personal taste depending on whether you feel it is better to under or over approximate the behaviour of the system. My reasoning was that all IEEE-754 compliant systems should be model of the theory. > For the competition, I think the best solution by far is to remove > affected benchmarks this year. Are there any other floating-point > operators with underspecified semantics that should be removed as well? (_ fp.to_ubv m), (_ fp.to_sbv m) and fp.to_real are all underspecified for the 'special values' such as +/-Inf and NaN. The first two are also underspecified for all values outside of the current range because, again, there are significant differences in hardware. Cheers, - Martin |
From: Tjark W. <tja...@it...> - 2015-06-10 19:09:41
|
On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > Is it too late to ask for a change in the FP standard? Fixing one return > value for e.g. (fp.min -0 +0) would make life simpler without losing > much IMHO, given that the underspecified semantics can still be encoded > if someone really wants that. What do people think? Fixing one return value while existing IEEE-compliant implementations return different values would be actively harmful in my opinion. It is foreseeable then that users will use fp.min to model IEEE min, that some (if not most) will be unaware of the subtle semantic difference, and that they will ultimately believe they've verified their code when it may well break on some architectures. For the competition, I think the best solution by far is to remove affected benchmarks this year. Are there any other floating-point operators with underspecified semantics that should be removed as well? Best, Tjark |
From: Martin B. <mar...@cs...> - 2015-06-10 17:19:44
|
On Wed, 2015-06-10 at 17:26 +0200, Alberto Griggio wrote: > Hello all, > > >> So far, none of the submissions to SMT-COMP 2015 have select QF_FP or > >> QF_BVFP as categories they would like to take part in: > >> > >> http://smtcomp.sourceforge.net/2015/participants.shtml > >> > >> We would like to run the floating-point demo track alongside the other > >> competition track, i.e., starting June 14. So, if you would like to > >> participate, please let us know as soon as possible. As Tjark said, if > >> we don’t hear from you, your solver(s) will not take part. > >> > >> If you want to take a look at the latest benchmarks before committing to > >> it, they are available on starexec in root/SMT/SMT-LIB > >> benchmarks/2015-06-01/non-incremental/QF_FP and …/QF_BVFP. > > > > I was planning to submit. As I told Tjark, I did not understand that the > > general SMTCOMP deadline was meant also for the FP demo tracks. If I'm > > still on time, I'll try to submit mathsat by june 14. > > I have a follow-up question about this. If I understand correctly, > fp.min and fp.max are underspecified in the current standard, in the > case the inputs are +0 and -0. Yes. This is only the cases min(+0,-0) and min(-0,+0) (and the corresponding max cases). > The reference paper [BTRW15] argues that > this is necessary to be fully compliant with IEEE. The specific clause is: <quote> minNum(x, y) is the canonicalized number x if x < y, y if y < x, the canonicalized number if one operand is a number and the other a quiet NaN. Otherwise it is either x or y, canonicalized (this means results might differ among implementations). </quote> Canonicalisation only applies in the case of decimal floating-point which SMT-LIB doesn't (currently) support. My understanding of this is that max and min were not included in the 1985 version of IEEE-754 and that different implementators made different assumptions about what they should do. IIRC the x87 and SSE units on Intel chips have different behaviour, likewise: !(x < y) ? x : y; !(x > y) ? y : x; have different behaviour around +0/-0. > To me, this seems > like an unnecessary complication (for the same reason, I think > bit-vector division by 0 should be specified). Regardless of this, > however, I found at least one benchmark that seems to be misclassified > (there might be more): > > wintersteiger/min/2066309/min-has-no-other-solution-13472.smt2 > > Is it too late to ask for a change in the FP standard? Fixing one return > value for e.g. (fp.min -0 +0) would make life simpler without losing > much IMHO, given that the underspecified semantics can still be encoded > if someone really wants that. What do people think? I, personally, think that we should keep the underspecified semantics as something similar will be needed for converting from float to signed and unsigned integers so it's not as if changing max/min will remove the need to support these. Benchmarks that use this aspect ... should probably be treated like bit-vector divide by 0. Cheers, - Martin |
From: Christoph W. <cw...@mi...> - 2015-06-10 15:39:07
|
Regarding fp.min/fp,max in the benchmarks and what's implemented in Z3, please see also this discussion: https://github.com/Z3Prover/z3/issues/68 I agree that we have to fix those to some value, or maybe the second argument. Users can always wrap them in ITEs that select whatever they want for those cases (and internally most of us would do the same kind of wrapping inside our solvers anyways). For the demo track, I think it would be fair to simply exclude that benchmark, so we don't have to find a community consensus right away. Cheers, Christoph Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB -----Original Message----- From: Alberto Griggio [mailto:gr...@fb...] Sent: 10 June 2015 16:27 To: Christoph Wintersteiger; smt...@li...; smt-lib (sm...@cs...) Cc: Martin Brain; Schanda Florian; Florian Lapschies; Pas...@in...; Philipp Ruemmer (phi...@it...); wa...@cc... Subject: Re: FP demo track at SMT-COMP Hello all, >> So far, none of the submissions to SMT-COMP 2015 have select QF_FP or >> QF_BVFP as categories they would like to take part in: >> >> http://smtcomp.sourceforge.net/2015/participants.shtml >> >> We would like to run the floating-point demo track alongside the >> other competition track, i.e., starting June 14. So, if you would >> like to participate, please let us know as soon as possible. As Tjark >> said, if we don't hear from you, your solver(s) will not take part. >> >> If you want to take a look at the latest benchmarks before committing >> to it, they are available on starexec in root/SMT/SMT-LIB >> benchmarks/2015-06-01/non-incremental/QF_FP and .../QF_BVFP. > > I was planning to submit. As I told Tjark, I did not understand that > the general SMTCOMP deadline was meant also for the FP demo tracks. If > I'm still on time, I'll try to submit mathsat by june 14. I have a follow-up question about this. If I understand correctly, fp.min and fp.max are underspecified in the current standard, in the case the inputs are +0 and -0. The reference paper [BTRW15] argues that this is necessary to be fully compliant with IEEE. To me, this seems like an unnecessary complication (for the same reason, I think bit-vector division by 0 should be specified). Regardless of this, however, I found at least one benchmark that seems to be misclassified (there might be more): wintersteiger/min/2066309/min-has-no-other-solution-13472.smt2 Is it too late to ask for a change in the FP standard? Fixing one return value for e.g. (fp.min -0 +0) would make life simpler without losing much IMHO, given that the underspecified semantics can still be encoded if someone really wants that. What do people think? Alberto [BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic Technical Report, 2015. |
From: Alberto G. <gr...@fb...> - 2015-06-10 15:27:01
|
Hello all, >> So far, none of the submissions to SMT-COMP 2015 have select QF_FP or >> QF_BVFP as categories they would like to take part in: >> >> http://smtcomp.sourceforge.net/2015/participants.shtml >> >> We would like to run the floating-point demo track alongside the other >> competition track, i.e., starting June 14. So, if you would like to >> participate, please let us know as soon as possible. As Tjark said, if >> we don’t hear from you, your solver(s) will not take part. >> >> If you want to take a look at the latest benchmarks before committing to >> it, they are available on starexec in root/SMT/SMT-LIB >> benchmarks/2015-06-01/non-incremental/QF_FP and …/QF_BVFP. > > I was planning to submit. As I told Tjark, I did not understand that the > general SMTCOMP deadline was meant also for the FP demo tracks. If I'm > still on time, I'll try to submit mathsat by june 14. I have a follow-up question about this. If I understand correctly, fp.min and fp.max are underspecified in the current standard, in the case the inputs are +0 and -0. The reference paper [BTRW15] argues that this is necessary to be fully compliant with IEEE. To me, this seems like an unnecessary complication (for the same reason, I think bit-vector division by 0 should be specified). Regardless of this, however, I found at least one benchmark that seems to be misclassified (there might be more): wintersteiger/min/2066309/min-has-no-other-solution-13472.smt2 Is it too late to ask for a change in the FP standard? Fixing one return value for e.g. (fp.min -0 +0) would make life simpler without losing much IMHO, given that the underspecified semantics can still be encoded if someone really wants that. What do people think? Alberto [BTRW15] Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic Technical Report, 2015. |
From: Alberto G. <gr...@fb...> - 2015-06-10 13:24:20
|
Hi, > Hi all, > > So far, none of the submissions to SMT-COMP 2015 have select QF_FP or > QF_BVFP as categories they would like to take part in: > > http://smtcomp.sourceforge.net/2015/participants.shtml > > We would like to run the floating-point demo track alongside the other > competition track, i.e., starting June 14. So, if you would like to > participate, please let us know as soon as possible. As Tjark said, if > we don’t hear from you, your solver(s) will not take part. > > If you want to take a look at the latest benchmarks before committing to > it, they are available on starexec in root/SMT/SMT-LIB > benchmarks/2015-06-01/non-incremental/QF_FP and …/QF_BVFP. I was planning to submit. As I told Tjark, I did not understand that the general SMTCOMP deadline was meant also for the FP demo tracks. If I'm still on time, I'll try to submit mathsat by june 14. Alberto |
From: Christoph W. <cw...@mi...> - 2015-06-10 13:08:35
|
Hi all, So far, none of the submissions to SMT-COMP 2015 have select QF_FP or QF_BVFP as categories they would like to take part in: http://smtcomp.sourceforge.net/2015/participants.shtml We would like to run the floating-point demo track alongside the other competition track, i.e., starting June 14. So, if you would like to participate, please let us know as soon as possible. As Tjark said, if we don't hear from you, your solver(s) will not take part. If you want to take a look at the latest benchmarks before committing to it, they are available on starexec in root/SMT/SMT-LIB benchmarks/2015-06-01/non-incremental/QF_FP and .../QF_BVFP. Thanks, Christoph Tjark Weber tjark.weber at it.uu.se <mailto:smt-comp%40cs.nyu.edu?Subject=Re%3A%20%5BSMT-COMP%5D%20Floating-Point%20Divisions&In-Reply-To=%3C1433712417.3478.33.camel%40it.uu.se%3E> Sun Jun 7 17:26:57 EDT 2015 * Previous message: [SMT-COMP] SMT-COMP 2015: Benchmarks and Tools Available <http://cs.nyu.edu/pipermail/smt-comp/2015/000327.html> * Next message: [SMT-COMP] SMT-COMP 2015: exit Command Optional <http://cs.nyu.edu/pipermail/smt-comp/2015/000329.html> * Messages sorted by: [ date ]<http://cs.nyu.edu/pipermail/smt-comp/2015/date.html#328> [ thread ]<http://cs.nyu.edu/pipermail/smt-comp/2015/thread.html#328> [ subject ]<http://cs.nyu.edu/pipermail/smt-comp/2015/subject.html#328> [ author ]<http://cs.nyu.edu/pipermail/smt-comp/2015/author.html#328> ________________________________ Dear SMT-COMP participants, The recent 2015-06-01 release of SMT-LIB features floating-point benchmarks in two new logics, QF_BVFP and QF_FP. Accordingly, SMT-COMP 2015 will have two experimental floating-point divisions. Please let us know before the final solver deadline on June 14 if you wish to enter your solver(s) into one or both of QF_BVFP and QF_FP. We will not enter your solver(s) into these divisions unless we hear from you, even if you previously entered your solver into "all divisions." Best, Tjark Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter<http://research.microsoft.com/people/cwinter> [MSFT_logo_Gray DE sized SIG1.png] Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB |