[SMT-LIB] BVDIV on Bitvector (SMTLIB2) ?

[Jun Koi]

On Wed, Aug 24, 2011 at 10:29 AM, Jun Koi <junkoi2004 at gmail.com> wrote:
> hi,
>
> in SMTLIB2, while we have most basic bitvector arithmetics, it seems
> there is no support for bvdiv?
> this is confirmed on Z3, which is fully compatible with SMTLIB2 from version 3.0
>
> so do i need to implement bvdiv myself? if so, any body did that
> before? any code to share, please?
>

ok, i found the bvudiv

> also, where i can find information on QF_BV of SMTLIB2? for example,
> to understand the syntax of bvxor, bvnot, ...etc\

another question: i found bvule, bvugt, etc. but i cannot find
anything to compare 2 vectors, so i can know if 2 vectors are equal.
or did i miss something?


many thanks,
Jun