OCamlPro
experiment with replacing bitvectors by integers theory
cc @filipeom and @hra687261 as we are actually working on something similar, have you ever played with the integers theories ? (are they simply implemented as bitvectors of a specialized size ?)
(cc @felixL-K)
The theory of integers is supposed to handle mathematical/arbitrary sized integers, so bit-wise reasoning is usually not included in theories of integers (https://smt-lib.org/theories-Ints.shtml). Afaik smt solvers use something like Zarith/GMP to reason over them, it's probably safe to assume that if you're doing pure arithmetic reasoning and not using bit-wise operations, the theory of integers would be better than bit-vectors notably if you're doing linear arithmetic (although I wouldn't expect bit-vector reasoning to be any better in non-linear arithmetic, but that's just intuition). I think it's definitely worth exploring, bench-marking is the best-way to know because it probably also depends on the tests you have and the kinds of operations they use.
I think it's definitely worth exploring, bench-marking is the best-way to know because it probably also depends on the tests you have and the kinds of operations they use.
Yes, I'd say so too. We will definitely lose some precision (we'll no longer detect integer overflows), but we might gain in other areas.
On smtml's side, I think it's pretty easy to implement. We would keep the bit-level reasoning for concrete values, since the Bitvector module handles that for us. But we would create a different Z3_mappings module that encodes Val (Bitv) and all bitvector-related operators using the theory of integers instead of bitvectors.
