smtcomp-discussion — Public mailing list to contact the SMT-COMP organizers

Re: [Smtcomp-discussion] MathSAT Solver and Transcendental Benchmarks

[Tjark W. <tja...@it...>]

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

[Smtcomp-discussion] MathSAT Solver and Transcendental Benchmarks

[Ahmed I. <ir...@fb...>]

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.

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2018: Call for Comments, Benchmarks, Solvers

[Carsten F. <ca...@dc...>]

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/
	

[Smtcomp-discussion] SMT-COMP 2018: Call for Comments, Benchmarks, Solvers

[Tjark W. <tja...@it...>]

======================================================================

    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

[Smtcomp-discussion] SMT-COMP 2017: Final Call for Solvers

[Tjark W. <tja...@it...>]

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

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Tjark W. <tja...@it...>]

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

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Andrew R. <and...@gm...>]

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
>
>
>

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Tjark W. <tja...@it...>]

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

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Mate S. <soo...@gm...>]

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
>
>

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Andrew R. <and...@gm...>]

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
>
>
>

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Tjark W. <tja...@it...>]

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

Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Andrew R. <and...@gm...>]

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
>

[Smtcomp-discussion] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers

[Tjark W. <tja...@it...>]

======================================================================

    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

[Smtcomp-discussion] SMT-COMP 2016: Final Call for Solvers

[Tjark W. <tja...@it...>]

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

[Smtcomp-discussion] SMT-COMP 2016: Call for Comments, Benchmarks, Solvers

[Tjark W. <tja...@it...>]

======================================================================

    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

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Christoph W. <cw...@mi...>]

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

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Tjark W. <tja...@it...>]

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

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Schanda F. <flo...@al...>]

> 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

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Martin B. <mar...@cs...>]

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

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Tjark W. <tja...@it...>]

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

Re: [Smtcomp-discussion] [SMT-LIB] FP demo track at SMT-COMP

[Martin B. <mar...@cs...>]

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

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Christoph W. <cw...@mi...>]

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.

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Alberto G. <gr...@fb...>]

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.

Re: [Smtcomp-discussion] FP demo track at SMT-COMP

[Alberto G. <gr...@fb...>]

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

[Smtcomp-discussion] FP demo track at SMT-COMP

[Christoph W. <cw...@mi...>]

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