[SMT-LIB] overflow checking for bit-vectors

[Florian Schanda]

On Friday 04 Sep 2015 09:20:51 Florian Schanda wrote:
> I propose to extend QF_BV as follows:
> 
>   Functions:
> 
>     (bvsaddo (_ BitVec m) (_ BitVec m) Bool)
>     (bvuaddo (_ BitVec m) (_ BitVec m) Bool)
>     (bvssubo (_ BitVec m) (_ BitVec m) Bool)
>     (bvusubo (_ BitVec m) (_ BitVec m) Bool)
>     (bvsmulo (_ BitVec m) (_ BitVec m) Bool)
>     (bvumulo (_ BitVec m) (_ BitVec m) Bool)
>     (bvsdivo (_ BitVec m) (_ BitVec m) Bool)
>       - signed and unsigned addition, subtraction, multiplication, and
>         unsigned division overflow checking
> 
>     (bvsnego (_ BitVec m) Bool)
>       - signed negation overflow checking

Armin tells me that Boolector already implements these [1] with the exception 
of bvsnego, with coincidentally the same names. This makes me happy that the 
names are understandable (if two people come up with the same ones 
independently then its a good sign in my book).

I also note that my text comment above should say "signed division", not 
"unsigned".

	Florian

[1] Robert Brummayer, Armin Biere, Florian Lonsing. BTOR: Bit-Precise 
Modelling of Word-Level Problems for Model Checking. In Proc. 1st Intl. 
Workshop on Bit-Precise Reasoning (BPR'08), Princeton, New Jersey, USA, July 
2008.