yices2 icon indicating copy to clipboard operation
yices2 copied to clipboard

Published 20 hours ago • verified publisher icon SRI-CSL

bv2nat support

Open weaversa opened this issue 3 years ago • 1 comments

bv2nat is part of the official SMTLib logic for bitvectors: http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml Though, it looks like Yices doesn't support it. Do you plan to support it? If not, do you have an alternate translation that folks can use?

Thank you!

weaversa avatar Apr 10 '21 00:04 weaversa

Hi @weaversa, bv2nat is not part of the official SMTLIB QF_BV logic. It cannot be part of this logic since it requires natural numbers in addition to bit-vectors.

The bv2nat and nat2bv in http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml are used as a notation to help define the semantics of bit-vector operators. They are not part of the QF_BV logic symbols.

Some solvers may have bv2nat or bv2int but these are non-standard extensions that involve QF_BV + integer arithmetic.

This said, we may support them in the future in Yices maybe.

BrunoDutertre avatar Apr 15 '21 01:04 BrunoDutertre