search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
332 stars 62 forks source link

Question on overflow operations #68

Closed aman-goel closed 4 years ago

aman-goel commented 4 years ago

Hi,

I see that the C API includes a bunch of operations relating to the overflow in arithmetic operations, like uaddo, saddo, usubo, ssubo, umulo, smulo, sdivo. Since these appear to me outside the SMT-LIB v2 format, are there any formal definition of each such function (especially the signed ones) into an equivalent SMT2 expression?

Thanks Regards Aman https://aman-goel.github.io

mpreiner commented 4 years ago

Hi Aman,

I can't point you to a document that includes all overflow operators in terms of SMT-LIB operators, but you can check out how they are implemented in Boolector in btorexp.c.

aman-goel commented 4 years ago

Thanks!

arminbiere commented 4 years ago

Page 77ff in Robert Brummayers thesis discusses this .... http://fmv.jku.at/papers/Brummayer-PhD-Thesis-2009.pdf