Ok I lied, there isn't just one bitfield domain, there are two. And I'm interested in both in them.

One them (henceforth BD1), as described here (chapter 2.8) works like this:
An abstract value in BD1 is a pair (z, o) describing the set { x for which (x | z) == -1 and (x | o) == o } (I know the o is easy to confuse with zero, but it's really an o and I didn't choose this notation)
So, in English, z is a bitmask where a zero at position k means that no elements in the set are allowed to have bit k set to zero, a one in z at position k means that elements in the set may have bit k set to zero (but they don't necessarily). o on the other hand is a mask that describes which bits are allowed to be one.
For example,
z = 1110
o = 0001
set: { 0001 }

z = 1111
o = 0011
set: { 0000, 0001, 0010, 0011 }

z = 1111
o = 1110
set: even numbersSome abstract operators are:
(z1, o1) | (z2, o2) = (z1 & z2, o1 | o2)
(z1, o1) & (z2, o2) = (z1 | z2, o1 & o2)
(z1, o1) ^ (z2, o2) = ((z1 & z2) | (o1 & o2), (z1 & o2) | (o1 & z2))
And obviously you can build addition out of those, but that's not very efficient. So, question 1, does anyone have a better idea for how to implement addition in BD1? Something nice and elegant like the ones above?

The other obvious implementation of a bitfield domain, BD2, is with a bitmask m that says which bits are known and a value v in which only the bits that are set in m are relevant and the rest are zero for convenience. Unlike BD1, BD2 has no representation for the empty set (BD1 has multiple such representations, namely all those where at some position k, both z and o have a zero).
Anyway, a value in BD2 is thus a tuple (m, v) and as example
m = 1111
v = 0101
set: { 0101 }

m = 1001
v = 0000
set: { 0000, 0010, 0100, 0110 }

m = 0001
v = 0000
set: even numbers
Some abstract operations are:
(m1, v1) | (m2, v2) = ((m1 & m2) | v1 | v2, v1 | v2)   // both known or one of them is 1
(m1, v1) & (m2, v2) = ((m1 & m2) | (m1 ^ v1) | (m2 ^ v2), v1 & v2) // both known or one of them is 0
(m1, v1) ^ (m2, v2) = (m1 & m2, (v1 ^ v2) & m1 & m2)
Most things get more complicated in this formulation, except XOR.
In BD2, building addition from these primitives is even worse than it was in BD1.
You can rewrite it a little and get this, which is about 14 times faster in practice:
uint abm = m1 & b2;
uint knownzero = m1 ^ v1 | m2 ^ v2;
uint knownone = v1 | v2;
uint cm = 1 | ((abm & ~(v1 ^ v2)) << 1);
uint cv = (v1 & v2) << 1;
uint m = 0;

for (int i = 0; i < 32; i++)
{
    uint e = cm & abm;
    m |= e;
    uint t = (cm & cv & knownone) << 1;
    cm |= ((e | cm & ~cv & knownzero) << 1) | t;
    cv |= t;
}
v = v1 + v2;But I suspect that there's some trick I'm missing. Something elegant I'm overlooking. Something like this:
(m1, v1) + (m2, v2) = (~(v1 + v2) ^ ((v1 | ~m1) + (v2 | ~m2)), v1 + v2)But that doesn't work. This is basically saying "a bit of the result is known if it is the same in (minimum element in set 1 + minimum element in set 2) and in (maximum element in set 1 + maximum element in set 2)", which is not true in general, because for example (now using the general notation where an * means "unknown") 000* + 000* = 00** whereas the above code would conclude that the least significant bit is known to be zero.
So question 2, is there a better way to implement addition in BD2?

Any useful (or interesting, or better yet: both) ideas are appreciated.

Well, I solved it. I'm sure a couple of operations can be shaved off, but this is a proper solution:
uint an = ~av & am;
uint bn = ~bv & bm;
uint g0 = an & bn;
uint g1 = av & bv;
uint p0 = an ^ bn;
uint pg1 = av | bv;
uint g0l = ~g0 & ((g0 << 1) | 1);
uint g1f = g1 & ~(g1 << 1);
uint nc = (p0 + g0l & ~p0) - g0l | g0;
uint m1 = ~pg1 | (pg1 & g1f);
uint c = (pg1 + g1f & m1) - g1f;
uint cm = (c | nc) << 1 | 1;
uint m = cm & am & bm;
uint v = av + bv;The inputs are (am, av) and (bm, bv), the output is (m, v)

The basic idea is that you can use a "known carry" to select a whole "will propagate carry"-block. That's what the (a + b & ~a) - b stuff is about - that's the main breakthrough that led to this algorithm. There are some details that are different on the "carry is known to be 1" and the "carry is known to be 0" sides, but in general it does the same thing for both and then combines the answer. Can't you do it in one go, you may wonder? I'm not sure, but I don't think so. I originally thought so, but a couple of details are different and they mess things up. Anyway, this isn't too bad.

The shitty variable names like g0 are "generates a 0 carry", pg1 = "propagates or generates a 1 carry", p0 = "propagates a 0 carry", g1f = "first of g1" (ie the rightmost bit of every run of 1s), g0l = "last of g0" (one past the last 1 of a run of 1s)