src/synth/synthDiv.c

Go to the documentation of this file.

#include "synthInt.h"

static char rcsid[] UNUSED = "$Id: synthDiv.c,v 1.25 2002/09/10 05:50:52 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

#define MAX_COUNT       100000000 /* just chosen for a very large number */

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

typedef struct  bfs_item {
  int                   reach; /* number of path from top node */
  int                   count; /* number of path to constant 1 */
  bdd_node              *node; /* ZDD node */
  struct bfs_item       *next;
} BfsItem;

typedef struct  bfs_list {
  struct bfs_item       *item;
  int                   child; /* 1 : T, 0 : E */
  struct bfs_list       *next;
} BfsList;


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int FindQuickDivisor(bdd_node *f, bdd_node *one, int *v);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/


bdd_node *
Synth_ZddQuickDivisor(bdd_manager *dd,
                      bdd_node *f)
{
  bdd_node      *res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddQuickDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


bdd_node *
Synth_ZddLeastDivisor(bdd_manager *dd,
                      bdd_node *f)
{
  bdd_node      *res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddLeastDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


bdd_node *
Synth_ZddMostDivisor(bdd_manager *dd,
                     bdd_node *f)
{
  bdd_node      *res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddMostDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


bdd_node *
Synth_ZddLevelZeroDivisor(bdd_manager *dd,
                          bdd_node *f)
{
  bdd_node      *res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddLevelZeroDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


bdd_node *
Synth_ZddCommonDivisor(bdd_manager *dd,
                       bdd_node *f)
{
  bdd_node      *res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddCommonDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


bdd_node *
Synth_ZddLpDivisor(bdd_manager *dd,
                   bdd_node *f)
{
  bdd_node      *res;

  if (bdd_get_package_name() != CUDD) {
    (void)fprintf(vis_stderr,
      "** synth error: Synthesis package can be used only with CUDD package\n");
    (void)fprintf(vis_stderr,"** synth error: Please link with CUDD package\n");
    return NIL(bdd_node);
  }

  do {
    bdd_set_reordered_field(dd, 0);
    res = SynthZddLpDivisor(dd, f);
  } while (bdd_read_reordered_field(dd) == 1);
  return(res);
}


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


bdd_node *
SynthZddQuickDivisor(bdd_manager *dd,
                     bdd_node *f)
{
  int           i, v;
  int           nvars;
  int           *count;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *divisor, *node;
  bdd_node      *tmp;
  int           min_count;

  if (f == one || f == zero)
    return(f);

  /* Search for a literal appearing in at least two cubes. */
  v = -1;
  FindQuickDivisor(f, one, &v);
  SynthZddClearFlag(f);

  if (v == -1) {
    /* Quick divisor not found by looking at the ZDD graph.
     * Find the literal that occurs the least among those occuring
     * at least twice.
     */
    min_count = MAX_COUNT;
    nvars = bdd_num_zdd_vars(dd);
    count = ALLOC(int, nvars);
    (void)memset((void *)count, 0, sizeof(int) * nvars);
    SynthCountLiteralOccurrence(dd, f, count);
    for (i = 0; i < nvars; i++) {
      if (count[i] > 1 && count[i] < min_count) {
        v = i;
        min_count = count[i];
      }
    }
    FREE(count);
    if (v == -1) {
      /* All literal appear exactly once. We are done. */
      return(f);
    }
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp) {
    bdd_recursive_deref_zdd(dd,node);
    return(NULL);
  }
  bdd_ref(tmp);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddQuickDivisor(dd, tmp);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd,tmp);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp);

  bdd_deref(divisor);
  return(divisor);
}


bdd_node *
SynthZddLeastDivisor(bdd_manager *dd,
                     bdd_node *f)
{
  int           i, v;
  int           nvars, min_count;
  int           *count;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *divisor, *node;
  bdd_node      *tmp1;

  if (f == one || f == zero)
    return(f);

  /* Find the literal that occurs the least among those occuring at
   * least twice.
   */
  v = -1;
  min_count = MAX_COUNT;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > 1 && count[i] < min_count) {
      v = i;
      min_count = count[i];
    }
  }
  FREE(count);

  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node) {
    return(NULL);
  }
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddLeastDivisor(dd, tmp1);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp1);

  bdd_deref(divisor);
  return(divisor);
}


