[SMT-LIB] BitVectors32

[Clark Barrett]

> However, two other small things occurred to me while implementing the BV 
> typechecker. I solved these, but they still seem kind of 'unclean' to 
> me, that's why I mention them:
> 
> - predicates are not defined for different bitvector sizes, e.g., = is 
> frequently used in the benchmarks with arguments of BitVec[8] and 
> Bitvec[32]. Also, the theories predicates (bvlt, bvleq...) are only 
> defined to be (pred BitVec[m] BitVec[m]), i.e., take arguments of equal 
> size m. And there is no bveq (not needed, but would be nice).

Equality ("=") should only be applied to arguments of the same size.  Can you
give me an example of where equality is applied to arguments of different sizes
in the benchmarks?

Theory predicates are supposed take arguments of equal size.  Are you
suggesting something different?

What would be the difference between bveq and "="?

> - Variables of sort BitVec[1] are implicitly assumed to be boolean. 
> While this is not a real problem, a typechecker still has to double 
> check the function definitions in that case.

I'm not sure what you mean by this.  The semantics of SMT-LIB do *NOT* allow a
term of sort BitVec[1] to be used where a formula is expected.  So in what way
are variables of sort BitVec[1] implicitly assumed to be Boolean?

-Clark