[SMT-LIB] Suggestion for addition in the BitVec theory

[Rémi Delmas]

Hello,

it would be very handy if the BitVec theory offered bitcount predicates 
that would allow to express cardinality constraints on the number of 
true bits in a bitvector.

(bvbitcounteq Int BitVec[m] Bool) :

true iff the number of true bits in the second argument is equal to the 
first argument


(bvbitcountlt Int BitVec[m] Bool) :

true iff the number of true bits in the second argument is strictly less 
than the first argument


we could have polymorphic variants of them for ease of use :

(bvbitcounteq BitVec[n] BitVec[m] BitVec[1]) :

true iff the number of true bits in the second argument is equal to the 
first argument (seen as an integer in 2's complement).

(bvbitcountlt BitVec[n] BitVec[m] BitVec[1]) :

true iff the number of true bits in the second argument is strictly less 
than the first argument (seen as an integer in 2's complement).

More proposed variants :
(bvbitcounteq[i] BitVec[m] BitVec[1])
(bvbitcountlt[i] BitVec[m] BitVec[1])
(bvbitcounteq[i] BitVec[m] Bool)
(bvbitcountlt[i] BitVec[m] Bool)



Best regards,

Rémi Delmas