[SMT-LIB] extensions to bitvector theory

[Domagoj Babic]

Hi,

I'd say it's great. My only suggestions at this point:

- To gradually introduce arbitrary bit-lengths. Extending the current format
  to support 1,8,16,32,64 bit types would suffice for now, and make the
  transition smoother.
- To limit the largest type size to 64 bits, so that DIV/MOD/MUL by a constant
  with magic numbers can be done in 128 bits with multiply high. 64 bit
  operations are not such a problem, but larger operations are. If you
  really pushed for arbitrary bitvector sizes, every solver would *have to* use
  some bignum library, which is a serious hassle from my perspective. If this
  is a too restrictive,  I'd suggest at least limiting the size of DIV/MOD/MUL
  operands to 64 bits.
- One way or another, with new [S|U][DIV|MOD] operators, everyone will
  have to make at least some modifications on their parsers & provers, so
  this might be a good opportunity to systematize and unify comparisons
  [SETUGE,SETSGE,SETULT,...]. The same applies to bvdiv and bvsdiv -
  if we change bvdiv to bvudiv, it's immediately clear to everyone what the
  operator is, even without reading the theory files. On the other hand, if
  you go with bvdiv and bvsdiv, and some benchmarks contain only bvdiv,
  you leave plenty of space for confusion.

However, I'm not really able to give you a detailed feedback until I get
my hands dirty... Now I'm busy with some other stuff, will start working
on generation of SW verification benchmarks in SMT modular arithmetic format
in early Feb. At that point, I'm sure I will have more questions and
suggestions.

A related question:

> > [Domagoj Babic wrote:]
> > BTW, what does "packet" mean in egt benchmarks?
>
> [Clark Barrett wrote:]
> I'm not sure.  These benchmarks came from verification work at Stanford,
> submitted by Vijay Ganesh.  "packet" is probably a variable name for an array
> used to model transactions or something similar.

Heh, Vijay said he had no clue, and that I should ask you Clark :-)

If it is an uninterpreted function, that means that all modular
arithmetic theorem provers have to handle UIFs as well.

Quote from egt_0083.smt benchmark:
packet def: :extrafuns ((packet BitVec[32] BitVec[8]))
usage: (packet (extract[31:0] bv241))

IMHO, the theory of modular arithmetic should be separate from UIFs.
Modular arithmetic is already hard enough. Any converter requiring
UIFs can do conversion before dumping benchmarks to SMT MA format.

Regards
       Domagoj Babic