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

[Clark Barrett]

> > > 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.
> 
> How many do you consider enough?

It's not a hard and fast rule.  However, in principle I agree that it makes
sense to separate out the benchmarks with/without uninterpreted functions.  The
other question is whether there are any solvers that only support bitvectors
(not UF's).  That would be another reason to separate the two.  I am currently
in the process of collecting and posting several sets of bitvector benchmarks,
so I'll keep this in mind as we go...

> Since you are introducing them into the format now, may I suggest
> several mods:
> 
> - replace mod by rem

:)

> - shift_leftX, shift_rightX became redundant by introduction of
>   bv(a|l)shr/bvshl
> - rotate_left and rotate_right are easy to synthetize and therefore
>   redundant

Yes, but these are just syntactic sugar anyway (not part of the underlying
theory), so I'm inclined to keep them around for backwards compatibility.

> - the grammar in SMT 1.2 document does not seem to allow production
>   formula ::= '(' formula ')'
>   without which I couldn't parse some instances available out there

If you are referring to the UCLID benchmarks from TACAS '07, I noticed the same
thing.  However, I easily fixed the benchmarks to comply to the SMT-LIB
standard (I'll be posting them soon--they don't include UF--interesting).  On
the other hand I don't feel too strongly about it if others want to change the
standard.

> Hmm... Even within one category, 100 benchmarks seems too few to me,
> especially when I see the 2006 results on QF_UFBV32 category: total
> runtime of the first two solvers: 0 sec.

That was more a function of not having challenging enough benchmarks, not of
picking too few.  Our competition is modeled after the CASC competition that
runs concurrently with CADE.  We like the real-time feel and the excitement of
results coming in throughout the conference.  Still, you make a good point--we
could have used more benchmarks last year and still finished on time.  We'll
see how it goes this year...maybe we'll be able to use more than 100 per
division...

-Clark