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

[Domagoj Babic]

Hi,

On 4/30/07, Cesare Tinelli <tinelli at cs.uiowa.edu> wrote:
> > I assumed
> > that this is just a cosmetic modification, but Clarke B. pointed
> > out that
> > this modification would require changes in the underlying logic.
> >
> What modification? Eliminating the difference between terms and formula?
> That modification would indeed require a major change of both the
> underlying logic's syntax and semantics.

Ok, I see. However, this is really inelegant for modular arithmetic.

> > 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(++)).

For details, please search google groups for "mod rem difference".
(http://groups.google.com/)

> > If all three suggestions are accepted, I can make the benchmarks
> > available
> > today...
> >
> Is your offer still valid? :)

Since there was little interest, I haven't been updating the code, and at
one point it became so outdated that I ditched it. Now when you mention
another modification of the SMT format, I wonder whether it makes sense
to write the generator at this point. So, here's what I propose:

I can generate benchmarks in the SF (see my webpage) format, which is so
trivial, that it can be translated into SMT in one afternoon.


For the benchmarks to make sense you would really need to replace mod
with rem.

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



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


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

I'd say it's too late to change the format at this point, perhaps for
the next year.


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.

Regards,
    Domagoj Babic