cdd_interval returns lower bound with incorrect interpretation

[magoorden]

Problem description
We can create a new CDD node with an interval using the method below.

/**
 * Creates a new CDD node corresponding to the constraint \a lower
 * <~ \a i - \a j <~ \a upper, where \a i and \a j are clock indexes and
 * \a lower and \a upper are bounds.
 * @param i a clock index
 * @param j a clock index
 * @param lower a lower bound
 * @param upper an upper bound
 * @return a CDD node encoding the interval
 * @see cdd_upper
 */
extern ddNode* cdd_interval(int32_t i, int32_t j, raw_t lower, raw_t upper);

So, for example, if we want to create a CDD node with the interval 0 <= x - y <= 2, we first convert the bounds into raw bounds: 1 for the unstrict lower bound and 5 for the unsrict upper bound. Then we call cdd_interval(1, 2, 1, 5) (just assume for the sake of simplicity that x has clock index 1 and y has 2). The result is a CDD node having the interval 0 < x - y <= 2, i.e., the strictness of the lower bound has changed.

Similarly, if we want 0 < x - y <= 2, we call cdd_interval(1, 2, 0, 5) and we get 0 <= x - y <= 2.

Root cause analysis
Internally, cdd_interval calls cdd_interval_from_level. This method does the actual work.

The actual interval of a CDD is a stack of bounds cdd_refstacktop. So cdd_interval_from_level adds the lower and upper bounds to this stack with (ignoring the checks for -INF and INF to simplify the explanation)

cdd_push(cddfalse, low);
cdd_push(cddtrue, high);
cdd_push(cddfalse, INF);

The translation of this stack into intervals is (INF to low)->cddfalse, (complement_strictness_of(low), high)->cddtrue, (complement_strictness_of(high), INF)->cddfalse.

So now you see that our desired interval has a flipped lower bound strictness.

Potential solutions
When cdd_interval_from_level pushes the lower bound to the interval stack, it should pushes it with the complementary strictness. But we see that cdd_interval_from_level is used several times by other methods, so other methods might work with this 'error'.