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

[Domagoj Babic]

Hi,

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

Heh, ok, but that's (really) confusing.

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

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

Sure, I'll send you an update on this soon. June 1 is more than enough
time.

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

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

> We don't have nearly as many solvers as the SAT competition.  Also, we pick

True, but you have many more categories than the SAT competition.

> only 100 benchmarks per division (distributed from easy to hard).  The

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.

Regards,
    Domagoj Babic