Is there a C/C++ library that allows you to find out whether a set of expressions are mutually exclusive?

Question

I'm writing a compiler for a dataflow programming language I have designed. One of the features that I really like about it is that you can express the following:

x <- a + 1 if b > 3;

x <- a - 1 if b <= 3;

Which implies something like:

x <- a - 1 + 2*(b>3);

In order to pull this off though the compiler needs to know that:

((b > 3) && (b <= 3)) = false

((b > 3) || (b <= 3)) = true

Are there any C/C++ libraries that anyone knows of that would be able to validate these 2 statements (as well as much more complicated ones)? Or are there any papers available via the web that anyone knows of that detail a similar system? Or could someone describe a possible approach?

Thanks,

Daniel

Answer 1

I think you need a small set of simple rules that tell you whether two expressions are equal, or are totally different.

Let's start with the easiest ones: b>3 and b<=3

Checking whether they're equal is easy: b>3 and b>3 are equal, b>3 and b<=3 clearly aren't.

To see whether they are completely different, we would have to compare b>3 and NOT (b<=3). By simply adding the NOT in front of it, we changed the "distinct" to an "equal" comparison.

Your software should now have the logic to transform NOT (b<=3) to (b>3). And since these are completely equal, the original ones are completely distinct.

If the comparisons are more difficult, you should start to use Morgans Law. This law states that the following expressions are equal:

NOT (A AND B) is equal to NOT A OR NOT B
NOT (A OR B) is equal to NOT A AND NOT B

Now combine both rules:

• Put NOT in front of one of the expressions
• Distribute NOT to the most elemental parts of the expression using Morgans law.
• Then compare all the elements

e.g. suppose we want to know if the following expressions are completely distinct:

(a<3) and not (b>=7)
(b>=7) or (a>=3)

First put a big NOT before the second one:

NOT ((b>=7) or (a>=3))

Then distribute the NOT:

(NOT (b>=7)) and (NOT (a>=3))

Now remove the NOTS from both expressions using the first rule:

(a<3) and (b<7)
(b<7) and (a<3)

Then find the same elements between the two expressions. In this case all the elements from the first expression can be found in the second one and vice versa. This means that the original expressions are completely distinct.