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

[Rémi Delmas]

Hi everyone!

I'm glad to have some feedback on this proposal.

I've done bibliographic research on the topic and found these papers to 
be quite interesting. The authors propose an arc coherent and polynomial 
size encoding of pseudo boolean constraints (cardinality is just a 
special case of this).

http://boolvar.net/static/pagespro/pdf/obybor-sat-2009.pdf

http://boolvar.net/static/pagespro/pdf/jsat-2006.pdf

I've done some experiments on my own, trying different encodings of 
cardinality constraints, and my observations match the authors claims, 
i.e. the proposed encoding is the one that lends itself best to unit 
propagation with MathSat, Z3, yices, etc.

Unfortunately, I will not be able to provide the community with 
benchmarks right now, as I manually bitblasted my examples to 
propositional logic, but I can work on it for later.

/Rémi

Duraid Madina wrote:
> 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