search

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
60 stars 17 forks source link

Add support for bv2int and for int2bv #146

Closed Heizmann closed 10 months ago

Heizmann commented 1 year ago
jhoenicke commented 1 year ago

I strongly prefer a totally defined function over a partially defined function.

Isn't any int2bv function only partially defined? Or should it always return the lowest n-bits? I can see that the latter is preferable as we don't have to reason about uninterpreted functions for the undefined case.

Is bv2int allowed to return a negative number or does it behave like bv2nat in the standard? If it's the first, you still want to have a bv2nat function.

jhoenicke commented 11 months ago

See also https://github.com/SMT-LIB/SMT-LIB-2/issues/2

The bitvector theory will define a new auxiliary function bv2int in addition to bv2nat which converts to signed integer. I'm not sure if we want to follow this. It's also not a publicly visible function.

Heizmann commented 10 months ago

See also SMT-LIB/SMT-LIB-2#2

The bitvector theory will define a new auxiliary function bv2int in addition to bv2nat which converts to signed integer. I'm not sure if we want to follow this. It's also not a publicly visible function.

So if Pascal proposes this semantics of for bv2int and no one objects, I would prefer that we use bv2nat and nat2bv with the semantics of the (not publicly visible) functions from the bitvector theory.

I already did the renaming: https://github.com/ultimate-pa/smtinterpol/commit/2d43d36344fddb2df8fd4c4dcb26d289415a2066

I think bv2nat and nat2bv are currently sufficient for us, we do not also need bv2int. However, for me it would be ok to also add bv2int or even also int2bv.

Heizmann commented 10 months ago

@jhoenicke I commited all modifications that I wanted to implement. So from my side this pull request is ready to be merged.