bdd_node *
SynthZddMostDivisor(bdd_manager *dd,
                    bdd_node *f)
{
  int           i, v;
  int           nvars, max_count;
  int           *count;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *divisor, *node;
  bdd_node      *tmp1;

  if (f == one || f == zero)
    return(f);

  /* Find the literal that occurs the most. */
  v = -1;
  max_count = 1;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > max_count) {
      v = i;
      max_count = count[i];
    }
  }

  FREE(count);

  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddMostDivisor(dd, tmp1);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp1);

  bdd_deref(divisor);
  return(divisor);
}


bdd_node *
SynthZddLevelZeroDivisor(bdd_manager *dd,
                         bdd_node *f)
{
  int           i, v;
  int           nvars, max_count;
  int           *count;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *divisor, *node;
  bdd_node      *tmp1, *tmp2;

  if (f == one || f == zero)
    return(f);

  /* Find the literal that occurs the most. */
  v = -1;
  max_count = 1;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > max_count) {
      v = i;
      max_count = count[i];
    }
  }

  FREE(count);

  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Factor out all literals appearing in all cubes. */
  tmp2 = SynthMakeCubeFree(dd, tmp1);
  if (!tmp2) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(tmp2);
  bdd_recursive_deref_zdd(dd, tmp1);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddLevelZeroDivisor(dd, tmp2);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp2);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp2);

  bdd_deref(divisor);
  return(divisor);
}

bdd_node *
SynthZddCommonDivisor(bdd_manager *dd,
                      bdd_node *f)
{
  int           i;
  int           nvars;
  int           *count;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *divisor, *node, *tmp;
  int           nCubes;

  divisor = (bdd_node *)NULL;   /* NULL means no such divisor exists */
  if (f == one || f == zero)
    return(divisor);

  nCubes = bdd_zdd_count(dd, f);
  if (nCubes == 1)
    return(divisor);

  /* Find the literals that appear exactly as many times as there
   * are cubes. These literals appear in all cubes, hence in the
   * common divisor. Their product is accumulated in divisor. */
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);
  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] == nCubes) {
      node = bdd_zdd_get_node(dd, i, one, zero);
      if (!node) {
        FREE(count);
        return(NULL);
      }
      bdd_ref(node);
      if (!divisor) {
        divisor = node;
        continue;
      }
      tmp = divisor;
      divisor = (* SynthGetZddProductRecurFunc())(dd, divisor, node);
      if (!divisor) {
        bdd_recursive_deref_zdd(dd, tmp);
        bdd_recursive_deref_zdd(dd, node);
        FREE(count);
        return(NULL);
      }
      bdd_ref(divisor);
      bdd_recursive_deref_zdd(dd, tmp);
      bdd_recursive_deref_zdd(dd, node);
    }
  }
  FREE(count);

  if (divisor)
    bdd_deref(divisor);
  return(divisor);
}


bdd_node *
SynthZddLpDivisor(bdd_manager *dd,
                  bdd_node *f)
{
  int           i, v;
  int           nvars, min_count, min_pos = 0;
  int           *count;
  bdd_node      *one = bdd_read_one(dd);
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *divisor, *node;
  bdd_node      *tmp1;

  if (f == one || f == zero)
    return(f);

  /* Find the literal that occurs the least among those occuring at
   * least twice.
   */
  v = -1;
  min_count = MAX_COUNT;
  nvars = bdd_num_zdd_vars(dd);
  count = ALLOC(int, nvars);
  (void)memset((void *)count, 0, sizeof(int) * nvars);

  SynthCountLiteralOccurrence(dd, f, count);
  for (i = 0; i < nvars; i++) {
    if (count[i] > 1 && count[i] < min_count) {
      v = i;
      min_count = count[i];
      min_pos = i;
    }
  }
  if (v == -1) {
    /* All literal appear exactly once. We are done. */
    FREE(count);
    return(f);
  }

  /* Among the literals with minimum count, find a good one. */
  v = SynthFindDivisorForLowPower(count, nvars, min_count, min_pos);

  FREE(count);

  if (v == -1) {
    return(f);
  }

  /* Obtain the literal divisor from its index and divide f. */
  node = bdd_zdd_get_node(dd, v, one, zero);
  if (!node)
    return(NULL);
  bdd_ref(node);

  tmp1 = (* SynthGetZddDivideRecurFunc())(dd, f, node);
  if (!tmp1) {
    bdd_recursive_deref_zdd(dd, node);
    return(NULL);
  }
  bdd_ref(tmp1);
  bdd_recursive_deref_zdd(dd, node);

  /* Recur on the quotient to make sure that all literals appear once. */
  divisor = SynthZddLpDivisor(dd, tmp1);
  if (!divisor) {
    bdd_recursive_deref_zdd(dd, tmp1);
    return(NULL);
  }
  bdd_ref(divisor);
  bdd_recursive_deref_zdd(dd, tmp1);

  bdd_deref(divisor);
  return(divisor);
}


