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

[Clark Barrett]

Remi,

I'm not sure if anyone ever responded to you about this.

Our usual policy is that if someone can provide benchmarks using an
additional operator like the one you mention, then we will strongly consider
adding it to the standard.

Would you be able to produce such benchmarks?

-Clark


On Mon, Feb 15, 2010 at 11:10 AM, Rémi Delmas <Remi.Delmas at onera.fr> wrote:

> 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
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>