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

[Clark Barrett]

Trevor,

Sorry for the delay in responding to this email.  See my responses below.

-Clark


On Tue, May 11, 2010 at 10:00 AM, Trevor Alexander HANSEN <
thansen at csse.unimelb.edu.au> wrote:

> 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)
>

In fact, if you scroll down to the formal definition of repeat, it does
exclude (_ repeat 0), so this is a mistake.  It has been fixed.


> > 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)
>

Correct again.  Same problem in zero_extend and the rotate operators.  This
has been fixed by using another numeral i which can range from 1.


> > 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.
>

There is no such restriction.  If j > m and m > 1, then the definition
requires unfolding the recursion j times until you end up with j = 0.
 Essentially, this means that for j > m it's equivalent to using j mod m
(i.e. the remainder when dividing j by m).