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

[Domagoj Babic]

Hi Clark,

On 5/2/07, Clark Barrett <barrett at cs.nyu.edu> wrote:
> 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...

I will submit a thm prover (Spear) that handles only modular arithmetic
(the translator can also chew some UIFs, but you can't push it too far).

About benchmarks: I've started the generation process. It is not a
problem to generate an extremely large number of benchmarks, the problem
is to generate hard ones --- Spear solves 99% of them in a couple of seconds.
Anyways, I will certainly be able to provide you with enough hard benchmarks
to open QF_BV64 category.

> > - replace mod by rem
>
> :)

Heh, look, it's like saying: our logic supports operator PLUS, but since
it initially seemed to us to be MINUS, we are calling it MINUS.
Later, when we figured out the difference, we still decided to keep
calling it MINUS, no matter what. :-)

Personally, I really don't mind how you call it - just wanted to let
you know that it is really wrong. Anyways, I will stop bringing up this
issue.

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

Yes, I understand - I'd just add 'redundant syntactic sugar' :-)

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

Yes, that's the set. I just wanted to let you know about this, but I see
you are already well informed :-)

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

Please do consider using a larger set - excitement of incoming results
is great, but a large set of diverse benchmarks will do even more for the
field.

Regards,
    Domagoj Babic