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

[Duraid Madina]

Hi Clark, Remi:

	I could certainly provide a few such benchmarks, up to now I have
been getting away with hacks like (in CVC3):

B0, B1, B2, B3 : BITVECTOR(16);
ASSERT(B0 = 0hex5555);
ASSERT(B1 = 0hex3333);
ASSERT(B2 = 0hex0f0f);
ASSERT(B3 = 0hex00ff);
popcount : BITVECTOR(16) -> BITVECTOR(16) =
  LET C1 = LAMBDA(x:  BITVECTOR(16)): BVPLUS(16, (x  >> 1)&B0[15:0],
x&B0[15:0]) IN
  LET C2 = LAMBDA(C1: BITVECTOR(16)): BVPLUS(16, (C1 >> 2)&B1[15:0],
C1&B1[15:0]) IN
  LET C3 = LAMBDA(C2: BITVECTOR(16)): BVPLUS(16, (C2 >> 4)&B2[15:0],
C2&B2[15:0]) IN
  LET C4 = LAMBDA(C3: BITVECTOR(16)): BVPLUS(16, (C3 >> 8)&B3[15:0],
C3&B3[15:0]) IN
  LAMBDA(x: BITVECTOR(16)) : C4(C3(C2(C1(x))));

	I would be thrilled if a tool did something more intelligent than
just blast away bitcount predicates doing something similar to the above, so
I agree with Remi that it might be a good idea to add such predicates. There
are a number of different ways of formulating the Hamming weight and I have
seen tools perform differently on benchmarks depending on the formulation
used. So if bitcount gets added to the SMT-LIB format, at the very least one
would hope that implementers would treat it in a way appropriate for their
particular tools.

	Duraid

	
On Thu, Mar 25, 2010 at 10:13:31PM -0400, Clark Barrett wrote:
> 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