[SMT-COMP] Bitvector language in SMTLIB

[Clark Barrett]

Vijay,

I like your suggestions.  I do know that there are some plans to implement some
of this.  I hope we can get some feedback from others as well.

However, this topic should be on the SMT-LIB mailing list, not the SMT-COMP
mailing list.  The former is for discussions about the format and library.  The
latter is for discussions specific to the competition.

I suggest you repost your message to smt-lib at cs.nyu.edu and that we close the
thread on this list.

-Clark

> 
> Dear Friends,
> 
> I would like to make some suggestions with regard to the SMTLIB bitvector 
> language.
> 
> * It would be nice to allow constants expressed in binary and hexadecimal 
> format. Currently, the language supports only decimal format for 
> constants. Hence, we are forced to put an extraction operator on top of 
> the decimally-represented constant in order to know its length. 
> Binary/Hexadecimal formats will obviate the need for extractions over 
> constants.
> 
> * Limiting the language to BV(32) is, well, too limiting. It would be 
> great if we could allow fixed-length variables/constants of any length. 
> There are many applications which require vectors of 64 bits or more. 
> Furthermore, it allows us to effectively parameterize the input, and thus 
> stress test our systems and know their limits.
> 
> * Support for DIV/MOD (signed and unsigned)
> 
> Thanks for your time,
> Vijay Ganesh
>