[SMT-LIB] Signed comparisons in bit vector theory

[Clark Barrett]

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
>