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

[Nikolaj Bjorner]

Hi Remi,

I have some comments. I think it is a great suggestion to deal with bit-counts in a built-in way. 
The main pain as I see it is that tool builders need to add specialized support for new operators in order to do benchmarks. 
So perhaps there are some basic ways around.

- One can already define bit-count indirectly as a macro that produces another bit-vector of log_2(n) bits.
  There are several ways to do so, for example using masking. The benchmarks therefore strictly don't need the additional operator.
  See for instance http://gurmeetsingh.wordpress.com/2008/08/05/fast-bit-counting-routines/

- What about introducing a function "bvbitcount" with arity [m] -> [log_2(m)+1] ?
  Then you can use existing bit-vector predicates and operations to obtain the predicates you list below.
  (The extra predicates you introduce can be expressed using these function. Tools that produce bit-count predicates 
   can use a procedure for producing the appropriate predicate as a composition of existing bit-vector operations and predicates.
  Tools that consume this output can pattern match for special purpose handling, or fall back to a macro definition for bit-counting).

- You use Int for the value of bit-counting. It may be easier for several tools to be monolithic about whether they use bit-vectors or integers. 
   One can introduce bv2int and bv2int functions as an orthogonal feature.

Thanks,

Nikolaj

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Clark Barrett
Sent: Thursday, March 25, 2010 7:14 PM
To: Rémi Delmas
Cc: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] Suggestion for addition in the BitVec theory

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