Hi Group, This is helpful, thank you. I'll take a look at Kellen Dye's work and L. D. Michel and P. Van Hentenryck paper.
Thanks, Serg On Wed, Mar 11, 2015 at 8:13 AM Jean-Noël Monette < jean-noel.mone...@it.uu.se> wrote: > 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 > > Expert Researcher, SICS, cschu...@sics.se > > > > *From:* users-boun...@gecode.org [mailto:users-boun...@gecode.org > <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 > listusers@gecode.orghttps://www.gecode.org/mailman/listinfo/gecode-users > > > _______________________________________________ > 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
