Clean up support for CVC5 #729
Conversation
| Cvc4 -> "bv2nat" | ||
| Cvc5 -> "bv2nat" |
There was a problem hiding this comment.
Is this correct? Sounds like bv2nat has different semantics than bv2int
There was a problem hiding this comment.
apparently they do the same thing... (per Nikolaj B.)
There was a problem hiding this comment.
cvc people say is not standard smtlib cvc5/cvc5#11252, but I see it here https://smt-lib.org/theories-FixedSizeBitVectors.shtml
There was a problem hiding this comment.
Yes, its odd. Furthermore -- CVC seems to just not support bv2int -- I get Symbol 'bv2int' not declared as a variable errors...? I guess you better only implicitly convert nats into bv...
There was a problem hiding this comment.
Btw, Z3Prover/z3#6419 seems to indicate that even in z3 bv2int and bv2nat do the same thing?
There was a problem hiding this comment.
Oh I get it now, bv2int and bv2nat are not part of the standard they are only defined to define the semantics. From the CVC5 issue it seems that is going to be standardized in smtlib 2.7 so maybe worth tracking in an issue.
Also is bv2int/bv2nat in z3 the same as bv2nat in CVC?
There was a problem hiding this comment.
Ok I get it now (for real)
- In Z3,
bv2intandbv2natare aliases. They both implement the semantics of the upcomingbv2nat, i.e., they interpret the bit vector as an unsigned integer - In CVC, only
bv2natis implemented and it has the semantics of the upcomingbv2nat
In smtlib 2.7, bv2int will have a precise meaning (bit vectors as signed integer) different from the one implemented by z3, so the correct thing here is to use bv2nat both for z3 and cvc because it will be forward compatible.
Fixpoint (and users of fixpoint) should probably start using *_to_nat instead of *_to_int to reserve to_int for the upcoming meaning in 2.7.
| , interpSym intbv32Name "(_ int2bv 32)" (FFunc intSort bv32) | ||
| , interpSym intbv64Name "(_ int2bv 64)" (FFunc intSort bv64) |
There was a problem hiding this comment.
probably a similar argument applies here and we should use nat2bv, but I haven't checked.
cvc5to the CI ... (!!!)Fixes #728