[SMT-LIB] Signed comparisons in bit vector theory

[Régis Blanc]

Thanks to both of you. Indeed everything I needed was in the QF_BV logic.

I was thinking that logic would only restrict the terms that can be
written, and not add new operators. Thus I didn't think to check there.


On Tue, Sep 2, 2014 at 7:31 PM, Clark Barrett <barrett at cs.nyu.edu> wrote:

> Regis,
>
> The bit-vector *theory* does not include all of the operators available in
> the bit-vector *logic*.  Take a look at the logic definition for QF_BV on
> the smtlib.org website.  At the top, you will see a summary of all of the
> available operators, including both signed and unsigned comparisons.
>
> -Clark
>
>
> On Tue, Sep 2, 2014 at 9:28 AM, Regis Blanc <regwblanc at gmail.com> wrote:
>
>> Hello all,
>>
>> I am trying to use the theory of bit vectors to encode some
>> properties of java Integers. However, as far as I can tell, the only
>> comparison operator available in the standard is bvult, which
>> does an unsigned comparison. I was wondering if there was a standard
>> way to do signed comparison (negative numbers in two-complement) or
>> if I had to do my own encoding based on the unsigned comparison and
>> extracting leading bits?
>>
>> Thanks,
>> Regis
>> _______________________________________________
>> SMT-LIB mailing list
>> SMT-LIB at cs.nyu.edu
>> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>>
>
>