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

[Cesare Tinelli]

Hi all,

On May 2, 2007, at 5:20 PM, Domagoj Babic wrote:

[...]

>> > - 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. :-)
>
I sympathize with Domagoj's point. Can anybody else who is familiar  
with bitvectors support his claim that mod is the wrong name? As  
Clark says, the logic literature uses mod so it'd be good to  
understand what the community prefers/recommends.


> 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' :-)
>
Note that saying 'redundant syntactic sugar' is redundant :)
Syntactic sugar is redundant by definition.



>> > - 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.
>
That's true. But notice that just increasing the number is no  
guarantee that the sample is representative. I do trust the SMT-COMP  
organizers though that they will make an effort.

To address this problem though we have been working on a different  
solution that we hope will be even more beneficial to the community:  
a new site, modeled after SatEx, that shows year-round runtime data  
on publicly available solvers for the whole SMT-LIB repository.
Aaron Stump is leading this project, so I'll let him add more details  
if he wants.


Cesare





> Regards,
>    Domagoj Babic