[SMT-LIB] Suggested small changes to the QF_BV logic.

[Trevor Alexander HANSEN]

Hello,

There seem to me to be some small problems with the QF_BV specification:

http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt2


> The following symbols are parameterized by the numeral i, where i >= 0.
>    ((_ repeat i) (_ BitVec m) (_ BitVec i*m))
>      - ((_ repeat i) x) means concatenate i copies of x

It's nicer to explictly exclude (_ repeat 0)

> For all numerals j > 1 and 0 < m, and all terms of s and t of
>   sort (_ BitVec m),
> ((_ zero_extend 0) t) stands for t
>    ((_ zero_extend j) t) abbreviates (concat ((_ repeat j) #b0) t)

Which doesn't define ((_zero_extend 1) t)

> For all numerals j > 1 and 0 < m, and all terms of s and t of
>    sort (_ BitVec m),
> ((_ rotate_left 0) t) stands for t
>    ((_ rotate_left j) t) abbreviates t if m = 1, and
>      ((_ rotate_left |j-1|)
>        (concat ((_ extract |m-2| 0) t) ((_ extract |m-1| |m-1|) t))
>      otherwise

Which allows j > m only for m=1. Limiting to j <= m for rotate_left and 
rotate_right seems the right thing to do.

Below is the patch I suggest.

Thanks,
Trevor



92c92
<     The following symbols are parameterized by the numeral i, where i > 0.
---
>     The following symbols are parameterized by the numeral i, where i >= 0.
96,98d95
<
<     The following symbols are parameterized by the numeral i, where i >= 0.
<
108c105
<       - ((_ rotate_right i) x) means rotate bits of x to the right i times
---
>       - ((_ rotate_right i) x) means rotate bits of x to the right y times
217,219d213
<     For all numerals j > 0 and 0 < m, and all terms of s and t of
<     sort (_ BitVec m),
<
227,229d220
<     For all numerals m >= j > 0 and 0 < m, and all terms of s and t of
<     sort (_ BitVec m),
<