Understanding Question

[ioah86]

Hello,

I am trying to work through your code, and I have a small understanding issue:
In SolverTypes.h, you define the class lbool. For the && operator of it, you are writing some optimized code; I guess to make it faster. My understanding is that lbool is one of three values: True (represented by 0), False (represented by 1), and Undefined (represented by 2). I would expect the result of the && operation, at least in theory, to be one of these three values. But when I run the lines

cout << toInt(l_True && l_True) << endl;
cout << toInt(l_True && l_False) << endl;
cout << toInt(l_True && l_Undef) << endl;
cout << toInt(l_False && l_True) << endl;
cout << toInt(l_False && l_False) << endl;
cout << toInt(l_False && l_Undef) << endl;
cout << toInt(l_Undef && l_True) << endl;
cout << toInt(l_Undef && l_False) << endl;
cout << toInt(l_Undef && l_Undef) << endl;

I get as output

0
1
3
1
1
1
3
1
3

Is that intended? Is anything that is not 0 or 1 automatically undef? This is just for my understanding. Thanks in advance for the answer.

[chanseokoh]

My understanding is that, if the second-rightmost bit is set (which includes 2 and 3), the value is considered undefined. If you look at the == operator,

    bool  operator == (lbool b) const {
        return ( (b.value & 2) & (value & 2) )  // (1)
                |
               ( !(b.value & 2) & (value == b.value) );  // (2)
    }

(1): Are they both undefined? Then yes, they are equal.
(2): Is b defined (i.e., either true or false)? Then check if the rightmost bits are same (i.e., check if both bits say they are 0 (true) or 1 (false)).

Then all the && outputs make sense.

[ioah86]

Ah, so it is more about the bit setting than the actual value? Interesting... As mentioned in the email correspondence, I think that should be commented somewhere (or unit tested ;-)).
Thank you very much for the response.
Kind regards,

Albert