void
SynthCountLiteralOccurrence(bdd_manager *dd,
                            bdd_node *f,
                            int *count)
{
  BfsItem       **level, *item, *cur_item, *next_item, *last_item;
  BfsList       *list, *pre_list, *cur_list, *next_list, *last_list;
  BfsList       *new_list, *save_last_list;
  int           cur_level, next_level, start_level, last_level;
  int           exist;
  bdd_node      *zero = bdd_read_zero(dd);
  bdd_node      *one = bdd_read_one(dd);
  int           i, ct, ce;
  bdd_node      *node;
  int           lv, *index, id;
  int           sizeZ = bdd_num_zdd_vars(dd);

  if (bdd_is_constant(f))
    return;

  level = ALLOC(BfsItem *, sizeZ);
  (void)memset((void *)level, 0, sizeof(BfsItem *) * sizeZ);
  index = ALLOC(int, sizeZ);
  (void)memset((void *)index, 0, sizeof(int) * sizeZ);

  /* Initialize BFS by entering f in the queue. */
  item = ALLOC(BfsItem, 1);
  (void)memset((void *)item, 0, sizeof(BfsItem));
  item->node = f;
  item->reach = 1;
  lv = bdd_read_zdd_level(dd,bdd_node_read_index(f));
  level[lv] = item;
  index[lv] = bdd_node_read_index(f);
  start_level = last_level = lv;

  if (!bdd_is_constant(bdd_bdd_T(f))) {
    list = ALLOC(BfsList, 1);
    (void)memset((void *)list, 0, sizeof(BfsList));
    list->item = item;
    list->child = 1;
    last_list = list;
  } else
    list = last_list = (BfsList *)NULL;
  if (!bdd_is_constant(bdd_bdd_E(f))) {
    last_list = ALLOC(BfsList, 1);
    (void)memset((void *)last_list, 0, sizeof(BfsList));
    last_list->item = item;
    last_list->child = 0;
    if (list)
      list->next = last_list;
    else
      list = last_list;
  }

  /* Perform the BFS. */
  while (list) {
    cur_level = sizeZ;
    cur_list = list;
    while (cur_list) {
      if (cur_list->child)
        id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
      else
        id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
      next_level = bdd_read_zdd_level(dd,id);
      cur_level = (cur_level < next_level) ? cur_level : next_level;
      cur_list = cur_list->next;
    }
    last_level = cur_level;
    save_last_list = last_list;

    pre_list = (BfsList *)NULL;
    cur_list = list;
    while (cur_list) {
      if (cur_list->child)
        id = bdd_node_read_index(bdd_bdd_T(cur_list->item->node));
      else
        id = bdd_node_read_index(bdd_bdd_E(cur_list->item->node));
      next_level = bdd_read_zdd_level(dd,id);

      if (next_level != cur_level) {
        pre_list = cur_list;
        cur_list = cur_list->next;
        continue;
      }

      if (cur_list->child)
        node = bdd_bdd_T(cur_list->item->node);
      else
        node = bdd_bdd_E(cur_list->item->node);

      exist = 0;
      last_item = level[cur_level];
      while (last_item) {
        if (node == last_item->node) {
          last_item->reach += cur_list->item->reach;
          exist = 1;
          break;
        }
        if (last_item->next)
          last_item = last_item->next;
        else
          break;
      }

      if (exist == 0) {
        item = ALLOC(BfsItem, 1);
        (void)memset((void *)item, 0, sizeof(BfsItem));
        item->node = node;
        item->reach = cur_list->item->reach;
        if (last_item)
          last_item->next = item;
        else {
          level[cur_level] = item;
          index[cur_level] = id;
        }

        if (!bdd_is_constant(bdd_bdd_T(node))) {
          new_list = ALLOC(BfsList, 1);
          (void)memset((void *)new_list, 0, sizeof(BfsList));
          new_list->item = item;
          new_list->child = 1;
          last_list->next = new_list;
          last_list = new_list;
        }
        if (!bdd_is_constant(bdd_bdd_E(node))) {
          new_list = ALLOC(BfsList, 1);
          (void)memset((void *)new_list, 0, sizeof(BfsList));
          new_list->item = item;
          new_list->child = 0;
          last_list->next = new_list;
          last_list = new_list;
        }
      }

      next_list = cur_list->next;
      if (cur_list == list && cur_list == last_list) {
        FREE(cur_list);
        list = next_list;
      } else if (cur_list == list) {
        FREE(cur_list);
        pre_list = (BfsList *)NULL;
        if (list == save_last_list) {
          list = next_list;
          next_list = (BfsList *)NULL;
        } else
          list = next_list;
      } else if (cur_list == last_list) {
        if (pre_list)
          pre_list->next = cur_list->next;
        FREE(cur_list);
        last_list = pre_list;
      } else {
        if (pre_list)
          pre_list->next = cur_list->next;
        if (cur_list == save_last_list) {
          FREE(cur_list);
          next_list = (BfsList *)NULL;
        } else
          FREE(cur_list);
      }

      cur_list = next_list;
    }
  }

  /* Compute the number of paths to the constant 1 for each node in
   * bottom up fashion. Update the occurrence count of the variables.
   */
  for (i = last_level; i >= start_level; i--) {
    item = level[i];
    while (item) {
      ct = ce = 0;
      if (bdd_bdd_T(item->node) == one)
        ct = 1;
      else {
        node = bdd_bdd_T(item->node);
        next_level = bdd_read_zdd_level(dd, bdd_node_read_index(node));
        cur_item = level[next_level];
        while (cur_item) {
          if (cur_item->node == node) {
            ct = cur_item->count;
            break;
          }
          cur_item = cur_item->next;
        }
      }
      if (bdd_bdd_E(item->node) != zero) {
        node = bdd_bdd_E(item->node);
        next_level = bdd_read_zdd_level(dd,
                                        bdd_node_read_index(node));
        cur_item = level[next_level];
        while (cur_item) {
          if (cur_item->node == node) {
            ce = cur_item->count;
            break;
          }
          cur_item = cur_item->next;
        }
      }
      item->count = ct + ce;
      count[index[i]] += ct * item->reach;
      item = item->next;
    }
  }

  /* Clean up. */
  for (i = last_level; i >= start_level; i--) {
    item = level[i];
    while (item) {
      next_item = item->next;
      FREE(item);
      item = next_item;
    }
  }

  FREE(level);
  FREE(index);
}


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/


static int
FindQuickDivisor(bdd_node *f,
                 bdd_node *one,
                 int *v)
{
  int           c, ct, ce;
  bdd_node      *temp = bdd_read_next(f);

  if (bdd_is_constant(f)) {
    if (f == one)
      return(1);
    else
      return(0);
  }

  if (bdd_is_complement(temp)) { /* already visited */
    *v = bdd_node_read_index(f);
    return(-1);
  }
  /* mark as visited */
  bdd_set_next(f, bdd_not_bdd_node(temp));

  ct = FindQuickDivisor(bdd_bdd_T(f), one, v);
  if (ct == -1) /* already found */
    return(-1);
  else if (ct > 1) {
    *v = bdd_node_read_index(f);
    return(-1);
  }

  ce = FindQuickDivisor(bdd_bdd_E(f), one, v);
  if (ce == -1) /* already found */
    return(-1);

  /* Add the number of path to constant 1 from two children nodes. */
  c = ct + ce;
  return(c);
}