Hi,

It seems that there is a bug in dbm_satisfies (library version 2.0.8) as demonstrated by the code below. This programs "shows" that the DBM (x>=1) satisfies the constraint (x>=2).

In a closed non-empty DBM, D_{i,j} sets the tightest constraint on x_i-x_j. Hence, checking if the DBM D satisfies the constraint x_i-x_j <= c_{i,j} simply amounts to checking D_{i,j} <= c_{i,j} (i.e. the constraint sets a weaker condition than the DBM). This is what is done in the first part of the test in dbm_satisfies:

    !(dbm[i*dim+j] > constraint &&             /* tightening ? */
          dbm_negRaw(constraint) >= dbm[j*dim+i]); /* too tight ? */

However, the second part in the test does not make sense to me and this is precisely the part that fails in the example below.

Best regards,
Frédéric




#include <stdio.h>
#include <stdlib.h>
#include <dbm/dbm.h>

int main() {
  cindex_t dim = 1 + 3;
  raw_t * dbm = (raw_t*) malloc(dim * dim * sizeof(raw_t));

  cindex_t i = 0,
    j = 1; // x

  /* Build DBM for zone (x>=1)
   */
  dbm_init(dbm, dim);

  constraint_t c;
  c.i = i; c.j = j; c.value = dbm_bound2raw(-1, dbm_WEAK);
  dbm_constrainC(dbm, dim, c);

  dbm_close(dbm, dim); // to make sure
  
  /* Checks if DBM satisfies (x>=2)
   */
  raw_t xGE2 = dbm_bound2raw(-2, dbm_WEAK);
  if (dbm_satisfies(dbm, dim, i, j, xGE2))
    printf("SAT\n");
  else
    printf("UNSAT\n");

  /* Checks satisfaction test by hand
   */
  printf("dbm[%d,%d]: %d, constraint: %d\n", i, j, dbm[i*dim+j], xGE2);
  printf("not(constraint): %d, dbm[%d,%d]: %d\n", dbm_negRaw(xGE2), j, i,
	 dbm[j*dim+i]);

  free(dbm);

  return 0;
}