[SMT-LIB] Bool as alias for BitVec[1]

[Clark Barrett]

> > > 3) I just noticed that the new operators that were recently
> > > proposed suggest
> > > bv(s)mod instead of bv(s)rem. That should be fixed.
> > >
> > In what way? What is the problem with bvmod?
> 
> mod and rem are two different operators, rem is usually used (what you
> get with % in C(++)).

OK, it seems that we agree on the meaning, just not the name.  I want to point
out that what you are calling rem is also called mod in much of the
literature.  See, for example, http://en.wikipedia.org/wiki/Modulo_operation.
The important thing, though is that our bv(s)mod operator has the semantics of
% in C.

> I'd also suggest that you open a modular-arithmetic-specific category,
> without UIFs. QF_BV64 ?

If we have enough benchmarks for such a category, we will consider it.

> Since you sent the SMT competition notification the very last moment,
> there are two possible options:
> 
> 1) Somebody from the organizers writes a quick SF2SMT translator. You
> can even write the parser manually, without using flex/bison, because
> the format is so trivially simple (and well-defined).
> 
> 2) You give me a couple of more days (by the beginning of the next week)
> to write SF2SMT translator (SMT2SF is available). I need this much time
> because I'm working on several other things right now (with a deadline
> coming soon).

I'm afraid the announcement may have been misleading.  We are accepting
benchmarks from now until June 1.  I hope you will consider the second option
and that we will be able to work together until we can agree on the format.

> > We plan to propose the new version of the theory
> > Fixed_Size_BitVectors and the logic QF_UFBV in the next few days.
> > With that, inserting ITEs in your benchmarks should not take a lot of
> > effort.
> 
> That's nice, but does it make sense to propose a new format at this
> particular point? You sent the competition announcement 5 days before
> the deadline for the benchmark submission, and now you are going to
> change the format after the deadline?

The format is not brand new--it's just the addition of the operators I proposed
some time ago on the SMT-LIB list.  I've been meaning to formalize their
addition by updating the SMT-LIB pages, but just haven't had the chance yet.
However, now that my semester is over, I should be able to do this by the end
of the week.

> Another organizational point that's unclear to me: In the SMT-COMP announcement
> you left only 5 days for the competition. So, either you expect a small number
> of trivial benchmarks, or you have a really large cluster? Let me remind you that
> SAT competition is running for 5 months, out of which is (I think) roughly 3 months
> for computation, on a decent cluster. I'm afraid that if I send the benchmarks, you
> will end up using 10-50 easier ones.

We don't have nearly as many solvers as the SAT competition.  Also, we pick
only 100 benchmarks per division (distributed from easy to hard).  The
benchmark selection process and competition format is spelled out in detail in
the "Rules" section of the webpage.  The rules have been carefully crafted and
have worked well the last two years.

-Clark