CDD x>=0 and x<0

[Brandhoej]

Clock guard x >= 0

Expected

• The resulting pointer should point to a CDD node which is equivalent to true (In other wordsisEquiv should return true).
• The resulting pointer should preferably point to the terminal true node after reduction (In other words after calling reduce the CDD should have isTrue return True).
• The resulting pointer should if isTrue returns True be a terminal node (In other words after reducing and isTrue returns true then isTerminal should return true).

Actual

• isEquiv to true returns false.
• isTrue returns false.
• isTerminal returns false.
• Interpretation of the CDD dot image below: Looks correct as the diagonal constraint on the global clock allows all valuations of x (x1 on the image) to be true.
  The dot output before and after reduction is the same (preview):

digraph G {
"0x7ff83c9826d1" [shape=box, label="1", style=filled, height=0.3, width=0.3];
"0x7ff83c9826d0" [shape=box, label="0", style=filled, height=0.3, width=0.3];
"0x7ff80c1b00400" [shape=octagon, color = black, label="x1-x0"];
"0x7ff80c1b00400" -> "0x7ff83c9826d1" [style=dashed, label="[0;INF["];
}

Experimentation
True gives the same result (Here the x is added to the cdd. Without the clock we just get the terminal true node which is correct).
x >= n gives the same result for a negative n value.
x >= n || True gives the same result where n is 0 or negative.
x < n || x >= n gives the same result even if n is negative.

Clock guard x < 0

Expected

• The resulting pointer should point to a CDD node which is equivalent to false (In other wordsisEquiv should return false).
• The resulting pointer should preferably point to the terminal false node after reduction (In other words after calling reduce the CDD should have isFalse return True).
• The resulting pointer should if isFalse returns True be a terminal node (In other words after reducing and isFalse returns true then isTerminal should return true).

Actual

• isEquiv to false returns false.
• isFalse returns false.
• isTerminal returns false.
  The dot output before and after reduction is the same (preview):

digraph G {
"0x7ff09e67f6d1" [shape=box, label="1", style=filled, height=0.3, width=0.3];
"0x7ff09e67f6d0" [shape=box, label="0", style=filled, height=0.3, width=0.3];
"0x7ff0701400500" [shape=octagon, color = black, label="x1-x0"];
"0x7ff0701400500" -> "0x7ff09e67f6d1" [style=dashed, label="[0;0["];
}

Experimentation
WIP