Hi Serg,
Kellen Dye implemented a Bit-Vector domain implementation for Gecode for
his master thesis. You can find his thesis at
http://uu.diva-portal.org/smash/record.jsf?pid=diva2%3A761927&dswid=8488
and the source-code at
https://github.com/kellen/bitvector-masters
He did not implement the addition constraint but the paper on which he
based his implementation gives an algorithm for the addition:
L. D. Michel and P. Van Hentenryck. *Constraint* *Satisfaction* *over*
*Bit-Vectors*. http://link.springer.com/chapter/10.1007/978-3-642-33558-7_39
Best,
Jean-Noël
On 2015-03-11 10:17, Christian Schulte wrote:
Hi Serg,
For the time being there is not much that you can do about this. And
Gecode cannot be easily recompiled using unsigned ints (or 64 bit
integers for that matter). I think some people have been experimenting
with arbitrary precision integers as well as bit vectors but I do not
know how far that got. Anybody?
Best
Christian
--
Christian Schulte, www.gecode.org/~schulte
Professor of Computer Science, KTH, cschu...@kth.se
<mailto:cschu...@kth.se>
Expert Researcher, SICS, cschu...@sics.se <mailto:cschu...@sics.se>
*From:*users-boun...@gecode.org [mailto:users-boun...@gecode.org] *On
Behalf Of *Serg Buslovsky
*Sent:* Wednesday, March 11, 2015 6:54 AM
*To:* users@gecode.org
*Subject:* [gecode-users] unsigned 32bit representation, additions
Hi Group,
I'm thinking about the ways of implementing 32bit unsigned integer
representations in gecode model.
So I have 32 BoolVar's per uint32 representation, which are used to
store corresponding bits, then I can easily define bitwise operations
on "integers" by posting relation constraints on the bits.
The problem is with the addition.
My first approach was to add an IntVar, post linear constraints with
powers of 2 as coefficients to reconstruct integer from bits, however
gecode limits IntVar into signed int bounds and it doesn't fit.
The second approach was to just implement binary addition:
bool lsb = true;
for (int i=(INT_BITS-1); i>=0; i--) {
BoolVarArgs bits;
bits << bools[i] << x->bools[i];
if (!lsb) {
bits << result->bools[INT_BITS+i+1];
}
rel(*model, BOT_XOR, bits, result->bools[i]);
if (lsb) {
rel(*model, BOT_AND, bits, result->bools[INT_BITS+i]);
lsb = false;
} else {
linear(*model, bits, IRT_GQ, 2, result->bools[INT_BITS+i]);
}
}
(bools[i] - bits of the first "integer", x->bools[i] - bits of the
second "integer", result->bools[i] - bits of the resulting "integer",
result->bools[INT_BITS+i] - carry bits)
That works but it turned out to be very inefficient in practice,
complexity of the model is growing exponentially with this approach.
Any thoughts? Maybe there's a way to recompile gecode to use unsigned
int internally? Maybe there are ideas on better implementation of
addition? Maybe just some suggestion on another tool which uses
unsigned ints internally?
Thanks,
Serg
_______________________________________________
Gecode users mailing list
users@gecode.org
https://www.gecode.org/mailman/listinfo/gecode-users
_______________________________________________
Gecode users mailing list
users@gecode.org
https://www.gecode.org/mailman/listinfo/gecode-users
